AEColumnOperator.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Recovering fiber operators from almost-everywhere column data

The common conull set is obtained from countably many additive and i-linearity identities. The extension has the original norm bound; each fixed column agrees almost everywhere with the original data.

theorem OAI.KadisonSimilarity.ae_exists_operator_of_countable_additive line 25
theorem OAI.KadisonSimilarity.ae_columnOperator_agrees_at line 47

theorem OAI.KadisonSimilarity.exists_conull_columnOperators line 82

Source documentation

Bounded AE column data gives a genuine bounded complex-linear operator on every fiber of a measurable conull restriction.

theorem exists_conull_columnOperators
    [TopologicalSpace.SeparableSpace E] (C : ℝ≥0)
    (f : ∀ _x : E, ∀ a, K a)
    (hzero : ∀ᵐ a ∂μ, f 0 a = 0)
    (hadd : ∀ x y : E, ∀ᵐ a ∂μ, f (x + y) a = f x a + f y a)
    (hI : ∀ x : E, ∀ᵐ a ∂μ, f (Complex.I • x) a = Complex.I • f x a)
    (hnorm : ∀ x : E, ∀ᵐ a ∂μ, ‖f x a‖ ≤ C * ‖x‖) :
    ∃ s : Set Ω, MeasurableSet s ∧ μ sᶜ = 0 ∧
      ∃ T : ∀ a : s, E →L[ℂ] K a,
        (∀ a, ‖T a‖ ≤ C) ∧
        ∀ x : E, ∀ᵐ a ∂Measure.comap ((↑) : s → Ω) μ, T a x = f x a := by
…