Theorem: prop2_1 (Carleson/Proposition1.lean)

State before:
X : Type u_1
A : ℝ
inst✝⁶ : MetricSpace X
inst✝⁵ : IsSpaceOfHomogeneousType X A
inst✝⁴ : Inhabited X
τ q q' D κ C₀ C : ℝ
Θ : 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
ψ : ℝ → ℝ
hA : 1 < A
hτ : τ ∈ Ioo 0 1
hq : q ∈ Ioc 1 2
hqq' : q.IsConjExponent q'
hC₀ : 0 < C₀
hC : C2_1 A τ q C₀ < C
hD : D2_1 A τ q C₀ < D
hκ : κ ∈ Ioo 0 (κ2_1 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_1 A τ q C₀) ψ
h2ψ : support ψ ⊆ Icc (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ᶠ (s : ℤ), ψ (D ^ s * x) = 1
⊢ ∃ G',
    volume G' ≤ volume G / 4 ∧
      ↑‖∫ (x : X) in G \ G', ∑' (p : 𝔓 X), T K Q' σ σ' ψ p F 1 x‖₊ ≤
        C * volume.real G ^ (1 / q') * volume.real F ^ (1 / q)
Tactic:
sorry
State after:
no goals