Formalizing arXiv:2212.08956

@[instance_reducible]

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

Every subset of the index type is measurable.

Equations

• Superorthogonal.pointwiseDiscreteMeasurableSpace = ⊤

@[instance_reducible]

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

Count indices with counting measure.

Equations

• Superorthogonal.pointwiseCountingMeasureSpace = { toMeasurableSpace := Superorthogonal.pointwiseDiscreteMeasurableSpace, volume := MeasureTheory.Measure.count }

theorem Superorthogonal.Codex.pointwise_estimate {ι : Type u_2} [Countable ι] {k : ℕ} (hk : 2 ≤ k) (a : Fin k → ι → ℂ) (ha : ∀ (i : Fin k), Summable fun (j : ι) => ‖a i j‖) : ‖Q a - ∏ i : Fin k, s (a i)‖ₑ ≤ (↑k.factorial - 1) * B hk a ^ 2 * max (A hk a) (B hk a) ^ (k - 2)