CharacterPacketTotality.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Totality of character translates of a nonvanishing scalar packet

Fourier uniqueness proves totality on the actual vector-valued L² space. No countability or pointwise choice of vector representatives is needed.

theorem OAI.KadisonKastler.fourierChar_eq_star_character line 19

theorem OAI.KadisonKastler.eq_zero_of_inner_character_packets line 30

Source documentation

Every vector orthogonal to all character translates of the packet is zero.

theorem eq_zero_of_inner_character_packets
    (φ : RegularCoreHilbert ℂ) (hφ : ∀ᵐ t : ℝ, φ t ≠ 0)
    (g : RegularCoreHilbert H)
    (hg : ∀ s : ℝ, ∀ x : H,
      inner ℂ ((regularCharacterUnitary (H := H) (2 * Real.pi * s) :
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCharacterUnitary