FiniteOrderAveraging.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Order bounds for concrete finite inner averages

def OAI.KadisonKastler.FiniteInnerAverage.linear line 20
Source documentation
The ambient average is complex linear.
```
def linear (A : FiniteInnerAverage M) : (H →L[ℂ] H) →ₗ[ℂ] (H →L[ℂ] H) where
…
```
Mentions: OAI.KadisonKastler.FiniteInnerAverage
theorem OAI.KadisonKastler.FiniteInnerAverage.apply_zero line 31
def OAI.KadisonKastler.FiniteInnerAverage.algebraApply line 35
Source documentation
The same finite average, with its value retained inside the algebra.
```
def algebraApply (A : FiniteInnerAverage M) (x : Algebra M) : Algebra M :=
…
```
Mentions: OAI.KadisonKastler.FiniteInnerAverage, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.FiniteInnerAverage.algebraApply_val line 38
theorem OAI.KadisonKastler.FiniteInnerAverage.algebraApply_sub line 48
theorem OAI.KadisonKastler.FiniteInnerAverage.apply_nonneg line 53
Source documentation
Positivity is preserved because every summand is an inner conjugate.
```
theorem apply_nonneg (A : FiniteInnerAverage M) {x : H →L[ℂ] H} (hx : 0 ≤ x) :
    0 ≤ A.apply x := by
…
```
Mentions: OAI.KadisonKastler.FiniteInnerAverage
theorem OAI.KadisonKastler.FiniteInnerAverage.apply_mono line 70

theorem OAI.KadisonKastler.FiniteInnerAverage.norm_apply_sub_scalar_le line 77

Source documentation

A scalar order interval gives a quantitative norm estimate after averaging.

theorem norm_apply_sub_scalar_le (A : FiniteInnerAverage M)
    (p q r : H →L[ℂ] H) (α β : ℝ) (hαβ : α ≤ β)
    (hqp : q ≤ p) (hpr : p ≤ r)
    (hq : A.apply q = algebraMap ℝ (H →L[ℂ] H) α)
    (hr : A.apply r = algebraMap ℝ (H →L[ℂ] H) β) :
    ‖A.apply p - algebraMap ℝ (H →L[ℂ] H) α‖ ≤ β - α := by
…

Mentions: OAI.KadisonKastler.FiniteInnerAverage

theorem OAI.KadisonKastler.FiniteInnerAverage.norm_apply_le_of_positive_interval line 94
Source documentation
A positive operator supported below a projection whose average is scalar inherits that scalar norm bound.
```
theorem norm_apply_le_of_positive_interval (A : FiniteInnerAverage M)
    (p r : H →L[ℂ] H) (β : ℝ) (hβ : 0 ≤ β) (hp : 0 ≤ p) (hpr : p ≤ r)
    (hr : A.apply r = algebraMap ℝ (H →L[ℂ] H) β) : ‖A.apply p‖ ≤ β := by
…
```
Mentions: OAI.KadisonKastler.FiniteInnerAverage