ScalarMeanLocality.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Locality and countable gluing for the scalar boundary mean

Indicator sections turn the module identity into equality on a measurable cell. Countable cells can then be glued without interchanging any infinite sum with the mean.

def OAI.KadisonKastler.scalarInfinityIndicator line 23
Source documentation
The scalar characteristic function of a measurable set.
```
def scalarInfinityIndicator (s : Set D) (hs : MeasurableSet s) : ScalarLInfinity μ :=
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.scalarInfinityIndicator_ae line 26
theorem OAI.KadisonKastler.scalarInfinity_indicator_mul_eq_iff line 31
Source documentation
Multiplication by an indicator detects exactly equality on its cell.
```
theorem scalarInfinity_indicator_mul_eq_iff (s : Set D) (hs : MeasurableSet s)
    (f g : ScalarLInfinity μ) :
    scalarInfinityMul (scalarInfinityIndicator s hs) f =
        scalarInfinityMul (scalarInfinityIndicator s hs) g ↔
      f =ᵐ[μ.restrict s] g := by
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity, OAI.KadisonKastler.scalarInfinityMul, OAI.KadisonKastler.scalarInfinityIndicator
theorem OAI.KadisonKastler.aestronglyMeasurable_scalarInfinity_glue line 64
Source documentation
A scalar field selected from countably many L-infinity sections is measurable when every selection fiber is measurable.
```
theorem aestronglyMeasurable_scalarInfinity_glue (a : D → ι)
    (ha : ∀ i, MeasurableSet {x | a x = i}) (f : ι → ScalarLInfinity μ) :
    AEStronglyMeasurable (fun x => f (a x) x) μ := by
…
```
Mentions: OAI.KadisonKastler.ScalarLInfinity
theorem OAI.KadisonKastler.scalarInfinity_glue_ae_bound line 82

def OAI.KadisonKastler.scalarInfinityGlue line 91

Source documentation

An actual L-infinity section obtained by bounded countable gluing.

def scalarInfinityGlue (a : D → ι) (ha : ∀ i, MeasurableSet {x | a x = i})
    (f : ι → ScalarLInfinity μ) (C : ℝ) (hC : ∀ i, ‖f i‖ ≤ C) : ScalarLInfinity μ :=
…

Mentions: OAI.KadisonKastler.ScalarLInfinity

theorem OAI.KadisonKastler.scalarInfinityGlue_ae line 97
theorem OAI.KadisonKastler.scalarInfinityGlue_restrict line 102
theorem OAI.KadisonKastler.norm_scalarInfinityGlue_le line 111

theorem OAI.KadisonKastler.ScalarBoundaryMean.locality line 131

Source documentation

The scalar mean is local on every measurable boundary cell.

theorem locality (s : Set D) (hs : MeasurableSet s)
    (F K : G →ᵇ ScalarLInfinity μ) (hFK : ∀ g, F g =ᵐ[μ.restrict s] K g) :
    m.toCLM F =ᵐ[μ.restrict s] m.toCLM K := by
…

Mentions: OAI.KadisonKastler.ScalarLInfinity

theorem OAI.KadisonKastler.ScalarBoundaryMean.local_models line 142

Source documentation

Equality of local models for the input transfers to every output cell.

theorem local_models {ι : Type*} (s : ι → Set D) (hs : ∀ i, MeasurableSet (s i))
    (F : G →ᵇ ScalarLInfinity μ) (K : ι → G →ᵇ ScalarLInfinity μ)
    (hFK : ∀ i g, F g =ᵐ[μ.restrict (s i)] K i g) :
    ∀ i, m.toCLM F =ᵐ[μ.restrict (s i)] m.toCLM (K i) :=
…

Mentions: OAI.KadisonKastler.ScalarLInfinity

theorem OAI.KadisonKastler.ScalarBoundaryMean.eq_of_countable_local_models line 149

Source documentation

A countable measurable cover determines the mean from its local models.

theorem eq_of_countable_local_models {ι : Type*} [Countable ι]
    (s : ι → Set D) (hs : ∀ i, MeasurableSet (s i))
    (hcover : ∀ᵐ x ∂μ, ∃ i, x ∈ s i)
    (F : G →ᵇ ScalarLInfinity μ) (K : ι → G →ᵇ ScalarLInfinity μ)
    (hFK : ∀ i g, F g =ᵐ[μ.restrict (s i)] K i g)
    (b : ScalarLInfinity μ) (hb : ∀ i, b =ᵐ[μ.restrict (s i)] m.toCLM (K i)) :
    m.toCLM F = b := by
…

Mentions: OAI.KadisonKastler.ScalarLInfinity

theorem OAI.KadisonKastler.ScalarBoundaryMean.map_countable_glue line 166

Source documentation

The mean commutes with selecting uniformly bounded local models on the fibers of a countably valued measurable boundary function.

theorem map_countable_glue {ι : Type*} [Countable ι]
    (a : D → ι) (ha : ∀ i, MeasurableSet {x | a x = i})
    (F : G →ᵇ ScalarLInfinity μ) (K : ι → G →ᵇ ScalarLInfinity μ)
    (hFK : ∀ i g, F g =ᵐ[μ.restrict {x | a x = i}] K i g)
    (C : ℝ) (hC : ∀ i, ‖K i‖ ≤ C) :
    m.toCLM F = scalarInfinityGlue a ha (fun i => m.toCLM (K i)) C
      (fun i => (m.norm_le (K i)).trans (hC i)) := by
…

Mentions: OAI.KadisonKastler.ScalarLInfinity, OAI.KadisonKastler.scalarInfinityGlue