Source indexedlemma · leanprover/lean4:v4.32.0

le_cdist_iterate

Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:494 to 505

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma le_cdist_iterate {x : X} {r : ℝ} (hr : 0 ≤ r) (f g : Θ X) (k : ℕ) :    2 ^ k * dist_{x, r} f g ≤ dist_{x, (defaultA a) ^ k * r} f g := by  induction k with  | zero => rw [pow_zero, one_mul]; congr! <;> simp  | succ k ih =>    trans 2 * dist_{x, (defaultA a) ^ k * r} f g    · rw [pow_succ', mul_assoc]      exact (mul_le_mul_iff_right₀ zero_lt_two).mpr ih    · convert le_cdist (ball_subset_ball _) using 1      · exact dist_congr rfl (by rw [← mul_assoc, pow_succ'])      · nth_rw 1 [← one_mul ((defaultA a) ^ k * r)]; gcongr        rw [← Nat.cast_one, Nat.cast_le]; exact Nat.one_le_two_pow