Source indexedlemma · leanprover/lean4:v4.32.0

holderApprox_le

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:266 to 281

Source documentation

Part of Lemma 8.0.1: sup 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 holderApprox_le {R t : ℝ} (hR : 0 < R) {C : ℝ≥0} (ht : 0 < t)
    {φ : X → ℂ} (hC : ∀ x, ‖φ x‖ ≤ C) (x : X) :
    ‖holderApprox R t φ x‖ ≤ C

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma holderApprox_le {R t : ℝ} (hR : 0 < R) {C : ℝ≥0} (ht : 0 < t)    {φ : X → ℂ} (hC : ∀ x, ‖φ x‖ ≤ C) (x : X) :    ‖holderApprox R t φ x‖ ≤ C := by  rw [holderApprox, norm_div, norm_real, Real.norm_eq_abs]  apply div_le_of_le_mul₀ (by positivity) (by positivity)  apply (norm_integral_le_integral_norm _).trans  rw [abs_of_pos (integral_cutoff_pos hR ht), ← integral_const_mul]  apply integral_mono_of_nonneg  · apply Eventually.of_forall (fun x ↦ by positivity)  · apply (integrable_cutoff hR ht).const_mul  apply Eventually.of_forall (fun y ↦ ?_)  simp only [Complex.norm_mul, norm_real, Real.norm_eq_abs, cutoff_nonneg, abs_of_nonneg,    mul_comm (C : ℝ)]  gcongr  · apply cutoff_nonneg  · exact hC y