Theorem: Memℒp_T (Carleson/Defs.lean)

State before:
X : Type u_1
A : ℝ
inst✝³ : PseudoMetricSpace X
inst✝² : IsSpaceOfHomogeneousType X A
D κ C : ℝ
inst✝¹ : Inhabited X
Θ : Set C(X, ℂ)
inst✝ : TileStructure Θ D κ C
K : X → X → ℂ
Q' : X → C(X, ℂ)
σ σ' : X → ℤ
ψ : ℝ → ℝ
p : 𝔓 X
F : Set X
f : X → ℂ
q : ℝ≥0∞
hf : Memℒp f q volume
⊢ Memℒp (T K Q' σ σ' ψ p F f) q volume
Tactic:
sorry
State after:
no goals