Formalizing arXiv:2212.08956
theorem
Superorthogonal.Codex.sqfct_estimate_of_type_iv_superorthogonal_finite
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
{ι : Type u_2}
{r : ℕ}
[Finite ι]
{f : ι → α → ℂ}
(hr : 1 ≤ r)
(hf : TypeIVSuperorthogonal μ f r)
(hsq : MeasureTheory.MemLp (sqfct f) (2 * ↑r) μ)
:
MeasureTheory.eLpNorm (∑' (j : ι), f j) (2 * ↑r) μ ≤ C r * MeasureTheory.eLpNorm (sqfct f) (2 * ↑r) μ
theorem
Superorthogonal.Codex.sqfct_estimate_of_type_iv_superorthogonal
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
{ι : Type u_2}
{r : ℕ}
[Countable ι]
[Fact (1 ≤ 2 * ↑r)]
(hr : 1 ≤ r)
{f : ι → ↥(MeasureTheory.Lp ℂ (2 * ↑r) μ)}
(hf : TypeIVSuperorthogonal μ (fun (i : ι) => ↑↑(f i)) r)
(hsum : ∀ᵐ (x : α) ∂μ, Summable fun (j : ι) => ‖↑↑(f j) x‖ ^ 2)
(hsq : MeasureTheory.MemLp (sqfct fun (i : ι) => ↑↑(f i)) (2 * ↑r) μ)
: