DiagonalFiberRepresentations.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Genuine representations of the diagonal commutant

For a norm-separable C-star algebra acting on a constant-fiber L² space, commutation with measurable localizations gives genuine representations on a conull base. All raw AE algebraic relations are derived from the actual L² action. The original operator norm is recovered from the fiber norms.

theorem OAI.KadisonSimilarity.exists_conull_diagonal_star_representations line 28

Source documentation

Actual diagonal-commuting representations decompose into genuine fiber representations, with pointwise action on every L² vector and the exact scalar norm-bound equivalence.

theorem exists_conull_diagonal_star_representations
    (σ : 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) := by
…

Mentions: OAI.KadisonSimilarity.l2Localization