OAI/Analysis/NuclearUltrapower/InducedApproximation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearUltrapower.AlmostInvariant line 18

   Source documentation

   Pointwise approximate invariance in a varying Hilbert family.

   def AlmostInvariant (g : Γ) : Prop :=
   …

2. theorem OAI.NuclearUltrapower.displacement_product_le line 21
3. theorem OAI.NuclearUltrapower.almostInvariant_mul line 44
4. theorem OAI.NuclearUltrapower.almostInvariant_one line 59
5. theorem OAI.NuclearUltrapower.almostInvariant_inv line 69
6. theorem OAI.NuclearUltrapower.almostInvariant_of_generators line 95

   Source documentation

   A fixed finite generating set controls every fixed group element. This closure proof does not require relations at individual coordinates.

   theorem almostInvariant_of_generators (S : Finset Γ)
       (hS : Subgroup.closure (S : Set Γ) = ⊤) {C : ℝ} (hx : ∀ i, ‖x i‖ ≤ C)
       (h1 : Tendsto (fun i => ‖(U 1 i : E i →L[ℂ] E i) -
         ((1 : E i ≃ₗᵢ[ℂ] E i) : E i →L[ℂ] E i)‖) l (𝓝 0))
       (hmul : ∀ g h, Tendsto (fun i => ‖(U (g*h) i : E i →L[ℂ] E i) -
         ((U g i * U h i) : E i →L[ℂ] E i)‖) l (𝓝 0))
       (hs : ∀ s ∈ S, AlmostInvariant l U x s) (g : Γ) : AlmostInvariant l U x g := by
   …

   Mentions: OAI.NuclearUltrapower.AlmostInvariant

7. theorem OAI.NuclearUltrapower.displacement_tendsto_of_energy line 128
8. theorem OAI.NuclearUltrapower.energy_tendsto_zero line 138
9. theorem OAI.NuclearUltrapower.free_le_atTop line 151
10. theorem OAI.NuclearUltrapower.exists_almost_invariant_vectors line 159

    Source documentation

    Unit vectors with vanishing energy can be selected even while the Hilbert spaces and their dimensions vary freely.

    theorem exists_almost_invariant_vectors
        (hω : ∀ i : ℕ, ({i} : Set ℕ) ∉ (ω : Filter ℕ))
        (hd : Tendsto (fun i => bottomEnergy S (fun g => U g i)) (ω : Filter ℕ) (𝓝 0)) :
        ∃ x : ∀ i, E i, (∀ i, ‖x i‖ = 1) ∧
          Tendsto (fun i => tupleEnergy S (fun g => U g i) (x i)) (ω : Filter ℕ) (𝓝 0) := by
    …

    Mentions: OAI.NuclearUltrapower.bottomEnergy, OAI.NuclearUltrapower.tupleEnergy

11. theorem OAI.NuclearUltrapower.bottom_tendsto_zero_of_small line 174

    Source documentation

    Matching below the Kazhdan threshold forces the bottom energies to zero; this uses no common bound on the dimensions.

    theorem bottom_tendsto_zero_of_small (κ a : ℝ)
        (hgap : HasKazhdanGap.{u,v} S κ) (ha : a < κ)
        (h1 : Tendsto (fun i => ‖(U 1 i : E i →L[ℂ] E i) -
          ((1 : E i ≃ₗᵢ[ℂ] E i) : E i →L[ℂ] E i)‖) (ω : Filter ℕ) (𝓝 0))
        (hmul : ∀ g h, Tendsto (fun i => ‖(U (g*h) i : E i →L[ℂ] E i) -
          ((U g i * U h i) : E i →L[ℂ] E i)‖) (ω : Filter ℕ) (𝓝 0))
        (hm : ∀ᶠ i in (ω : Filter ℕ), bottomEnergy S (fun g => U g i) < a) :
        Tendsto (fun i => bottomEnergy S (fun g => U g i)) (ω : Filter ℕ) (𝓝 0) := by
    …

    Mentions: OAI.NuclearUltrapower.bottomEnergy

12. theorem OAI.NuclearUltrapower.tensorMapBetween_sub_left line 207
13. theorem OAI.NuclearUltrapower.tensorMapBetween_norm_le line 220
14. theorem OAI.NuclearUltrapower.tensorMapBetween_sub_norm_le line 225
15. theorem OAI.NuclearUltrapower.matchingTuple_one line 238
16. theorem OAI.NuclearUltrapower.matchingTuple_mul_defect line 249
17. def OAI.NuclearUltrapower.inducedCoordinate line 283
18. def OAI.NuclearUltrapower.representedUnitary line 286
19. theorem OAI.NuclearUltrapower.representedUnitary_toCLM line 289
20. def OAI.NuclearUltrapower.inductionTerm line 293

    Source documentation

    The fixed finite list of induced tensor coordinates.

    def inductionTerm (i : Γ ⧸ H) : TensorHilbert E α →L[ℂ] TensorHilbert E (finiteInduced H α) :=
    …

    Mentions: OAI.NuclearUltrapower.TensorHilbert, OAI.NuclearUltrapower.finiteInduced

21. def OAI.NuclearUltrapower.inductionSeed line 296
22. theorem OAI.NuclearUltrapower.inductionTerm_norm line 299
23. theorem OAI.NuclearUltrapower.identityCoordinate_comp_inclusion line 305
24. theorem OAI.NuclearUltrapower.inductionSeed_identity line 314
25. theorem OAI.NuclearUltrapower.inductionSeed_norm_ge line 335
26. theorem OAI.NuclearUltrapower.coordinate_action_comp line 347
27. theorem OAI.NuclearUltrapower.completedTensorMap_eq_between line 356
28. theorem OAI.NuclearUltrapower.inductionTerm_action_map line 361
29. theorem OAI.NuclearUltrapower.inductionTerm_action line 372
30. def OAI.NuclearUltrapower.dualAction line 396
31. theorem OAI.NuclearUltrapower.dualAction_toDual line 412
32. def OAI.NuclearUltrapower.FiniteUnitaryRep.dual line 419
33. theorem OAI.NuclearUltrapower.FiniteUnitaryRep.Irreducible.dual line 423
34. theorem OAI.NuclearUltrapower.FiniteUnitaryRep.equivalent_of_dual line 462

    Source documentation

    Contragredience is faithful on unitary equivalence classes.

    theorem equivalent_of_dual {π τ : FiniteUnitaryRep.{u,v} Γ}
        (he : π.dual.Equivalent τ.dual) : π.Equivalent τ := by
    …

35. theorem OAI.NuclearUltrapower.FiniteUnitaryRep.dual_pull line 483
36. theorem OAI.NuclearUltrapower.FiniteUnitaryRep.dual_aperiodic line 486