Source indexedlemma · leanprover/lean4:v4.32.0

norm_holderApprox_sub_le

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:406 to 433

Source documentation

Part of Lemma 8.0.1: Lipschitz norm control in Equation (8.0.2). Note that it only uses the sup norm of φ, no need for a Hölder control.

Exact Lean statement

lemma norm_holderApprox_sub_le {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (h't : t ≤ 1)
    {C : ℝ≥0} {φ : X → ℂ} (hc : Continuous φ) (hφ : φ.support ⊆ ball z R)
    (hC : ∀ x, ‖φ x‖ ≤ C) {x x' : X} :
    ‖holderApprox R t φ x - holderApprox R t φ x'‖ ≤
    2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - a : ℝ) * C * dist x x' / (2 * R)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_holderApprox_sub_le {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (h't : t ≤ 1)    {C : ℝ≥0} {φ : X → ℂ} (hc : Continuous φ) (hφ : φ.support ⊆ ball z R)    (hC : ∀ x, ‖φ x‖ ≤ C) {x x' : X} :    ‖holderApprox R t φ x - holderApprox R t φ x'‖ ≤    2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - a : ℝ) * C * dist x x' / (2 * R) := by  rcases lt_or_ge (dist x x') R with hx | hx  · rw [norm_sub_rev]    exact norm_holderApprox_sub_le_aux hR ht h't hc hφ hC hx  calc    ‖holderApprox R t φ x - holderApprox R t φ x'‖  _ ≤ ‖holderApprox R t φ x‖ + ‖holderApprox R t φ x'‖ := norm_sub_le _ _  _ ≤ C + C := by    gcongr    · exact holderApprox_le hR ht hC x    · exact holderApprox_le hR ht hC x'  _ = 2⁻¹ * 2 ^ 3 * 1 * C * 2⁻¹ := by ring  _ ≤ 2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - a : ℝ) * C * (dist x x' / (2 * R)) := by    gcongr    · exact one_le_two    · have : 4 ≤ a := four_le_a X      linarith    · apply Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht h't      have : (4 : ℝ) ≤ a := mod_cast (four_le_a X)      linarith    · simp only [inv_eq_one_div]      apply (div_le_div_iff₀ (by norm_num) (by positivity)).2      linarith  _ = _ := by ring