OAI/Analysis/FactorGeneration/UnitaryMetric.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Generator.Tracial.selfAdjointTraceBall line 19
2. theorem OAI.Generator.Tracial.selfAdjointTraceBall_closed line 22
3. theorem OAI.Generator.Tracial.selfAdjointTraceBall_convex line 40
4. theorem OAI.Generator.Tracial.exists_selfAdjoint_ball_minimum line 53
5. theorem OAI.Generator.Tracial.exists_selfAdjoint_ball_variational line 74
6. theorem OAI.Generator.Tracial.commute_of_norm₂_limit line 114
7. theorem OAI.Generator.Tracial.exists_countable_commutant_family line 130
8. structure OAI.Generator.Tracial.TraceUnitary line 162
9. def OAI.Generator.Tracial.TraceUnitary.algebra line 167
10. def OAI.Generator.Tracial.TraceUnitary.vector line 169
11. theorem OAI.Generator.Tracial.TraceUnitary.vector_injective line 171
12. instance OAI.Generator.Tracial.TraceUnitary.(instance at line 182) line 182
13. theorem OAI.Generator.Tracial.TraceUnitary.vector_isometry line 185
14. theorem OAI.Generator.Tracial.TraceUnitary.dist_eq line 187
15. theorem OAI.Generator.Tracial.TraceUnitary.algebra_norm_le line 193
16. theorem OAI.Generator.Tracial.TraceUnitary.unitary_of_limit line 196
17. theorem OAI.Generator.Tracial.TraceUnitary.vector_range_closed line 220
18. instance OAI.Generator.Tracial.TraceUnitary.(instance at line 232) line 232
19. theorem OAI.Generator.Tracial.TraceUnitary.tendsto_iff line 237

    Source documentation

    Convergence in the constructed metric is exactly trace two-norm convergence.

    theorem tendsto_iff {I : Type*} (l : Filter I) (u : I → TraceUnitary τ)
        (v : TraceUnitary τ) :
        Tendsto u l (𝓝 v) ↔ Tendsto (fun i => τ.norm₂ ((u i).algebra τ-v.algebra τ)) l (𝓝 0) := by
    …

    Mentions: OAI.Generator.Tracial.TraceUnitary, OAI.Generator.Tracial.TraceUnitary.algebra