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