OAI/Analysis/NuclearUltrapower/TensorMatching.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NuclearUltrapower.complex_real_card_smul line 13
2. theorem OAI.NuclearUltrapower.norm_complement_gt_of_energy_lt line 20
3. def OAI.NuclearUltrapower.matchingUnitary line 49
4. def OAI.NuclearUltrapower.matchingTuple line 54
5. theorem OAI.NuclearUltrapower.matchingUnitary_val line 59
6. def OAI.NuclearUltrapower.Matches line 65

   Source documentation

   Direct second-factor convention. Conjugating all irreducibles gives an equivalent convention with the same quantification over representation classes.

   def Matches (a : ℝ) (π : FiniteUnitaryRep.{u,v} Γ) : Prop :=
   …

7. theorem OAI.NuclearUltrapower.Matches.norm_complement line 69
8. theorem OAI.NuclearUltrapower.coordinateComplement_poly line 76
9. theorem OAI.NuclearUltrapower.coordinateComplement_apply line 87
10. def OAI.NuclearUltrapower.FiniteUnitaryRep.classSetoid line 99
11. abbrev OAI.NuclearUltrapower.RepClass line 103
12. def OAI.NuclearUltrapower.matchClasses line 105
13. theorem OAI.NuclearUltrapower.matchClasses_finite line 111

    Source documentation

    The full class-valued finiteness conclusion for an arbitrary nuclear tuple. This does not assert any group relation for the tuple.

    theorem matchClasses_finite (ω : Ultrafilter ℕ)
        (hB : IsNuclear.{v,v} B) (κ a : ℝ)
        (hS : S.Nonempty) (hκ0 : 0 < κ) (hκ : κ ≤ 4 * (S.card : ℝ))
        (hgap : HasKazhdanGap.{u,v} S κ) (ha : a < κ ^ 2 / (4 * (S.card : ℝ)))
        (hω : ∀ i : ℕ, ({i} : Set ℕ) ∉ (ω : Filter ℕ)) :
        (matchClasses ρ S u a).Finite := by
    …

    Mentions: OAI.NuclearUltrapower.matchClasses

14. theorem OAI.NuclearUltrapower.subspace_projection_intertwines line 145
15. theorem OAI.NuclearUltrapower.FiniteUnitaryRep.orthogonal_invariant line 166
16. theorem OAI.NuclearUltrapower.FiniteUnitaryRep.projection_action line 179
17. theorem OAI.NuclearUltrapower.matches_iff_homogeneous line 193

    Source documentation

    Normalized and homogeneous strict Rayleigh inequalities agree.

    theorem matches_iff_homogeneous (a : ℝ) (π : FiniteUnitaryRep.{u,v} Γ) :
        Matches ρ S u a π ↔ ∃ x : TensorHilbert E π,
          tupleEnergy S (matchingTuple ρ u π) x < a * ‖x‖^2 := by
    …

    Mentions: OAI.NuclearUltrapower.Matches, OAI.NuclearUltrapower.TensorHilbert, OAI.NuclearUltrapower.tupleEnergy, OAI.NuclearUltrapower.matchingTuple

18. theorem OAI.NuclearUltrapower.matchingTuple_toCLM line 231
19. theorem OAI.NuclearUltrapower.tensor_intertwining line 236
20. theorem OAI.NuclearUltrapower.Matches.embeds line 258
21. theorem OAI.NuclearUltrapower.Matches.equivalent line 274
22. theorem OAI.NuclearUltrapower.tensor_projection_action line 279
23. theorem OAI.NuclearUltrapower.tensor_projection_energy line 288