OAI/NumberTheory/Ostmann/Supply/FiniteSpectralProjection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.densityFourier_sub line 10
2. theorem OAI.Ostmann.densityFourier_const_mul line 14
3. theorem OAI.Ostmann.densityFourierInverse_fourier line 20
4. def OAI.Ostmann.finiteSpectralProjection line 26
5. theorem OAI.Ostmann.finiteSpectralProjection_fourier line 30
6. theorem OAI.Ostmann.finiteSpectralProjection_energy line 36

   Source documentation

   The counting energy of the projection equals the selected Fourier energy.

   theorem finiteSpectralProjection_energy {p : ℕ} [NeZero p]
       (E : Finset (ZMod p)) (f : ZMod p → ℂ) :
       (∑ x, ‖finiteSpectralProjection E f x‖ ^ 2) =
         ∑ b ∈ E, ‖densityFourier f b‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.finiteSpectralProjection, OAI.Ostmann.densityFourier

7. theorem OAI.Ostmann.finiteSpectralProjection_energy_le line 44
8. theorem OAI.Ostmann.finiteSpectralProjection_residual_energy line 51

   Source documentation

   The exact discarded energy, rather than a dimension-dependent bound.

   theorem finiteSpectralProjection_residual_energy {p : ℕ} [NeZero p]
       (E : Finset (ZMod p)) (f : ZMod p → ℂ) :
       (∑ x, ‖f x - finiteSpectralProjection E f x‖ ^ 2) =
         ∑ b ∈ Finset.univ \ E, ‖densityFourier f b‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.finiteSpectralProjection, OAI.Ostmann.densityFourier

9. theorem OAI.Ostmann.finiteSpectralProjection_half_energy line 67

   Source documentation

   Every spectral projection minus half the identity has operator norm one half, expressed in the counting energy needed for the block estimate.

   theorem finiteSpectralProjection_half_energy {p : ℕ} [NeZero p]
       (E : Finset (ZMod p)) (f : ZMod p → ℂ) :
       (∑ x, ‖finiteSpectralProjection E f x - (1 / 2 : ℂ) * f x‖ ^ 2) =
         (1 / 4 : ℝ) * ∑ x, ‖f x‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.finiteSpectralProjection

10. theorem OAI.Ostmann.finiteSpectralProjection_idempotent line 86

    Source documentation

    Zero outside the selected frequencies makes the projection idempotent.

    theorem finiteSpectralProjection_idempotent {p : ℕ} [NeZero p]
        (E : Finset (ZMod p)) (f : ZMod p → ℂ) :
        finiteSpectralProjection E (finiteSpectralProjection E f) = finiteSpectralProjection E f := by
    …

    Mentions: OAI.Ostmann.finiteSpectralProjection

11. theorem OAI.Ostmann.finiteSpectralProjection_constant line 95