OAI/NumberTheory/Ostmann/Characters/SparseTensorPolynomial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.localSparseCoefficient line 13
2. def OAI.Ostmann.sparseTensorCoefficient line 22
3. theorem OAI.Ostmann.sparseTensorKernel_polynomial line 28
4. theorem OAI.Ostmann.finiteKernelOperator_polynomial line 51
5. theorem OAI.Ostmann.sparseTensorOperator_polynomial line 61
6. theorem OAI.Ostmann.sparseTensorOperator_truncation_error line 70

   Source documentation

   The actual coefficient truncation of the tensor has exponentially small error in the cutoff, with the exact radius 1.03 from the local estimate.

   theorem sparseTensorOperator_truncation_error {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)
       (K : ℕ) :
       ‖finiteKernelOperator (sparseTensorKernel p S 1 1) -
         rectangularPolynomialSum (fun i j => finiteKernelOperator (sparseTensorCoefficient p S i j))
   …

   Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.finiteKernelOperator, OAI.Ostmann.sparseTensorKernel, OAI.Ostmann.rectangularPolynomialSum, OAI.Ostmann.sparseTensorCoefficient