OAI/NumberTheory/Ostmann/Characters/SparseTensorModes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.centeredCoordinateSupport line 11
2. theorem OAI.Ostmann.localSparseCoefficient_constant line 15
3. theorem OAI.Ostmann.sparseTensorCoefficient_mode_support line 26

   Source documentation

   A coefficient of bidegree (j,k) vanishes on every output or input coordinate with more than j+k centered factors.

   theorem sparseTensorCoefficient_mode_support {n : ℕ}
       (p : Fin n → ℕ) [∀ i, NeZero (p i)]
       (S : ∀ i, Finset (ZMod (p i))) (j k : ℕ)
       (x y : ∀ i, Option (ZMod (p i)))
       (h : j + k < (centeredCoordinateSupport x).card ∨
         j + k < (centeredCoordinateSupport y).card) :
       sparseTensorCoefficient p S j k x y = 0 := by
   …

   Mentions: OAI.Ostmann.centeredCoordinateSupport, OAI.Ostmann.sparseTensorCoefficient

4. def OAI.Ostmann.truncatedSparseTensorKernel line 54
5. theorem OAI.Ostmann.truncatedSparseTensorKernel_mode_support line 59
6. theorem OAI.Ostmann.truncatedSparseTensorKernel_projected line 79