DiagonalOperatorField.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The field of a diagonal-commuting L² operator

An operator commuting with every measurable localization has bounded constant-vector columns. Those actual columns determine a field of bounded operators on a measurable conull subset of the base, without any additional pointwise linearity assumption.

theorem OAI.KadisonSimilarity.exists_conull_diagonal_operator_field line 26

Source documentation

Reconstruct the pointwise operator from its actual constant-vector columns. Each fixed column is preserved almost everywhere.

theorem exists_conull_diagonal_operator_field
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (hT : ∀ (r : Set Ω) (hr : MeasurableSet r),
      T * l2Localization μ r hr = l2Localization μ r hr * T) :
    ∃ s : Set Ω, MeasurableSet s ∧ μ sᶜ = 0 ∧
      ∃ field : ∀ _a : s, H →L[ℂ] H,
        (∀ a, ‖field a‖ ≤ ‖T‖) ∧
        ∀ x : H, ∀ᵐ a ∂Measure.comap ((↑) : s → Ω) μ,
          field a x = T (Lp.const 2 μ x) a := by
…

Mentions: OAI.KadisonSimilarity.l2Localization