`BookProof.CarlemanUnboundedHop.geoHop_norm_off` {b : ℕ → ℝ} {rho : ℝ} (hrho : 0 ≤ rho) {n k : ℕ} (h : n ≠ k) : ‖geoHop b rho n k‖ = (1 + ((min n k : ℕ) : ℝ)) * rho ^ (max n...
ProvedBookProof.CarlemanUnboundedHop.geoHop_norm_offtheoremstimepiece
Prove the following Lean 4 theorem from ChapterCarlemanUnboundedHop.
BookProof.CarlemanUnboundedHop.geoHop_norm_off {b : ℕ → ℝ} {rho : ℝ} (hrho : 0 ≤ rho) {n k : ℕ} (h : n ≠ k) : ‖geoHop b rho n k‖ = (1 + ((min n k : ℕ) : ℝ)) * rho ^ (max n k - min n k)
Formalization note: Lean 4 identifier BookProof.CarlemanUnboundedHop.geoHop_norm_off.
Preamble
-- Generated from ChapterCarlemanUnboundedHop.lean — theorem BookProof.CarlemanUnboundedHop.geoHop_norm_off
import Mathlib
import Definitions.Def_ChapterCarlemanUnboundedHop
open BookProof.CarlemanUnboundedHop
open Finset
noncomputable section
variable {a : ℕ → ℕ → ℂ} {u : ℕ → ℂ} {A θ Θ : ℕ → ℝ}Formal statement
theorem BookProof.CarlemanUnboundedHop.geoHop_norm_off {b : ℕ → ℝ} {rho : ℝ} (hrho : 0 ≤ rho) {n k : ℕ} (h : n ≠ k) :
‖geoHop b rho n k‖ = (1 + ((min n k : ℕ) : ℝ)) * rho ^ (max n k - min n k) := by sorry