OAI/NumberTheory/Ostmann/Supply/CenteredSupportProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.finiteSupportMean line 10
2. def OAI.Ostmann.centeredSupportProjection line 13
3. theorem OAI.Ostmann.finiteSupportMean_spec line 17
4. theorem OAI.Ostmann.centered_support_energy line 25
5. theorem OAI.Ostmann.centeredSupportProjection_energy line 42
6. theorem OAI.Ostmann.centeredSupportProjection_energy_le line 52
7. theorem OAI.Ostmann.centeredSupportProjection_eq_of_eqOn line 59
8. theorem OAI.Ostmann.centeredSupportProjection_disjoint line 70
9. theorem OAI.Ostmann.centeredSupportProjection_spectral_energy line 77

   Source documentation

   The off-diagonal compression has norm at most one half. This uses only orthogonal support and the exact half-identity spectral bound.

   theorem centeredSupportProjection_spectral_energy {p : ℕ} [NeZero p]
       (S T E : Finset (ZMod p)) (hST : Disjoint S T) (f : ZMod p → ℂ) :
       (∑ x, ‖centeredSupportProjection S
         (finiteSpectralProjection E (centeredSupportProjection T f)) x‖ ^ 2) ≤
         (1 / 4 : ℝ) * ∑ x, ‖f x‖ ^ 2 := by
   …

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