ScalarBoundaryMean.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The scalar boundary mean on actual L-infinity classes

The source is the bounded family of L-infinity sections indexed by the countable discrete group. Multiplication and nonsingular pullback are defined on the actual almost-everywhere classes. The scalar conditional-expectation property includes the module and action identities.

abbrev OAI.KadisonKastler.ScalarLInfinity line 26
def OAI.KadisonKastler.scalarInfinityConst line 29
Source documentation
Constant scalar functions as actual L-infinity classes.
```
def scalarInfinityConst (μ : Measure D) (z : ℂ) : ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.scalarInfinityConst_ae line 32
theorem OAI.KadisonKastler.scalarInfinity_ae_norm_le line 36
Source documentation
The essential norm bounds any representative almost everywhere.
```
theorem scalarInfinity_ae_norm_le (f : ScalarLInfinity μ) :
    ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖f‖ := by
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
def OAI.KadisonKastler.scalarInfinityMul line 42
Source documentation
Pointwise multiplication descends to L-infinity classes.
```
def scalarInfinityMul (f g : ScalarLInfinity μ) : ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.scalarInfinityMul_ae line 45
theorem OAI.KadisonKastler.norm_scalarInfinityMul_le line 48
theorem OAI.KadisonKastler.scalarInfinityMul_add_left line 55
theorem OAI.KadisonKastler.scalarInfinityMul_smul_left line 64
theorem OAI.KadisonKastler.scalarInfinityMul_comm line 72
theorem OAI.KadisonKastler.scalarInfinityMul_const_one line 78
theorem OAI.KadisonKastler.memLp_scalarInfinity_comp line 92
Source documentation
Nonsingular pullback preserves essential boundedness.
```
theorem memLp_scalarInfinity_comp (f : ScalarLInfinity ν) (T : D → E)
    (hT : Measure.QuasiMeasurePreserving T μ ν) : MemLp (fun x => f (T x)) ⊤ μ :=
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
def OAI.KadisonKastler.scalarInfinityPullback line 97
theorem OAI.KadisonKastler.scalarInfinityPullback_ae line 102
theorem OAI.KadisonKastler.norm_scalarInfinityPullback_le line 107
def OAI.KadisonKastler.scalarInfinityPullbackL line 116
def OAI.KadisonKastler.scalarBoundaryModule line 145
Source documentation
The scalar module action on a bounded family of L-infinity sections.
```
def scalarBoundaryModule (b : ScalarLInfinity μ) (F : G →ᵇ ScalarLInfinity μ) :
    G →ᵇ ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
def OAI.KadisonKastler.scalarBoundaryTranslate line 153
Source documentation
Simultaneous inverse translation of the group and boundary coordinates.
```
def scalarBoundaryTranslate (α : NonsingularAction G D μ) (g : G)
    (F : G →ᵇ ScalarLInfinity μ) : G →ᵇ ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.ScalarLInfinity
structure OAI.KadisonKastler.ScalarBoundaryMean line 162
Source documentation
Scalar equivariant conditional expectation in the section model of L-infinity(G × D). These are the exact structural scalar conclusions of Adams–Elliott–Giordano, Theorem 3.4; existence is not asserted here.
```
structure ScalarBoundaryMean (α : NonsingularAction G D μ) where
…
```
Mentions: OAI.KadisonKastler.NonsingularAction
theorem OAI.KadisonKastler.scalarBoundaryModule_const_one line 176
Source documentation
Multiplying the constant-one family recovers the constant family.
```
theorem scalarBoundaryModule_const_one (b : ScalarLInfinity μ) :
    scalarBoundaryModule b (BoundedContinuousFunction.const G (scalarInfinityConst μ 1)) =
      BoundedContinuousFunction.const G b := by
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity, OAI.KadisonKastler.scalarBoundaryModule, OAI.KadisonKastler.scalarInfinityConst
theorem OAI.KadisonKastler.ScalarBoundaryMean.fixed line 185
Source documentation
The scalar conditional expectation fixes all boundary sections.
```
theorem ScalarBoundaryMean.fixed {α : NonsingularAction G D μ}
    (m : ScalarBoundaryMean α) (b : ScalarLInfinity μ) :
    m.toCLM (BoundedContinuousFunction.const G b) = b := by
…
```
Mentions: OAI.KadisonKastler.NonsingularAction, OAI.KadisonKastler.ScalarBoundaryMean, OAI.KadisonKastler.ScalarLInfinity