DiagonalFieldAction.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Pointwise action on all L² vectors

The field reconstructed from constant columns acts pointwise on arbitrary L² vectors. Indicator constants give a dense class; two successive AE subsequences prove that the pointwise-action identity is norm closed.

theorem OAI.KadisonSimilarity.isClosed_pointwise_operator_action line 26
Source documentation
Pointwise action by any family of continuous operators is a closed condition on L² vectors for a fixed bounded operator.
```
theorem isClosed_pointwise_operator_action
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (field : Ω → H →L[ℂ] H) :
    IsClosed {f : Lp H 2 μ | ∀ᵐ a ∂μ, T f a = field a (f a)} := by
…
```

theorem OAI.KadisonSimilarity.aestronglyMeasurable_of_pointwise_operator_action line 50

Source documentation

Measurability of the field acting on a section follows from its actual L² operator action, so it is not an extra input to the construction.

theorem aestronglyMeasurable_of_pointwise_operator_action
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (field : Ω → H →L[ℂ] H) (f : Lp H 2 μ)
    (h : ∀ᵐ a ∂μ, T f a = field a (f a)) :
    AEStronglyMeasurable (fun a => field a (f a)) μ :=
…

theorem OAI.KadisonSimilarity.diagonal_operator_action_of_columns line 59

Source documentation

Commutation with diagonal localizations extends the constant-column formula to every L² vector.

theorem diagonal_operator_action_of_columns
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (hT : ∀ (r : Set Ω) (hr : MeasurableSet r),
      T * l2Localization μ r hr = l2Localization μ r hr * T)
    (field : Ω → H →L[ℂ] H)
    (hcolumns : ∀ x : H, ∀ᵐ a ∂μ, T (Lp.const 2 μ x) a = field a x)
    (f : Lp H 2 μ) : ∀ᵐ a ∂μ, T f a = field a (f a) := by
…

Mentions: OAI.KadisonSimilarity.l2Localization

theorem OAI.KadisonSimilarity.exists_conull_diagonal_field_action line 93

Source documentation

The actual field of a diagonal-commuting operator, with the complete pointwise-action formula on all L² vectors.

theorem exists_conull_diagonal_field_action
    (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‖) ∧
        ∀ f : Lp H 2 μ, ∀ᵐ (a : s) ∂Measure.comap ((↑) : s → Ω) μ,
          T f a = field a (f a) := by
…

Mentions: OAI.KadisonSimilarity.l2Localization

theorem OAI.KadisonSimilarity.norm_le_of_conull_pointwise_action line 124

Source documentation

An AE norm bound on a conull pointwise field bounds the original L² operator. This proves the converse direction of the essential-norm formula.

theorem norm_le_of_conull_pointwise_action
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (s : Set Ω) (hsm : MeasurableSet s) (hsnull : μ sᶜ = 0)
    (field : ∀ _a : s, H →L[ℂ] H)
    (haction : ∀ f : Lp H 2 μ, ∀ᵐ (a : s) ∂Measure.comap ((↑) : s → Ω) μ,
      T f a = field a (f a))
    (C : ℝ) (hC : 0 ≤ C)
    (hbound : ∀ᵐ (a : s) ∂Measure.comap ((↑) : s → Ω) μ, ‖field a‖ ≤ C) : ‖T‖ ≤ C := by
…

theorem OAI.KadisonSimilarity.exists_diagonal_field_with_norm_iff line 157

Source documentation

A diagonal-commuting operator has a genuine field with both the pointwise-action identity and the exact scalar norm-bound equivalence.

theorem exists_diagonal_field_with_norm_iff
    (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,
        (∀ f : Lp H 2 μ, ∀ᵐ (a : s) ∂Measure.comap ((↑) : s → Ω) μ,
          T f a = field a (f a)) ∧
        ∀ C : ℝ, 0 ≤ C →
          (‖T‖ ≤ C ↔ ∀ᵐ (a : s) ∂Measure.comap ((↑) : s → Ω) μ, ‖field a‖ ≤ C) := by
…

Mentions: OAI.KadisonSimilarity.l2Localization