SparseTensorKernel.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual sparse tensor kernel of Section 5.3

def OAI.Ostmann.sparseTensorKernel line 12
theorem OAI.Ostmann.product_one_add_le_exp_sum line 18
theorem OAI.Ostmann.sparseTensorKernel_energy_le line 26

theorem OAI.Ostmann.sparseTensorKernel_contraction line 51

Source documentation

The full (untruncated) product has the manuscript's strict exponential contraction.

theorem sparseTensorKernel_contraction {n : ℕ} (p : Fin n → ℕ) [∀ i, Fact (p i).Prime]
    (S : ∀ i, Finset (ZMod (p i)))
    (hS : ∀ i, (S i).Nonempty) (hSp : ∀ i, (S i).card < p i)
    (hp : ∀ i, (100 : ℝ) ≤ p i)
    (hlo : ∀ i, (1 / 3 : ℝ) ≤ residueDensity (S i))
    (hhi : ∀ i, residueDensity (S i) ≤ 2 / 3)
    (ε : ℝ) (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 1000000)
    (hL1 : ∀ i, (p i : ℝ)⁻¹ * ∑ b, ‖normalizedResidueTransform (S i) b‖ ≤ ε ^ 2)
    (f : (∀ i, Option (ZMod (p i))) → ℂ) :
    let U := ∏ i, sparseKernelUnitFactor (p i)
…

Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.sparseKernelUnitFactor

theorem OAI.Ostmann.sparseTensorKernel_point_identity line 88