DiagonalMatrixNorm.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Matrix norms of the reconstructed diagonal representations

Finite L² sums are identified isometrically with tuple-valued L². The actual matrix action is pointwise under this identification, so its norm is exactly the essential supremum of the fiber matrix norms.

theorem OAI.KadisonSimilarity.pointwise_action_commutes_localization line 26

Source documentation

A genuine pointwise operator automatically commutes with all measurable localizations.

theorem pointwise_action_commutes_localization
    (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))
    (s : Set Ω) (hs : MeasurableSet s) :
    T * l2Localization μ s hs = l2Localization μ s hs * T := by
…

Mentions: OAI.KadisonSimilarity.l2Localization

theorem OAI.KadisonSimilarity.pointwise_field_norm_iff line 47

Source documentation

The field in any actual all-L² action has precisely the original operator's scalar norm bounds.

theorem pointwise_field_norm_iff
    (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))
    (C : ℝ) (hC : 0 ≤ C) :
    ‖T‖ ≤ C ↔ ∀ᵐ a ∂μ, ‖R a‖ ≤ C := by
…

theorem OAI.KadisonSimilarity.l2_matrix_action line 87

Source documentation

The transported finite matrix acts pointwise by the corresponding matrix of the actual scalar fields.

theorem l2_matrix_action {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (R : Ω → Matrix (Fin n) (Fin n) (H →L[ℂ] H))
    (hR : ∀ (i j : Fin n) (f : Lp H 2 μ),
      ∀ᵐ a ∂μ, X i j f a = R a i j (f a))
    (f : Lp (HilbertCopies H n) 2 μ) :
    ∀ᵐ a ∂μ, (l2FiniteCopiesEquiv (H := H) μ n).conjStarAlgEquiv (matrixOperator X) f a =
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.l2FiniteCopiesEquiv, OAI.KadisonSimilarity.matrixOperator

theorem OAI.KadisonSimilarity.diagonal_matrix_norm_iff line 116

Source documentation

Matrix norms are preserved exactly by the actual pointwise fields.

theorem diagonal_matrix_norm_iff {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (R : Ω → Matrix (Fin n) (Fin n) (H →L[ℂ] H))
    (hR : ∀ (i j : Fin n) (f : Lp H 2 μ),
      ∀ᵐ a ∂μ, X i j f a = R a i j (f a)) (C : ℝ) (hC : 0 ≤ C) :
    ‖matrixOperator X‖ ≤ C ↔ ∀ᵐ a ∂μ, ‖matrixOperator (R a)‖ ≤ C := by
…

Mentions: OAI.KadisonSimilarity.matrixOperator

theorem OAI.KadisonSimilarity.conull_representation_matrix_norm_iff line 133

Source documentation

The matrix norm field on a conull base is the entrywise matrix of the genuine fiber representations, with no additional matrix-norm input.

theorem conull_representation_matrix_norm_iff
    (σ : A →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (s : Set Ω) (hsm : MeasurableSet s) (hsnull : μ sᶜ = 0)
    (ρ : ∀ _a : s, A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (haction : ∀ (b : A) (f : Lp H 2 μ),
      ∀ᵐ (a : s) ∂Measure.comap ((↑) : s → Ω) μ, σ b f a = ρ a b (f a))
    {n : ℕ} (X : CStarMatrix (Fin n) (Fin n) A) (C : ℝ) (hC : 0 ≤ C) :
    ‖representedMatrix σ X‖ ≤ C ↔
      ∀ᵐ (a : s) ∂Measure.comap ((↑) : s → Ω) μ, ‖representedMatrix (ρ a) X‖ ≤ C := by
…

Mentions: OAI.KadisonSimilarity.representedMatrix

theorem OAI.KadisonSimilarity.exists_conull_diagonal_representations_with_matrices line 172

Source documentation

The constructive diagonal decomposition supplies both scalar and all finite matrix norm equivalences on the same conull family of representations.

theorem exists_conull_diagonal_representations_with_matrices
    [TopologicalSpace.SeparableSpace A]
    (σ : A →⋆ₐ[ℂ] (Lp H 2 μ →L[ℂ] Lp H 2 μ))
    (hσ : ∀ (b : A) (r : Set Ω) (hr : MeasurableSet r),
      σ b * l2Localization μ r hr = l2Localization μ r hr * σ b) :
    ∃ s : Set Ω, MeasurableSet s ∧ μ sᶜ = 0 ∧
      ∃ ρ : ∀ _a : s, A →⋆ₐ[ℂ] (H →L[ℂ] H),
        (∀ (b : A) (f : Lp H 2 μ),
          ∀ᵐ (a : s) ∂Measure.comap ((↑) : s → Ω) μ,
            σ b f a = ρ a b (f a)) ∧
        (∀ (b : A) (C : ℝ), 0 ≤ C →
          (‖σ b‖ ≤ C ↔ ∀ᵐ (a : s) ∂Measure.comap ((↑) : s → Ω) μ, ‖ρ a b‖ ≤ C)) ∧
…

Mentions: OAI.KadisonSimilarity.l2Localization