OAI/Analysis/KadisonKastler/FinitePhases.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.finitePhaseSum line 24
2. theorem OAI.KadisonKastler.finitePhaseSum_inner line 27
3. theorem OAI.KadisonKastler.finitePhaseSum_mean_square line 45

   Source documentation

   Parseval's identity for any finite family of orthogonal phases.

   theorem finitePhaseSum_mean_square (χ : W → Ω → ℂ)
       (hχ : ∀ i j, (𝔼 t : Ω, star (χ i t) * χ j t) = if i = j then 1 else 0)
       (v : W → H) :
       (𝔼 t : Ω, ‖finitePhaseSum χ v t‖ ^ 2) = ∑ w, ‖v w‖ ^ 2 := by
   …

   Mentions: OAI.KadisonKastler.finitePhaseSum

4. theorem OAI.KadisonKastler.additiveCharacters_orthogonal line 58

   Source documentation

   Distinct additive characters supply the required orthogonal phases.

   theorem additiveCharacters_orthogonal {G : Type*} [AddCommGroup G] [Fintype G]
       (χ : W → AddChar G ℂ) (hχ : Function.Injective χ) (i j : W) :
       (𝔼 t : G, star (χ i t) * χ j t) = if i = j then 1 else 0 := by
   …

5. theorem OAI.KadisonKastler.additiveCharacters_mean_square line 65
6. theorem OAI.KadisonKastler.finitePhaseSum_rms_le line 72

   Source documentation

   A finite orthogonal phase average preserves any coefficient-column bound, with no factor for the number of coefficients.

   theorem finitePhaseSum_rms_le (χ : W → Ω → ℂ)
       (hχ : ∀ i j, (𝔼 t : Ω, star (χ i t) * χ j t) = if i = j then 1 else 0)
       (v : W → H) {C : ℝ} (hv : ‖WithLp.toLp 2 v‖ ≤ C) :
       Real.sqrt (𝔼 t : Ω, ‖finitePhaseSum χ v t‖ ^ 2) ≤ C := by
   …

   Mentions: OAI.KadisonKastler.finitePhaseSum

7. theorem OAI.KadisonKastler.unitary_phase_coefficient_column line 81

   Source documentation

   If every phase polynomial is unitary, its coefficient column is an isometry. This proves the coefficient-column identity used before clipping.

   theorem unitary_phase_coefficient_column [CompleteSpace H] [Nonempty Ω]
       (χ : W → Ω → ℂ)
       (hχ : ∀ i j, (𝔼 t : Ω, star (χ i t) * χ j t) = if i = j then 1 else 0)
       (K : W → H →L[ℂ] H)
       (hK : ∀ t, (∑ w, χ w t • K w) ∈ unitary (H →L[ℂ] H)) (x : H) :
       ‖WithLp.toLp 2 (fun w => K w x)‖ = ‖x‖ := by
   …