FiniteCentralAveraging.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Arbitrarily accurate finite averages toward the center

def OAI.KadisonKastler.FiniteInnerAverage.identity line 21
Source documentation
The one-term average.
```
def identity (M : VonNeumannAlgebra H) : FiniteInnerAverage M where
…
```
Mentions: OAI.KadisonKastler.FiniteInnerAverage
theorem OAI.KadisonKastler.FiniteInnerAverage.identity_apply line 27
theorem OAI.KadisonKastler.FiniteInnerAverage.apply_central line 37
Source documentation
Every inner average fixes every central element.
```
theorem apply_central (A : FiniteInnerAverage M) (z : Algebra (concreteCenter M)) :
    A.apply z.val = z.val := by
…
```
Mentions: OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.concreteCenter
def OAI.KadisonKastler.centralInclusion line 56
Source documentation
The concrete center included in the original algebra.
```
def centralInclusion : Algebra (concreteCenter M) →⋆ₐ[ℂ] Algebra M :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.concreteCenter

theorem OAI.KadisonKastler.exists_selfAdjoint_central_average_power line 60

Source documentation

Iteration of the uniform contraction gives a geometric error estimate.

theorem exists_selfAdjoint_central_average_power [Nontrivial H]
    (x : Algebra M) (hx : IsSelfAdjoint x) (n : ℕ) :
    ∃ (A : FiniteInnerAverage M) (c : Algebra (concreteCenter M)),
      IsSelfAdjoint c ∧ ‖A.apply x.val - c.val‖ ≤ (3 / 4 : ℝ)^n * ‖x‖ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.concreteCenter

theorem OAI.KadisonKastler.exists_selfAdjoint_central_average line 90
Source documentation
Self-adjoint elements have finite averages arbitrarily close to the center.
```
theorem exists_selfAdjoint_central_average [Nontrivial H]
    (x : Algebra M) (hx : IsSelfAdjoint x) (ε : ℝ) (hε : 0 < ε) :
    ∃ (A : FiniteInnerAverage M) (c : Algebra (concreteCenter M)),
      IsSelfAdjoint c ∧ ‖A.apply x.val - c.val‖ < ε := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.concreteCenter
theorem OAI.KadisonKastler.exists_central_average line 103
Source documentation
Two successive self-adjoint averages handle every element of the algebra.
```
theorem exists_central_average [Nontrivial H] (x : Algebra M) (ε : ℝ) (hε : 0 < ε) :
    ∃ (A : FiniteInnerAverage M) (c : Algebra (concreteCenter M)),
      ‖A.apply x.val - c.val‖ < ε := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.concreteCenter