Theorem: prop2_3 (Carleson/Proposition3.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
ψ : ℝ → ℝ
n : ℕ
𝔉 : Forest G Q' δ n
hA : 1 < A
hτ : τ ∈ Ioo 0 1
hq : q ∈ Ioc 1 2
hC₀ : 0 < C₀
hC : C2_3 A τ q C₀ < C
hκ : κ ∈ Ioo 0 (κ2_3 A τ q C₀)
hε : ε ∈ Ioo 0 (ε2_3 A τ q C₀)
hδ : δ ∈ Ioo 0 (δ2_3 A τ q C₀)
hD : (2 * A) ^ 100 < D
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_3 A τ q C₀) ψ
h2ψ : support ψ ⊆ Icc (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ᶠ (s : ℤ), ψ (D ^ s * x) = 1
ht : t ∈ Ioc 0 1
h𝔉 : 𝔉.carrier ⊆ boundedTiles F t
⊢ ↑‖∑ᶠ (p : 𝔓 X) (_ : p ∈ 𝔉.carrier), TL K Q' σ σ' ψ p F‖₊ ≤ C * 2 ^ (-ε * ↑n) * t ^ (1 / q - 1 / 2)
Tactic:
sorry
State after:
no goals