OAI/Analysis/KadisonSimilarity/Representation/BoundedMeasurableField.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Bounded measurable operator fields on L²

Strong measurability of each constant column suffices to apply a field to an arbitrary L² vector. An almost-everywhere uniform bound then constructs the actual bounded L² operator, with its pointwise action and localization commutation proved directly. No norm measurability of the operator field is required.

  1. theorem OAI.KadisonSimilarity.aestronglyMeasurable_field_simple line 23

    Source documentation

    Measurability of constant columns extends to simple-vector sections.

    theorem aestronglyMeasurable_field_simple
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (f : SimpleFunc Ω H) : AEStronglyMeasurable (fun a => R a (f a)) μ := by
…
  2. theorem OAI.KadisonSimilarity.aestronglyMeasurable_field_apply line 40

    Source documentation

    Only the strong operator measurability of the field is needed for applying it to a measurable vector section.

    theorem aestronglyMeasurable_field_apply
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    {f : Ω → H} (hf : AEStronglyMeasurable f μ) :
    AEStronglyMeasurable (fun a => R a (f a)) μ := by
…
  3. theorem OAI.KadisonSimilarity.boundedField_memLp line 57

    Source documentation

    An essentially bounded field sends L² sections to L² sections.

    theorem boundedField_memLp
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C) (f : Lp H 2 μ) :
    MemLp (fun a => R a (f a)) 2 μ := by
…
  4. def OAI.KadisonSimilarity.boundedFieldVector line 68

    Source documentation

    The L² section obtained by applying an essentially bounded field.

    def boundedFieldVector
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C) (f : Lp H 2 μ) : Lp H 2 μ :=
…
  5. theorem OAI.KadisonSimilarity.boundedFieldVector_ae line 74
  6. def OAI.KadisonSimilarity.boundedFieldLinear line 81
  7. theorem OAI.KadisonSimilarity.boundedFieldVector_norm_le line 104
  8. def OAI.KadisonSimilarity.boundedFieldOperator line 116

    Source documentation

    The bounded L² operator associated to an essentially bounded strongly operator measurable field.

    def boundedFieldOperator
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C) : Lp H 2 μ →L[ℂ] Lp H 2 μ :=
…
  9. theorem OAI.KadisonSimilarity.boundedFieldOperator_action line 123
  10. theorem OAI.KadisonSimilarity.boundedFieldOperator_norm_le line 130
  11. theorem OAI.KadisonSimilarity.boundedFieldOperator_eq_of_action line 138

    Source documentation

    This construction is the reverse direction of diagonal reconstruction.

    theorem boundedFieldOperator_eq_of_action
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C)
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (hT : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a)) :
    boundedFieldOperator μ R hR C hbound = T := by
…

    Mentions: OAI.KadisonSimilarity.boundedFieldOperator

  12. theorem OAI.KadisonSimilarity.boundedFieldOperator_commutes_localization line 152

    Source documentation

    Every bounded measurable field commutes with all scalar localizations.

    theorem boundedFieldOperator_commutes_localization
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C)
    (s : Set Ω) (hs : MeasurableSet s) :
    boundedFieldOperator μ R hR C hbound * l2Localization μ s hs =
      l2Localization μ s hs * boundedFieldOperator μ R hR C hbound :=
…

    Mentions: OAI.KadisonSimilarity.boundedFieldOperator, OAI.KadisonSimilarity.l2Localization

  13. theorem OAI.KadisonSimilarity.boundedFieldOperator_commutes_of_ae line 164

    Source documentation

    Pointwise commutation with an already reconstructed operator gives actual commutation of the L² operators.

    theorem boundedFieldOperator_commutes_of_ae
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C)
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (S : Ω → H →L[ℂ] H)
    (hT : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = S a (f a))
    (hcomm : ∀ᵐ a ∂μ, R a * S a = S a * R a) :
    boundedFieldOperator μ R hR C hbound * T =
      T * boundedFieldOperator μ R hR C hbound := by
…

    Mentions: OAI.KadisonSimilarity.boundedFieldOperator

  14. theorem OAI.KadisonSimilarity.boundedFieldOperator_left_support line 187

    Source documentation

    A measurable field supported on a projection gives a genuinely left-supported L² operator.

    theorem boundedFieldOperator_left_support
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C)
    (P : Lp H 2 μ →L[ℂ] Lp H 2 μ) (p : Ω → H →L[ℂ] H)
    (hP : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, P f a = p a (f a))
    (hsupport : ∀ᵐ a ∂μ, p a * R a = R a) :
    P * boundedFieldOperator μ R hR C hbound = boundedFieldOperator μ R hR C hbound := by
…

    Mentions: OAI.KadisonSimilarity.boundedFieldOperator

  15. theorem OAI.KadisonSimilarity.boundedFieldOperator_right_support line 207

    Source documentation

    Right support is also recovered from the corresponding pointwise identity, with no simultaneous null-set assumption.

    theorem boundedFieldOperator_right_support
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C)
    (P : Lp H 2 μ →L[ℂ] Lp H 2 μ) (p : Ω → H →L[ℂ] H)
    (hP : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, P f a = p a (f a))
    (hsupport : ∀ᵐ a ∂μ, R a * p a = R a) :
    boundedFieldOperator μ R hR C hbound * P = boundedFieldOperator μ R hR C hbound := by
…

    Mentions: OAI.KadisonSimilarity.boundedFieldOperator

  16. theorem OAI.KadisonSimilarity.exists_bounded_operator_of_measurable_field line 227

    Source documentation

    A bounded measurable field yields the actual localization-commuting operator required for measurable fiber selectors.

    theorem exists_bounded_operator_of_measurable_field
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C) :
    ∃ T : Lp H 2 μ →L[ℂ] Lp H 2 μ, ‖T‖ ≤ C ∧
      (∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a)) ∧
      ∀ (s : Set Ω) (hs : MeasurableSet s),
        T * l2Localization μ s hs = l2Localization μ s hs * T :=
…

    Mentions: OAI.KadisonSimilarity.l2Localization

  17. theorem OAI.KadisonSimilarity.boundedFieldOperator_norm_iff line 243

    Source documentation

    The constructed operator has exactly the essential uniform norm bounds of its pointwise field.

    theorem boundedFieldOperator_norm_iff
    (R : Ω → H →L[ℂ] H)
    (hR : ∀ x : H, AEStronglyMeasurable (fun a => R a x) μ)
    (C : ℝ) (hbound : ∀ᵐ a ∂μ, ‖R a‖ ≤ C) (c : ℝ) (hc : 0 ≤ c) :
    ‖boundedFieldOperator μ R hR C hbound‖ ≤ c ↔ ∀ᵐ a ∂μ, ‖R a‖ ≤ c :=
…

    Mentions: OAI.KadisonSimilarity.boundedFieldOperator