OAI/RepresentationTheory/FiniteUnitary/Fourier.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CubeShuffle.FiniteFourier.CoefficientIndex line 18
  2. def OAI.CubeShuffle.FiniteFourier.coefficientFamily line 20
  3. lemma OAI.CubeShuffle.FiniteFourier.coefficientFamily_orthonormal line 25
  4. lemma OAI.CubeShuffle.FiniteFourier.coefficientIndex_card line 38
  5. def OAI.CubeShuffle.FiniteFourier.coefficientBasis line 42
  6. lemma OAI.CubeShuffle.FiniteFourier.coefficientBasis_apply line 47
  7. theorem OAI.CubeShuffle.FiniteFourier.parseval line 53

    Source documentation

    Finite-group Plancherel, produced from the actual complete irreducible coefficient basis rather than postulated as a Fourier hypothesis.

    theorem parseval (f : EuclideanSpace ℂ G) :
    ∑ a : CoefficientIndex V, ‖inner ℂ (coefficientFamily V ρ a) f‖^2=‖f‖^2 := by
…

    Mentions: OAI.CubeShuffle.FiniteFourier.CoefficientIndex, OAI.CubeShuffle.FiniteFourier.coefficientFamily

  8. def OAI.CubeShuffle.FiniteFourier.realVector line 71
  9. lemma OAI.CubeShuffle.FiniteFourier.coefficient_realVector line 74
  10. lemma OAI.CubeShuffle.FiniteFourier.coefficient_realVector_sq line 88
  11. lemma OAI.CubeShuffle.FiniteFourier.parseval_operator line 97
  12. lemma OAI.CubeShuffle.FiniteFourier.realVector_bound line 120
  13. theorem OAI.CubeShuffle.FiniteFourier.l1_fourier_bound line 138

    Source documentation

    The exact full-group Fourier upper bound, with no marginal replacement.

    theorem l1_fourier_bound (p : G → ℝ) :
    (∑ g,|p g|)^2≤∑ i,(Module.finrank ℂ (V i):ℝ)^2*‖weightedOperator (ρ i) p‖^2 := by
…