Source indexedlemma · leanprover/lean4:v4.32.0

cdist_le_mul_cdist

Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:519 to 531

Mathematical statement

Exact Lean statement

lemma cdist_le_mul_cdist {x x' : X} {r r' : ℝ} (hr : 0 < r) (hr' : 0 < r') (f g : Θ X) :
    dist_{x', r'} f g ≤ As (defaultA a) ((r' + dist x' x) / r) * dist_{x, r} f g

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cdist_le_mul_cdist {x x' : X} {r r' : ℝ} (hr : 0 < r) (hr' : 0 < r') (f g : Θ X) :    dist_{x', r'} f g ≤ As (defaultA a) ((r' + dist x' x) / r) * dist_{x, r} f g := by  calc    dist_{x', r'} f g ≤ dist_{x, 2 ^ _ * r} f g := ?e    _ ≤ _ := cdist_le_iterate hr f g _  case e =>    apply cdist_mono    apply ball_subset_ball'    calc      r' + dist x' x = (r' + dist x' x) / r * r := div_mul_cancel₀ _ hr.ne' |>.symm      _ ≤ 2 ^ ⌈Real.logb 2 ((r' + dist x' x) / r)⌉₊ * r := by        gcongr        apply Real.le_pow_natCeil_logb (by norm_num) (by positivity)