DiagonalFieldAlgebra.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Algebraic laws for fields of diagonal-commuting operators

The fields are constructed from the actual operators. Their algebraic laws hold almost everywhere, by the pointwise action on all L² vectors and a countable dense family of constant columns.

theorem OAI.KadisonSimilarity.exists_global_diagonal_field line 24

Source documentation

Extending by the zero operator outside the conull reconstruction set produces a field on the original measure space.

theorem exists_global_diagonal_field
    (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, (∀ a, ‖field a‖ ≤ ‖T‖) ∧
      ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = field a (f a) := by
…

Mentions: OAI.KadisonSimilarity.l2Localization

def OAI.KadisonSimilarity.diagonalField line 49

Source documentation

A chosen genuine field for an operator in the diagonal commutant.

def diagonalField
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (hT : ∀ (r : Set Ω) (hr : MeasurableSet r),
      T * l2Localization μ r hr = l2Localization μ r hr * T) : Ω → H →L[ℂ] H :=
…

Mentions: OAI.KadisonSimilarity.l2Localization

theorem OAI.KadisonSimilarity.diagonalField_norm line 55
theorem OAI.KadisonSimilarity.diagonalField_action line 62
theorem OAI.KadisonSimilarity.ae_operator_eq_of_forall_vectors line 72
Source documentation
Countably many dense test vectors suffice for equality of operator fields almost everywhere.
```
theorem ae_operator_eq_of_forall_vectors
    (R S : Ω → H →L[ℂ] H)
    (h : ∀ x : H, ∀ᵐ a ∂μ, R a x = S a x) : ∀ᵐ a ∂μ, R a = S a := by
…
```

theorem OAI.KadisonSimilarity.pointwise_action_column line 85

Source documentation

The all-vector action supplies the constant-column formula.

theorem pointwise_action_column
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R : Ω → H →L[ℂ] H)
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a)) (x : H) :
    ∀ᵐ a ∂μ, T (Lp.const 2 μ x) a = R a x := by
…

theorem OAI.KadisonSimilarity.pointwise_field_zero line 94

Source documentation

Zero is preserved by any field realizing its pointwise action.

theorem pointwise_field_zero (R : Ω → H →L[ℂ] H)
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, (0 : Lp H 2 μ →L[ℂ] Lp H 2 μ) f a = R a (f a)) :
    ∀ᵐ a ∂μ, R a = 0 := by
…

theorem OAI.KadisonSimilarity.pointwise_field_one line 104

Source documentation

The identity is preserved almost everywhere.

theorem pointwise_field_one (R : Ω → H →L[ℂ] H)
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, (1 : Lp H 2 μ →L[ℂ] Lp H 2 μ) f a = R a (f a)) :
    ∀ᵐ a ∂μ, R a = 1 := by
…

theorem OAI.KadisonSimilarity.pointwise_field_add line 114

Source documentation

Addition of L² operators becomes addition of their fields.

theorem pointwise_field_add
    (T S : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R Q U : Ω → H →L[ℂ] H)
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hQ : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, S f a = Q a (f a))
    (hU : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, (T + S) f a = U a (f a)) :
    ∀ᵐ a ∂μ, U a = R a + Q a := by
…

theorem OAI.KadisonSimilarity.pointwise_field_mul line 129

Source documentation

Composition uses the all-L² action on the inner operator's column.

theorem pointwise_field_mul
    (T S : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R Q U : Ω → H →L[ℂ] H)
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hQ : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, S f a = Q a (f a))
    (hU : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, (T * S) f a = U a (f a)) :
    ∀ᵐ a ∂μ, U a = R a * Q a := by
…

theorem OAI.KadisonSimilarity.pointwise_field_smul line 144

Source documentation

Complex scalar multiplication, in particular multiplication by i, is inherited from the actual L² operators.

theorem pointwise_field_smul
    (c : ℂ) (T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (R U : Ω → H →L[ℂ] H)
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hU : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, (c • T) f a = U a (f a)) :
    ∀ᵐ a ∂μ, U a = c • R a := by
…