OAI/Analysis/NuclearUltrapower/RepresentationUltraproduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearUltrapower.VariableUltra.representationSequence line 26

   Source documentation

   The bounded coordinate representation, before taking its quotient.

   def representationSequence : Γ →* unitary (operatorSeq (fun i => π i)) where
   …

   Mentions: OAI.NuclearUltrapower.VariableUltra.operatorSeq

2. def OAI.NuclearUltrapower.VariableUltra.quotientRepresentation line 51

   Source documentation

   Any unital representation of the quotient carries the source group tuple.

   def quotientRepresentation (φ : operatorQuotient (fun i => π i) ω →⋆ₐ[ℂ] (K →L[ℂ] K)) :
       Γ →* (K ≃ₗᵢ[ℂ] K) :=
   …

   Mentions: OAI.NuclearUltrapower.VariableUltra.operatorQuotient

3. theorem OAI.NuclearUltrapower.VariableUltra.quotientRepresentation_apply line 57
4. theorem OAI.NuclearUltrapower.VariableUltra.eventually_inequivalent line 63

   Source documentation

   An inequivalent sequence has at most one coordinate of any fixed type.

   theorem eventually_inequivalent
       (hω : ∀ i : ι, ({i} : Set ι) ∉ (ω : Filter ι))
       (hne : Pairwise (fun i j => ¬ (π i).Equivalent (π j)))
       (τ : FiniteUnitaryRep.{u,v} Γ) :
       ∀ᶠ i in (ω : Filter ι), ¬ τ.Equivalent (π i) := by
   …

5. theorem OAI.NuclearUltrapower.VariableUltra.inequivalent_tensor_gap line 80

   Source documentation

   The ordinary finite-dimensional tensor gap at a nonexceptional coordinate.

   theorem inequivalent_tensor_gap (P T : FiniteUnitaryRep.{u,v} Γ)
       (hP : P.Irreducible) (hT : T.Irreducible) (hne : ¬ T.Equivalent P)
       (S : Finset Γ) (κ : ℝ) (hgap : HasKazhdanGap.{u,v} S κ) :
       ∀ w : P ⊗[ℂ] StrongDual ℂ T, κ * ‖w‖ ^ 2 ≤ ∑ s ∈ S,
         ‖TensorProduct.congrIsometry (P.action s) (dualUnitary (T.action s)) w - w‖ ^ 2 := by
   …

   Mentions: OAI.NuclearUltrapower.dualUnitary

6. theorem OAI.NuclearUltrapower.VariableUltra.quotientRepresentation_weakly_mixing line 93

   Source documentation

   The varying matrix quotient has no finite-dimensional parts in any unital representation. This is the hard quotient step of nuclear-finiteness.

   theorem quotientRepresentation_weakly_mixing
       (hω : ∀ i : ι, ({i} : Set ι) ∉ (ω : Filter ι))
       (hirr : ∀ i, (π i).Irreducible)
       (hne : Pairwise (fun i j => ¬ (π i).Equivalent (π j)))
       (S : Finset Γ) (κ : ℝ) (hκ0 : 0 < κ) (hκ : κ ≤ 4 * (S.card : ℝ))
       (hgap : HasKazhdanGap.{u,v} S κ)
       (φ : operatorQuotient (fun i => π i) ω →⋆ₐ[ℂ] (K →L[ℂ] K)) :
       HasNoFiniteDimensionalSubrep (quotientRepresentation π ω φ) := by
   …

   Mentions: OAI.NuclearUltrapower.VariableUltra.operatorQuotient, OAI.NuclearUltrapower.HasNoFiniteDimensionalSubrep, OAI.NuclearUltrapower.VariableUltra.quotientRepresentation