Source indexedlemma · leanprover/lean4:v4.32.0

cdist_le_iterate

Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:507 to 517

Mathematical statement

Exact Lean statement

lemma cdist_le_iterate {x : X} {r : ℝ} (hr : 0 < r) (f g : Θ X) (k : ℕ) :
    dist_{x, 2 ^ k * r} f g ≤ (defaultA a) ^ k * dist_{x, r} f g

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cdist_le_iterate {x : X} {r : ℝ} (hr : 0 < r) (f g : Θ X) (k : ℕ) :    dist_{x, 2 ^ k * r} f g ≤ (defaultA a) ^ k * dist_{x, r} f g := by  induction k with  | zero => simp_rw [pow_zero, one_mul]; congr! <;> simp  | succ k ih =>    trans defaultA a * dist_{x, 2 ^ k * r} f g    · convert cdist_le _ using 1      · exact dist_congr rfl (by ring)      · rw [dist_self]; positivity    · replace ih := (mul_le_mul_iff_right₀ (show 0 < (defaultA a : ℝ) by positivity)).mpr ih      rwa [← mul_assoc, ← pow_succ'] at ih