Source indexedlemma · leanprover/lean4:v4.32.0

enorm_integral_exp_le

Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:242 to 259

Mathematical statement

Exact Lean statement

lemma enorm_integral_exp_le [CompatibleFunctions ℝ X A] {τ : ℝ} [IsCancellative X τ]
    {x : X} {r : ℝ} {φ : X → ℂ} (h2 : support φ ⊆ ball x r) {f g : Θ X} :
    ‖∫ x, exp (I * (f x - g x)) * φ x‖ₑ ≤
    (A : ℝ≥0∞) * volume (ball x r) * iLipENorm φ x r * (1 + edist_{x, r} f g) ^ (- τ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma enorm_integral_exp_le [CompatibleFunctions ℝ X A] {τ : ℝ} [IsCancellative X τ]    {x : X} {r : ℝ} {φ : X → ℂ} (h2 : support φ ⊆ ball x r) {f g : Θ X} :    ‖∫ x, exp (I * (f x - g x)) * φ x‖ₑ ≤    (A : ℝ≥0∞) * volume (ball x r) * iLipENorm φ x r * (1 + edist_{x, r} f g) ^ (- τ) := by  rcases le_or_gt r 0 with hr | hr  · simp only [ball_eq_empty.2 hr, subset_empty_iff, support_eq_empty_iff] at h2    simp [h2]  rcases eq_or_ne A 0 with rfl | hA  · have : (volume : Measure X) = 0 := by      have := hXA.toIsDoubling      simp at this      apply eq_zero_of_isDoubling_zero    simp [this]  rcases eq_or_ne (iLipENorm φ x r) ∞ with h1 | h1  · apply le_top.trans_eq    symm    simp [h1, edist_ne_top, hA, (measure_ball_pos volume x hr).ne']  exact IsCancellative.enorm_integral_exp_le' hr h1 h2