CentralAveragingLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KadisonKastler.exists_central_mem_closed_orbit line 19
Source documentation
Geometric refinement makes the central corrections summable and produces an actual central element in the norm-closed unitary orbit hull.
```
theorem exists_central_mem_closed_orbit (x : Algebra M) :
    ∃ c : Algebra (concreteCenter M),
      c.val ∈ closure (convexHull ℝ (innerUnitaryOrbit M x.val)) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.concreteCenter, OAI.KadisonKastler.innerUnitaryOrbit
theorem OAI.KadisonKastler.publishedDixmierAveraging line 107
Source documentation
The exact published averaging input, in every represented von Neumann algebra.
```
theorem publishedDixmierAveraging (N : VonNeumannAlgebra H) : PublishedDixmierAveraging N := by
…
```
Mentions: OAI.KadisonKastler.PublishedDixmierAveraging