Source indexedlemma · leanprover/lean4:v4.32.0

iLipENorm_holderApprox_le

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:482 to 499

Mathematical statement

Exact Lean statement

lemma iLipENorm_holderApprox_le {z : X} {R t : ℝ} (ht : 0 < t) (h't : t ≤ 1)
    {φ : X → ℂ} (hφ : support φ ⊆ ball z R) :
    iLipENorm (holderApprox R t φ) z (2 * R) ≤
      2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * iHolENorm φ z (2 * R) τ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma iLipENorm_holderApprox_le {z : X} {R t : ℝ} (ht : 0 < t) (h't : t ≤ 1)    {φ : X → ℂ} (hφ : support φ ⊆ ball z R) :    iLipENorm (holderApprox R t φ) z (2 * R) ≤      2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * iHolENorm φ z (2 * R) τ := by  rcases eq_or_ne (iHolENorm φ z (2 * R) τ) ∞ with h'φ | h'φ  · apply le_top.trans_eq    rw [eq_comm]    simp only [defaultτ] at h'φ    simp [h'φ, ht]  rw [← ENNReal.coe_toNNReal h'φ]  apply iLipENorm_holderApprox' ht h't  · apply continuous_of_iHolENorm_ne_top' (τ_pos X) hφ h'φ  · exact hφ  · apply fun x ↦ norm_le_iHolNNNorm_of_subset h'φ (hφ.trans ?_)    intro y hy    simp only [mem_ball] at hy ⊢    have : 0 < R := dist_nonneg.trans_lt hy    linarith