OAI/NumberTheory/Ostmann/Supply/CenteredCoordinateSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.supportedCoordinates line 11
2. theorem OAI.Ostmann.supportedCoordinates_support line 15
3. theorem OAI.Ostmann.supportedCoordinates_injective line 21
4. theorem OAI.Ostmann.supportedCoordinates_reconstruct line 33
5. def OAI.Ostmann.centeredSupportEquiv line 45
6. theorem OAI.Ostmann.tensorPointCoordinates_supported line 55
7. theorem OAI.Ostmann.lowMode_tensor_energy line 77

   Source documentation

   The low-mode norm appearing in the actual truncated-kernel pairing is the sum of the centered subset energies, without a dimension-dependent loss.

   theorem lowMode_tensor_energy {n : ℕ} (p : Fin n → ℕ) [∀ i, NeZero (p i)]
       (S : ∀ i, Finset (ZMod (p i))) {ι : Type*} (A : Finset ι)
       (a : ι → ∀ i, ZMod (p i)) (K : ℕ) :
       countingVectorNorm (lowModeVector K
         (averagedCoordinates A (fun x => tensorPointCoordinates p S (a x)))) ^ 2 =
         ∑ T : Finset (Fin n), if T.card ≤ K then centeredSubsetEnergy p S T A a else 0 := by
   …

   Mentions: OAI.Ostmann.countingVectorNorm, OAI.Ostmann.lowModeVector, OAI.Ostmann.averagedCoordinates, OAI.Ostmann.tensorPointCoordinates, OAI.Ostmann.centeredSubsetEnergy