DiagonalLocality.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Pointwise locality of operators commuting with scalar multipliers

Cutting down the operator norm inequality by every measurable indicator gives the same inequality pointwise. This is the boundedness step in constructing the diagonal field, before choosing any representatives.

theorem OAI.KadisonKastler.regular_integral_norm_sq line 23
theorem OAI.KadisonKastler.regular_setIntegral_norm_sq line 30

theorem OAI.KadisonKastler.ae_norm_apply_le_of_commute_indicators line 45

Source documentation

Commuting with all scalar projections makes the ambient operator norm a pointwise bound on every vector-valued function.

theorem ae_norm_apply_le_of_commute_indicators
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ (s : Set ℝ) (hs : MeasurableSet s),
      Commute T (regularIndicatorProjection s hs)) (f : RegularCoreHilbert H) :
    ∀ᵐ t : ℝ, ‖T f t‖ ≤ ‖T‖ * ‖f t‖ := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularIndicatorProjection

theorem OAI.KadisonKastler.commute_indicators_of_commute_scalarMultipliers line 71

Source documentation

The published diagonal-commutant hypothesis supplies exactly the indicator commutation used in the local norm argument.

theorem commute_indicators_of_commute_scalarMultipliers
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ (φ : ℝ → ℂ) (hφ : Measurable φ) (C : ℝ)
      (hC : ∀ t, ‖φ t‖ ≤ C), Commute T (regularScalarMultiplier φ hφ C hC))
    (s : Set ℝ) (hs : MeasurableSet s) :
    Commute T (regularIndicatorProjection s hs) :=
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularScalarMultiplier, OAI.KadisonKastler.regularIndicatorProjection

theorem OAI.KadisonKastler.ae_apply_eq_of_eq_of_commute_indicators line 81
Source documentation
Equal local vector values have equal local images. The exceptional set may depend on the two vectors, which suffices for a countable core.
```
theorem ae_apply_eq_of_eq_of_commute_indicators
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT : ∀ (s : Set ℝ) (hs : MeasurableSet s),
      Commute T (regularIndicatorProjection s hs)) (f g : RegularCoreHilbert H) :
    ∀ᵐ t : ℝ, f t = g t → T f t = T g t := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularIndicatorProjection
theorem OAI.KadisonKastler.ae_norm_apply_sub_le_of_commute_indicators line 95