Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.holder_correlation_tile

Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:838 to 854

Source documentation

Lemma 7.5.5.

Exact Lean statement

lemma holder_correlation_tile (hu : u ∈ t) (hp : p ∈ t u) (hf : BoundedCompactSupport f) :
    edist (exp (.I * 𝒬 u x) * adjointCarleson p f x) (exp (.I * 𝒬 u x') * adjointCarleson p f x') ≤
    C7_5_5 a / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) *
      (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ * ∫⁻ x in E p, ‖f x‖ₑ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma holder_correlation_tile (hu : u ∈ t) (hp : p ∈ t u) (hf : BoundedCompactSupport f) :    edist (exp (.I * 𝒬 u x) * adjointCarleson p f x) (exp (.I * 𝒬 u x') * adjointCarleson p f x') ≤    C7_5_5 a / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) *      (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ * ∫⁻ x in E p, ‖f x‖ₑ := by  by_cases hxx : x ∉ ball (𝔠 p) (5 * D ^ 𝔰 p) ∧ x' ∉ ball (𝔠 p) (5 * D ^ 𝔰 p)  · rw [adjoint_tile_support1, indicator_of_notMem hxx.1, indicator_of_notMem hxx.2]; simp  rw [not_and_or, not_notMem, not_notMem] at hxx  wlog hx : x ∈ ball (𝔠 p) (5 * D ^ 𝔰 p) generalizing x x'  · rw [or_comm] at hxx; specialize this hxx (hxx.resolve_right hx)    rwa [edist_comm, edist_comm x' x] at this  clear hxx  by_cases! hx' : x' ∉ ball (𝔠 p) (5 * D ^ 𝔰 p)  · nth_rw 2 [adjoint_tile_support1]    rw [indicator_of_notMem hx', mul_zero, edist_zero_right, enorm_mul, mul_comm I, ← enorm_norm,      norm_exp_ofReal_mul_I, enorm_one, one_mul]    exact holder_correlation_tile_one hf hx'  exact holder_correlation_tile_two hu hp hf hx hx'