Theorem: equation2_2 (Carleson/Carleson.lean)

State before:
X : Type u_1
a : ℝ
inst✝⁵ : MetricSpace X
inst✝⁴ : IsSpaceOfHomogeneousType X a
inst✝³ : Inhabited X
τ q q' C : ℝ
Θ : Set C(X, ℂ)
inst✝² : IsCompatible Θ
inst✝¹ : IsCancellative a Θ
F G : Set X
K : X → X → ℂ
inst✝ : IsCZKernel a K
D : ℝ
ψ : ℝ → ℝ
s : ℤ
x y : X
hD : D > D1_1 a τ q
hψ : LipschitzWith (Cψ1_1 a τ q) ψ
h2ψ : support ψ = Ioo (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ s ∈ nonzeroS D x, ψ (D ^ s * x) = 1
hA : 1 < a
hτ : τ ∈ Ioo 0 1
hq : q ∈ Ioc 1 2
hqq' : q.IsConjExponent q'
hF : MeasurableSet F
hG : MeasurableSet G
h2F : volume F ∈ Ioo 0 ⊤
h2G : volume G ∈ Ioo 0 ⊤
hT : NormBoundedBy (ANCZOperatorLp 2 K) (2 ^ a ^ 3)
⊢ ∃ G',
    volume G' ≤ volume G / 2 ∧
      ↑‖∫ (x : X) in G \ G', CarlesonOperator K Θ (F.indicator 1) x‖₊ ≤
        Ce2_2 a τ q * volume.real G ^ (1 / q') * volume.real F ^ (1 / q)
Tactic:
sorry
State after:
no goals