Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.correlation_separated_trees_of_subset

Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:92 to 124

Mathematical statement

Exact Lean statement

lemma correlation_separated_trees_of_subset (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hg₁ : BoundedCompactSupport g₁) (hg₂ : BoundedCompactSupport g₂) :
    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂) g₂ x)‖ₑ ≤
    C7_4_4 a n *
    eLpNorm ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) ·) 2 volume *
    eLpNorm ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) ·) 2 volume

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma correlation_separated_trees_of_subset (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hg₁ : BoundedCompactSupport g₁) (hg₂ : BoundedCompactSupport g₂) :    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂) g₂ x)‖ₑ ≤    C7_4_4 a n *    eLpNorm ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) ·) 2 volume *    eLpNorm ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) ·) 2 volume := by  calc    _ = ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) g₂ x) +        adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) g₂ x)‖ₑ := by      congr! 3 with x; rw [← mul_add, ← map_add]; congr 2      rw [adjointCarlesonSum_inter, sub_add_cancel]    _ = ‖(∫ x, adjointCarlesonSum (t u₁) g₁ x *          conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) g₂ x)) +        ∫ x, adjointCarlesonSum (t u₁) g₁ x *          conj (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) g₂ x)‖ₑ := by      congr 1; apply integral_add      · exact (integrable_adjointCarlesonSum (t u₁) hg₁).mul_conj          hg₁.adjointCarlesonSum (integrable_adjointCarlesonSum _ hg₂)      · exact (integrable_adjointCarlesonSum (t u₁) hg₁).mul_conj          hg₁.adjointCarlesonSum (integrable_adjointCarlesonSum _ hg₂)    _ ≤ ‖∫ x, adjointCarlesonSum (t u₁) g₁ x *          conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) g₂ x)‖ₑ +        ‖∫ x, adjointCarlesonSum (t u₁) g₁ x *          conj (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) g₂ x)‖ₑ := enorm_add_le _ _    _ ≤ (C7_4_5 a n + C7_4_6 a n) *        eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) ·) 2 volume *        eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) ·) 2 volume := by      simp_rw [add_mul]; gcongr      · exact correlation_distant_tree_parts hu₁ hu₂ hu h2u hg₁ hg₂      · exact correlation_near_tree_parts hu₁ hu₂ hu h2u hg₁ hg₂    _ ≤ _ := by      rw [inter_eq_self_of_subset_left h2u.1, ← ENNReal.coe_add]; gcongr      apply le_C7_4_4 (four_le_a X)