OAI/RepresentationTheory/FiniteUnitary/Frames.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RowColumn.HilbertSchmidt.hsInner line 14

   Source documentation

   The algebraic Hilbert--Schmidt scalar product, irrespective of the operator norm on the carrier. A core is used to avoid changing any source norm.

   def hsInner (T U : E →ₗ[ℂ] E) : ℂ :=
   …

2. lemma OAI.RowColumn.HilbertSchmidt.hsInner_basis line 17
3. def OAI.RowColumn.HilbertSchmidt.endCore line 24
4. lemma OAI.RowColumn.HilbertSchmidt.adjoint_isometry line 47
5. lemma OAI.RowColumn.HilbertSchmidt.hsInner_conj line 57
6. lemma OAI.RowColumn.UnitaryFrame.norm_minimizer_unique line 78
7. theorem OAI.RowColumn.UnitaryFrame.exists_fixed_minimum line 99

   Source documentation

   Simultaneous fixed point obtained from the unique minimum-norm point of a closed convex invariant set. Applied to rank-one unitary frames, this replaces Haar integration by finite-dimensional convex averaging.

   theorem exists_fixed_minimum (K : Set E) (hne : K.Nonempty) (hclosed : IsClosed K)
       (hconv : Convex ℝ K) (L : ι → E →ₗᵢ[ℝ] E)
       (hL : ∀ i x, x ∈ K → L i x ∈ K) :
       ∃ x ∈ K, ∀ i, L i x = x := by
   …

8. def OAI.RowColumn.UnitaryFrame.quadraticForm line 122
9. lemma OAI.RowColumn.UnitaryFrame.quadraticForm_real_smul line 125
10. lemma OAI.RowColumn.UnitaryFrame.quadraticForm_continuous line 131
11. theorem OAI.RowColumn.UnitaryFrame.positive_coercive line 135

    Source documentation

    Strict positivity of a finite-dimensional frame is uniformly coercive.

    theorem positive_coercive (T : E →ₗ[ℂ] E)
        (hT : ∀ x : E, x ≠ 0 → 0 < quadraticForm T x) :
        ∃ ε : ℝ, 0 < ε ∧ ∀ x, ε * ‖x‖^2 ≤ quadraticForm T x := by
    …

    Mentions: OAI.RowColumn.UnitaryFrame.quadraticForm

12. def OAI.RowColumn.UnitaryFrame.conjugationIsometry line 177
13. def OAI.RowColumn.UnitaryFrame.conjugationReal line 181
14. lemma OAI.RowColumn.UnitaryFrame.conjugation_apply line 186
15. lemma OAI.RowColumn.UnitaryFrame.conjugation_rankOne line 189
16. def OAI.RowColumn.UnitaryFrame.matrixEntry line 198
17. def OAI.RowColumn.UnitaryFrame.quadraticEval line 203
18. def OAI.RowColumn.UnitaryFrame.coerciveSet line 210
19. lemma OAI.RowColumn.UnitaryFrame.coerciveSet_closed line 213
20. lemma OAI.RowColumn.UnitaryFrame.coerciveSet_convex line 222
21. lemma OAI.RowColumn.UnitaryFrame.positiveSet_closed line 235
22. lemma OAI.RowColumn.UnitaryFrame.positiveSet_convex line 267
23. def OAI.RowColumn.UnitaryFrame.frameHull line 274
24. lemma OAI.RowColumn.UnitaryFrame.frameHull_invariant line 278
25. lemma OAI.RowColumn.UnitaryFrame.quadraticForm_conj line 291
26. theorem OAI.RowColumn.UnitaryFrame.exists_invariant_frame_of_coercive line 301

    Source documentation

    A genuine invariant strictly positive frame is obtained by convex averaging; no Haar measure or compact-group orthogonality is taken as a hypothesis.

    theorem exists_invariant_frame_of_coercive
        (π : G →* E ≃ₗᵢ[ℂ] E) (x₀ : E)
        (T₀ : E →ₗ[ℂ] E) (hT₀ : T₀ ∈ frameHull π x₀) (hp₀ : T₀.IsPositive)
        (ε : ℝ) (_ : 0 < ε) (hε₀ : T₀ ∈ coerciveSet ε) :
        ∃ T : E →ₗ[ℂ] E, T ∈ frameHull π x₀ ∧ T.IsPositive ∧
          T ∈ coerciveSet ε ∧ ∀ g, conjugationReal (π g) T = T := by
    …

    Mentions: OAI.RowColumn.UnitaryFrame.frameHull, OAI.RowColumn.UnitaryFrame.coerciveSet, OAI.RowColumn.UnitaryFrame.conjugationReal

27. lemma OAI.RowColumn.UnitaryFrame.rankOne_quadratic line 329
28. lemma OAI.RowColumn.UnitaryFrame.finite_frame_strict line 336
29. def OAI.RowColumn.UnitaryFrame.finiteFrame line 354
30. lemma OAI.RowColumn.UnitaryFrame.finiteFrame_quadratic line 358
31. lemma OAI.RowColumn.UnitaryFrame.finiteFrame_positive line 374
32. theorem OAI.RowColumn.UnitaryFrame.exists_invariant_frame line 386

    Source documentation

    Spanning unitary orbits have an invertible positive invariant frame, with its approximation by finite probability mixtures of the original orbit.

    theorem exists_invariant_frame (π : G →* E ≃ₗᵢ[ℂ] E) (x₀ : E)
        (hspan : Submodule.span ℂ (Set.range fun g : G => π g x₀) = ⊤) :
        ∃ T : E →ₗ[ℂ] E, T ∈ frameHull π x₀ ∧ T.IsPositive ∧
          Function.Bijective T ∧ ∀ g, conjugationReal (π g) T = T := by
    …

    Mentions: OAI.RowColumn.UnitaryFrame.frameHull, OAI.RowColumn.UnitaryFrame.conjugationReal

33. theorem OAI.RowColumn.UnitaryFrame.exists_density line 447

    Source documentation

    Algebraic and convex reconstruction from a spanning unitary group. The trace is the physical trace, not the trace of the algebra's regular action.

    theorem exists_density (τ : A →ₗ[ℂ] ℂ) (core : InnerProductSpace.Core ℂ A)
        (hinner : ∀ x y, core.inner x y = τ (star x * y))
        (u : G →* unitary A)
        (hspan : Submodule.span ℂ (Set.range fun g : G => (u g : A)) = ⊤) :
        ∃ D : A, τ D = (Module.finrank ℂ A : ℂ) ∧
          (∀ x : A, 0 ≤ τ (star x * x * D)) ∧
          (∀ (B : A) (ℓ : A →ₗ[ℂ] ℂ) (R : ℝ),
            (∀ g, ‖τ (star (u g : A) * (B*D)) * ℓ (u g : A)‖ ≤ R) → ‖ℓ B‖ ≤ R) := by
    …