DiagonalFieldAdjoint.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Adjoint compatibility of the actual diagonal field

Localized inner products recover the adjoint identity almost everywhere. Together with the algebraic laws, this supplies the raw AE relations needed for the conull fiber-representation construction.

theorem OAI.KadisonSimilarity.l2Localization_inner line 24
Source documentation
A measurable localization is symmetric for the L² inner product.
```
theorem l2Localization_inner (s : Set Ω) (hs : MeasurableSet s)
    (f g : Lp H 2 μ) :
    inner ℂ (l2Localization μ s hs f) g = inner ℂ f (l2Localization μ s hs g) := by
…
```
Mentions: OAI.KadisonSimilarity.l2Localization

theorem OAI.KadisonSimilarity.inner_indicatorConstLp_right line 38

Source documentation

The right-indicator version of the standard L² set-integral formula.

theorem inner_indicatorConstLp_right (f : Lp H 2 μ)
    (s : Set Ω) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (y : H) :
    inner ℂ f (indicatorConstLp 2 hs hμs y) = ∫ a in s, inner ℂ (f a) y ∂μ := by
…

theorem OAI.KadisonSimilarity.diagonal_adjoint_columns line 54

Source documentation

Equality of all localized inner products identifies adjoint constant columns almost everywhere.

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

Mentions: OAI.KadisonSimilarity.l2Localization

theorem OAI.KadisonSimilarity.pointwise_field_star line 93

Source documentation

Adjoint compatibility follows from the original operator's localized inner products, rather than being postulated as a field relation.

theorem pointwise_field_star
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (hT : ∀ (r : Set Ω) (hr : MeasurableSet r),
      T * l2Localization μ r hr = l2Localization μ r hr * T)
    (R Q : Ω → H →L[ℂ] H)
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hQ : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, (star T) f a = Q a (f a)) :
    ∀ᵐ a ∂μ, Q a = star (R a) := by
…

Mentions: OAI.KadisonSimilarity.l2Localization

theorem OAI.KadisonSimilarity.exists_diagonal_subalgebra_fields line 125

Source documentation

A star subalgebra of the diagonal commutant has actual bounded fields whose raw algebraic relations all hold almost everywhere. Each fixed operator also has its full pointwise L²-action formula.

theorem exists_diagonal_subalgebra_fields
    (P : StarSubalgebra ℂ (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (hP : ∀ (T : P) (r : Set Ω) (hr : MeasurableSet r),
      (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) * l2Localization μ r hr =
        l2Localization μ r hr * (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)) :
    ∃ field : P → Ω → H →L[ℂ] H,
      (∀ T a, ‖field T a‖ ≤ ‖T‖) ∧
      (∀ (T : P) (f : Lp H 2 μ), ∀ᵐ a ∂μ, T.val f a = field T a (f a)) ∧
      (∀ᵐ a ∂μ, field 0 a = 0) ∧
      (∀ᵐ a ∂μ, field 1 a = 1) ∧
      (∀ T S : P, ∀ᵐ a ∂μ, field (T + S) a = field T a + field S a) ∧
      (∀ T S : P, ∀ᵐ a ∂μ, field (T * S) a = field T a * field S a) ∧
…

Mentions: OAI.KadisonSimilarity.l2Localization