Formalizing arXiv:2212.08956

@[instance_reducible]

def Superorthogonal.familyDiscreteMeasurableSpace {ι : Type u_2} : MeasurableSpace ι

Every subset of the index type is measurable.

Equations

• Superorthogonal.familyDiscreteMeasurableSpace = ⊤

@[instance_reducible]

noncomputable def Superorthogonal.familyCountingMeasureSpace {ι : Type u_2} : MeasureTheory.MeasureSpace ι

Count indices with counting measure.

Equations

• Superorthogonal.familyCountingMeasureSpace = { toMeasurableSpace := Superorthogonal.familyDiscreteMeasurableSpace, volume := MeasureTheory.Measure.count }

def Superorthogonal.allDistinct {ι : Type u_2} (k : ℕ) (j : Fin k → ι) : Prop

The k tuple j consists of all distinct indices.

Equations

• Superorthogonal.allDistinct k j = ∀ (i i' : Fin k), i ≠ i' → j i ≠ j i'

@[reducible, inline]

abbrev Superorthogonal.cprod {α : Type u_1} {ι : Type u_2} (f : ι → α → ℂ) {r : ℕ} (j : Fin (2 * r) → ι) (x : α) : ℂ

The product function x ↦ ∏ i < r, f (j i) x * ∏ i ≥ r, conj f (j i) x

Equations

• Superorthogonal.cprod f j x = ∏ i : Fin (2 * r), if ↑i < r then f (j i) x else star (f (j i) x)

structure Superorthogonal.TypeIVSuperorthogonal {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {ι : Type u_2} (f : ι → α → ℂ) (r : ℕ) : Prop

Type IV superorthogonality of a family of functions

• measurable (j : ι) : Measurable (f j)
• integrable_cprod (j : Fin (2 * r) → ι) : allDistinct (2 * r) j → MeasureTheory.Integrable (cprod f j) μ
• superorthogonal (j : Fin (2 * r) → ι) : allDistinct (2 * r) j → ∫ (x : α), cprod f j x ∂μ = 0

noncomputable def Superorthogonal.sqfct {α : Type u_1} {ι : Type u_2} (f : ι → α → ℂ) (x : α) : ℝ

Square-function associated with the family of functions f

Equations

• Superorthogonal.sqfct f x = (∑' (j : ι), ‖f j x‖ ^ 2) ^ 2⁻¹

@[reducible, inline]

noncomputable abbrev Superorthogonal.s {ι : Type u_2} (a : ι → ℂ) : ℂ

Sum of a sequence.

Equations

• Superorthogonal.s a = ∑' (j : ι), a j

@[reducible, inline]

abbrev Superorthogonal.allDistinctSet {ι : Type u_2} (k : ℕ) : Set (Fin k → ι)

Set of k tuples of all distinct indices.

Equations

• Superorthogonal.allDistinctSet k j = Superorthogonal.allDistinct k j

@[reducible, inline]

noncomputable abbrev Superorthogonal.Q {ι : Type u_2} {k : ℕ} (a : Fin k → ι → ℂ) : ℂ

Auxiliary quantity Q from the pointwise estimate

Equations

• Superorthogonal.Q a = ∑' (j : Fin k → ι), (Superorthogonal.allDistinctSet k).indicator (fun (j : Fin k → ι) => ∏ i : Fin k, a i (j i)) j

@[reducible, inline]

noncomputable abbrev Superorthogonal.A {ι : Type u_2} {k : ℕ} (hk : 2 ≤ k) (a : Fin k → ι → ℂ) : ENNReal

Auxiliary quantity A from the pointwise estimate

Equations

• Superorthogonal.A hk a = ENNReal.ofReal ((Finset.image (fun (i : Fin k) => ‖Superorthogonal.s (a i)‖) Finset.univ).max' ⋯)

@[reducible, inline]

noncomputable abbrev Superorthogonal.B {ι : Type u_2} {k : ℕ} (hk : 2 ≤ k) (a : Fin k → ι → ℂ) : ENNReal

Auxiliary quantity B from the pointwise estimate

Equations

• Superorthogonal.B hk a = (Finset.image (fun (i : Fin k) => MeasureTheory.eLpNorm (a i) 2 MeasureTheory.volume) Finset.univ).max' ⋯

noncomputable def Superorthogonal.C (r : ℕ) : ENNReal

Constant in the main theorem on Type IV superorthogonality

Equations

• Superorthogonal.C 1 = 1
• Superorthogonal.C r = 2 ^ 2⁻¹ * (↑(2 * r).factorial - 1) ^ 2⁻¹