Theorem: prop2_2 (Carleson/Proposition2.lean)

State before:
X : Type u_1
A : ℝ
inst✝⁶ : MetricSpace X
inst✝⁵ : IsSpaceOfHomogeneousType X A
inst✝⁴ : Inhabited X
τ q D κ ε C₀ C t : ℝ
Θ : Set C(X, ℂ)
inst✝³ : IsCompatible Θ
inst✝² : IsCancellative τ Θ
inst✝¹ : TileStructure Θ D κ C₀
F G : Set X
σ σ' : X → ℤ
Q' : X → C(X, ℂ)
K : X → X → ℂ
inst✝ : IsCZKernel τ K
ψ : ℝ → ℝ
𝔄 : Set (𝔓 X)
hA : 1 < A
hτ : τ ∈ Ioo 0 1
hq : q ∈ Ioc 1 2
hC₀ : 0 < C₀
hC : C2_2 A τ q C₀ < C
hD : D2_2 A τ q C₀ < D
hκ : κ ∈ Ioo 0 (κ2_2 A τ q C₀)
hε : ε ∈ Ioo 0 (ε2_2 A τ q C₀)
hF : MeasurableSet F
hG : MeasurableSet G
h2F : volume F ∈ Ioo 0 ⊤
h2G : volume G ∈ Ioo 0 ⊤
Q'_mem : ∀ (x : X), Q' x ∈ Θ
m_Q' : Measurable Q'
m_σ : Measurable σ
m_σ' : Measurable σ'
hT : NormBoundedBy (ANCZOperatorLp 2 K) 1
hψ : LipschitzWith (Cψ2_2 A τ q C₀) ψ
h2ψ : support ψ ⊆ Icc (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ᶠ (s : ℤ), ψ (D ^ s * x) = 1
ht : t ∈ Ioc 0 1
h𝔄 : IsAntichain (fun x x_1 => x ≤ x_1) 𝔄
h2𝔄 : 𝔄 ⊆ boundedTiles F t
h3𝔄 : 𝔄.Finite
⊢ ↑‖∑ᶠ (p : 𝔓 X) (_ : p ∈ 𝔄), TL K Q' σ σ' ψ p F‖₊ ≤ C * density G Q' 𝔄 ^ ε * t ^ (1 / q - 1 / 2)
Tactic:
sorry
State after:
no goals