OAI/NumberTheory/Ostmann/Supply/CenteredResidueProjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.centeredSupportProjection_sub line 10
2. theorem OAI.Ostmann.centeredSupportProjection_const_mul line 19
3. theorem OAI.Ostmann.centeredSupportProjection_constant_on line 28
4. theorem OAI.Ostmann.centeredSupportProjection_residue_zero line 46
5. theorem OAI.Ostmann.centeredSupportProjection_compl_residue_zero line 54
6. theorem OAI.Ostmann.centered_residue_projection_energy_le line 65

   Source documentation

   Annihilation of the physical indicator turns the sparse projection error into the small side block required by Lemma 5.2.

   theorem centered_residue_projection_energy_le {p : ℕ} [NeZero p]
       (S E T : Finset (ZMod p)) (ε : ℝ)
       (hT : centeredSupportProjection T (normalizedResidueIndicator S) = fun _ => 0)
       (herr : (∑ x, ‖normalizedResidueIndicator S x -
         finiteSpectralProjection E (normalizedResidueIndicator S) x‖ ^ 2) ≤ ε ^ 2 * p) :
       (∑ x, ‖centeredSupportProjection T
         (finiteSpectralProjection E (normalizedResidueIndicator S)) x‖ ^ 2) ≤ ε ^ 2 * p := by
   …

   Mentions: OAI.Ostmann.centeredSupportProjection, OAI.Ostmann.normalizedResidueIndicator, OAI.Ostmann.finiteSpectralProjection