ScalarMeanStar.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Conjugation preservation of the scalar boundary mean

Positivity preserves real sections after adding a sufficiently large constant. Applying this to the real and imaginary parts proves that the complex-linear scalar mean commutes with conjugation.

theorem OAI.KadisonKastler.scalarInfinity_norm_star_le line 23
Source documentation
Conjugating a scalar L-infinity class does not enlarge its norm.
```
theorem scalarInfinity_norm_star_le (f : ScalarLInfinity μ) : ‖star f‖ ≤ ‖f‖ := by
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.scalarInfinity_norm_star line 29
def OAI.KadisonKastler.scalarBoundaryStar line 34
Source documentation
Coordinatewise conjugation on the bounded family of scalar sections.
```
def scalarBoundaryStar (F : G →ᵇ ScalarLInfinity μ) : G →ᵇ ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.scalarBoundaryStar_apply line 40
theorem OAI.KadisonKastler.scalarBoundaryStar_ae line 43
theorem OAI.KadisonKastler.ScalarBoundaryMean.map_real line 56
Source documentation
Positivity and fixed constants imply preservation of real sections.
```
theorem map_real (F : G →ᵇ ScalarLInfinity μ)
    (hF : ∀ g, ∀ᵐ x ∂μ, (F g x).im = 0) :
    ∀ᵐ x ∂μ, (m.toCLM F x).im = 0 := by
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.ScalarBoundaryMean.map_star line 88
Source documentation
A positive complex-linear scalar boundary mean preserves conjugation.
```
theorem map_star (F : G →ᵇ ScalarLInfinity μ) :
    m.toCLM (scalarBoundaryStar F) = star (m.toCLM F) := by
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity, OAI.KadisonKastler.scalarBoundaryStar