OAI/Analysis/KadisonKastler/VectorCoreField.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measurable operator fields from a countable vector core

Pointwise bounded rational-linear maps commuting with multiplication by i extend to complex-linear operators. Countability gives simultaneous identities off one null set; dense coefficient tests give measurability.

  1. structure OAI.KadisonKastler.CoherentVectorCore line 24
  2. def OAI.KadisonKastler.CoherentVectorCore.linearMap line 34
  3. def OAI.KadisonKastler.CoherentVectorCore.operator line 39
  4. theorem OAI.KadisonKastler.CoherentVectorCore.operator_coe line 42
  5. theorem OAI.KadisonKastler.CoherentVectorCore.norm_operator_le line 45
  6. theorem OAI.KadisonKastler.coherentVectorCore_ae line 54
  7. theorem OAI.KadisonKastler.exists_field_of_vectorCore line 70

    Source documentation

    A bounded operator field agreeing with the supplied core vectors. The bad set is assigned the zero operator.

    theorem exists_field_of_vectorCore [SeparableSpace H] (hB : 0 ≤ B)
    (hm : ∀ x, AEStronglyMeasurable (g x) volume)
    (hc : ∀ᵐ t : ℝ, CoherentVectorCore C B (fun x => g x t)) :
    ∃ F : ℝ → H →L[ℂ] H,
      (∀ ξ, AEStronglyMeasurable (fun t => F t ξ) volume) ∧
      (∀ t, ‖F t‖ ≤ B) ∧ ∀ x : C.space, (fun t => F t (x : H)) =ᵐ[volume] g x := by
…

    Mentions: OAI.KadisonKastler.CoherentVectorCore