OAI/Analysis/NuclearUltrapower/PullbackMatching.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NuclearUltrapower.vectors_of_small_energies line 18
2. theorem OAI.NuclearUltrapower.matchingTuple_defects line 51
3. theorem OAI.NuclearUltrapower.matchingTuple_identity line 69
4. theorem OAI.NuclearUltrapower.matched_vectors line 84

   Source documentation

   A sequence of matched representations admits unit vectors invariant under EVERY fixed group element in the ultralimit; dimensions are still unrestricted.

   theorem matched_vectors (κ a : ℝ) (hgap : HasKazhdanGap.{u,v} S κ)
       (hS : Subgroup.closure (S : Set Γ) = ⊤) (ha : a < κ)
       (hω : ∀ n : ℕ, ({n} : Set ℕ) ∉ (ω : Filter ℕ))
       (h1 : ∀ n, u 1 n = 1)
       (hmul : ∀ g h, Tendsto (fun n => ‖(u (g*h) n : B) - (u g n : B)*(u h n : B)‖)
         (ω : Filter ℕ) (𝓝 0))
       (hm : ∀ᶠ n in (ω : Filter ℕ), Matches ρ S (fun g => u g n) a (π n)) :
       ∃ ξ : ∀ n, TensorHilbert E (π n), (∀ n, ‖ξ n‖ = 1) ∧
         ∀ g, Tendsto (fun n => ‖matchingTuple ρ (fun g => u g n) (π n) g (ξ n) - ξ n‖)
           (ω : Filter ℕ) (𝓝 0) := by
   …

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

5. theorem OAI.NuclearUltrapower.tensor_covariance_bound line 122

   Source documentation

   Quantitative tensor covariance; the two fixed coordinate maps are isometries.

   theorem tensor_covariance_bound (U W : E →L[ℂ] E) (V : E →ₗᵢ[ℂ] E)
       (A : F →ₗᵢ[ℂ] F) (J : F →ₗᵢ[ℂ] F') (x : TensorHilbert E F) :
       ‖tensorMapBetween U (J.comp A).toContinuousLinearMap x -
           tensorMapBetween V.toContinuousLinearMap J.toContinuousLinearMap x‖ ≤
         ‖U - V.toContinuousLinearMap * W‖ * ‖x‖ +
           ‖tensorMapBetween W A.toContinuousLinearMap x - x‖ := by
   …

   Mentions: OAI.NuclearUltrapower.TensorHilbert, OAI.NuclearUltrapower.tensorMapBetween

6. theorem OAI.NuclearUltrapower.represented_product_defect line 160
7. def OAI.NuclearUltrapower.FiniteUnitaryRep.comap line 186

   Source documentation

   Pullback along an arbitrary group homomorphism, retaining the Hilbert space.

   def comap (π : FiniteUnitaryRep.{u,v} Γ) (f : Λ →* Γ) : FiniteUnitaryRep.{w,v} Λ :=
   …

8. theorem OAI.NuclearUltrapower.FiniteUnitaryRep.comap_action line 189
9. theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Irreducible.comap line 192
10. theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Embeds.comap line 200
11. def OAI.NuclearUltrapower.rangeTwist line 209
12. theorem OAI.NuclearUltrapower.rangeTwist_irreducible line 212
13. theorem OAI.NuclearUltrapower.rangeTwist_action line 216
14. theorem OAI.NuclearUltrapower.frobenius_predecessor line 221
15. def OAI.NuclearUltrapower.rangeTwistInclusion line 250
16. def OAI.NuclearUltrapower.shiftVector line 254

    Source documentation

    Translation of a tensor vector by the stable-letter coordinate.

    def shiftVector (π : FiniteUnitaryRep.{u,u} Γ) (b : unitary B) :
        TensorHilbert E π →ₗᵢ[ℂ] TensorHilbert E (rangeTwist θ hθ π) :=
    …

    Mentions: OAI.NuclearUltrapower.TensorHilbert, OAI.NuclearUltrapower.rangeTwist

17. theorem OAI.NuclearUltrapower.shiftVector_action_map line 258
18. theorem OAI.NuclearUltrapower.shiftVector_displacement line 277
19. theorem OAI.NuclearUltrapower.inductionTerm_displacement line 314
20. theorem OAI.NuclearUltrapower.inductionSeed_displacement line 331
21. theorem OAI.NuclearUltrapower.inductionSeed_almostInvariant line 352
22. theorem OAI.NuclearUltrapower.Matches.exists_irreducible line 391