ProbabilityMatrixDistance.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Distance to an algebra after vector integration

Diagonal amplification commutes with the actual vector integral. Applying the published complete commutant-distance bound to the commutant gives an algebra approximation without choosing measurable nearest points.

theorem OAI.KadisonKastler.diagonalOperator_vector_measurable line 33

Source documentation

Finite diagonal amplification preserves vector measurability.

theorem diagonalOperator_vector_measurable
    (μ : Measure S) (F : S → H →L[ℂ] H)
    (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) μ) (n : ℕ) :
    ∀ x : Generator.FiniteHilbert (Fin n) H,
      AEStronglyMeasurable (fun s => Generator.diagonalOperator (F s) x) μ := by
…

Mentions: OAI.Generator.FiniteHilbert, OAI.Generator.diagonalOperator

theorem OAI.KadisonKastler.norm_diagonalOperator_le line 49
theorem OAI.KadisonKastler.probabilityOperatorIntegral_diagonal line 54

theorem OAI.KadisonKastler.diagonal_commutes_commutant_matrix line 75

Source documentation

A matrix over the commutant commutes with each diagonal element of the algebra.

theorem diagonal_commutes_commutant_matrix (M : VonNeumannAlgebra H)
    (b : H →L[ℂ] H) (hb : b ∈ M) (n : ℕ)
    (X : CStarMatrix (Fin n) (Fin n) (Algebra M.commutant)) :
    Generator.diagonalOperator b * matrixOperatorHom M.commutant X =
      matrixOperatorHom M.commutant X * Generator.diagonalOperator b := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.Generator.diagonalOperator, OAI.KadisonKastler.matrixOperatorHom

theorem OAI.KadisonKastler.probabilityOperatorIntegral_complete_commutant_bound line 98

Source documentation

Pointwise algebra distance bounds pass to a complete commutator bound for the integral against the algebra's commutant.

theorem probabilityOperatorIntegral_complete_commutant_bound
    (μ : Measure S) [IsProbabilityMeasure μ]
    (F : S → H →L[ℂ] H) (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) μ)
    (C : ℝ) (hC : ∀ᵐ s ∂μ, ‖F s‖ ≤ C)
    (M : VonNeumannAlgebra H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hnear : ∀ᵐ s ∂μ, ∃ b : H →L[ℂ] H, b ∈ M ∧ ‖F s - b‖ ≤ δ) :
    CompletelyBoundedBy
      ((innerDerivation (probabilityOperatorIntegral μ F hF C hC)).comp
        M.commutant.toStarSubalgebra.subtype.toLinearMap) (2 * δ) := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.innerDerivation, OAI.KadisonKastler.probabilityOperatorIntegral

theorem OAI.KadisonKastler.exists_algebra_approximation_probabilityOperatorIntegral line 134

Source documentation

The published complete commutant-distance theorem supplies the needed algebra distance after integration, without any measurable selection.

theorem exists_algebra_approximation_probabilityOperatorIntegral
    (μ : Measure S) [IsProbabilityMeasure μ]
    (F : S → H →L[ℂ] H) (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) μ)
    (C : ℝ) (hC : ∀ᵐ s ∂μ, ‖F s‖ ≤ C)
    (M : VonNeumannAlgebra H)
    (hDistance : PublishedBlockCommutantApproximation (Algebra M.commutant) H)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (hnear : ∀ᵐ s ∂μ, ∃ b : H →L[ℂ] H, b ∈ M ∧ ‖F s - b‖ ≤ δ)
    (r : ℝ) (hr : δ < r) :
    ∃ b : H →L[ℂ] H, b ∈ M ∧
      ‖probabilityOperatorIntegral μ F hF C hC - b‖ < r := by
…

Mentions: OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.probabilityOperatorIntegral

theorem OAI.KadisonKastler.infDist_probabilityOperatorIntegral_le line 152

Source documentation

Algebra distance is not increased by the vectorwise probability integral.

theorem infDist_probabilityOperatorIntegral_le
    (μ : Measure S) [IsProbabilityMeasure μ]
    (F : S → H →L[ℂ] H) (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) μ)
    (C : ℝ) (hC : ∀ᵐ s ∂μ, ‖F s‖ ≤ C)
    (M : VonNeumannAlgebra H)
    (hDistance : PublishedBlockCommutantApproximation (Algebra M.commutant) H)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (hnear : ∀ᵐ s ∂μ, Metric.infDist (F s) (M : Set (H →L[ℂ] H)) ≤ δ) :
    Metric.infDist (probabilityOperatorIntegral μ F hF C hC)
      (M : Set (H →L[ℂ] H)) ≤ δ := by
…

Mentions: OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.probabilityOperatorIntegral

theorem OAI.KadisonKastler.infDist_measurablePoissonAverage_le line 177

Source documentation

The positive Poisson kernel retains an essential algebra-distance bound at every point above the real axis.

theorem infDist_measurablePoissonAverage_le
    (F : ℝ → H →L[ℂ] H)
    (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) volume)
    (C : ℝ) (hC : ∀ᵐ s, ‖F s‖ ≤ C)
    (M : VonNeumannAlgebra H)
    (hDistance : PublishedBlockCommutantApproximation (Algebra M.commutant) H)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (hnear : ∀ᵐ s, Metric.infDist (F s) (M : Set (H →L[ℂ] H)) ≤ δ)
    (t r : ℝ) (hr : 0 < r) :
    Metric.infDist (measurablePoissonAverage F hF C hC t r hr)
      (M : Set (H →L[ℂ] H)) ≤ δ :=
…

Mentions: OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.measurablePoissonAverage

theorem OAI.KadisonKastler.infDist_smul_algebra line 192

Source documentation

Scalar multiplication scales distance to the concrete complex algebra.

theorem infDist_smul_algebra (M : VonNeumannAlgebra H) (z : ℂ)
    (T : H →L[ℂ] H) :
    Metric.infDist (z • T) (M : Set (H →L[ℂ] H)) =
      ‖z‖ * Metric.infDist T (M : Set (H →L[ℂ] H)) := by
…