CommonFieldCompression.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compressing an actual measurable field in the common spectral model returns an operator in the original abelian commutant.

def OAI.KadisonSimilarity.commonFieldCompression line 22

Source documentation

The original operator obtained by compressing the reconstructed field.

def commonFieldCompression
    (R : WeakDual.characterSpace ℂ A → ScalarHilbertCoordinates D.generators →L[ℂ]
      ScalarHilbertCoordinates D.generators)
    (hmeas : ∀ v, AEStronglyMeasurable (fun x => R x v) (cyclicCommonBaseMeasure π D))
    (C : ℝ) (hbound : ∀ᵐ x ∂cyclicCommonBaseMeasure π D, ‖R x‖ ≤ C) : H →L[ℂ] H :=
…

Mentions: OAI.KadisonSimilarity.ScalarHilbertCoordinates, OAI.KadisonSimilarity.cyclicCommonBaseMeasure

theorem OAI.KadisonSimilarity.commonFieldCompression_eq line 32

Source documentation

Expose the compression formula without unfolding its field operator.

theorem commonFieldCompression_eq
    (R : WeakDual.characterSpace ℂ A → ScalarHilbertCoordinates D.generators →L[ℂ]
      ScalarHilbertCoordinates D.generators)
    (hmeas : ∀ v, AEStronglyMeasurable (fun x => R x v) (cyclicCommonBaseMeasure π D))
    (C : ℝ) (hbound : ∀ᵐ x ∂cyclicCommonBaseMeasure π D, ‖R x‖ ≤ C) :
    commonFieldCompression π D R hmeas C hbound =
      ((cyclicCommonEmbedding π D).toContinuousLinearMap.adjoint.comp
        (boundedFieldOperator (cyclicCommonBaseMeasure π D) R hmeas C hbound)).comp
          (cyclicCommonEmbedding π D).toContinuousLinearMap := rfl

Mentions: OAI.KadisonSimilarity.ScalarHilbertCoordinates, OAI.KadisonSimilarity.cyclicCommonBaseMeasure, OAI.KadisonSimilarity.commonFieldCompression, OAI.KadisonSimilarity.cyclicCommonEmbedding, OAI.KadisonSimilarity.boundedFieldOperator

theorem OAI.KadisonSimilarity.commonFieldCompression_mem line 42

theorem OAI.KadisonSimilarity.commonFieldCompression_mem_of_range_eq line 59

Source documentation

The same compression belongs to any representation generating this commutant.

theorem commonFieldCompression_mem_of_range_eq {B : Type*} [CStarAlgebra B]
    (σ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hgen : representationVonNeumannAlgebra σ = starSubalgebraCommutant π.range)
    (R : WeakDual.characterSpace ℂ A → ScalarHilbertCoordinates D.generators →L[ℂ]
      ScalarHilbertCoordinates D.generators)
    (hmeas : ∀ v, AEStronglyMeasurable (fun x => R x v) (cyclicCommonBaseMeasure π D))
    (C : ℝ) (hbound : ∀ᵐ x ∂cyclicCommonBaseMeasure π D, ‖R x‖ ≤ C) :
    ((cyclicCommonEmbedding π D).toContinuousLinearMap.adjoint.comp
      (boundedFieldOperator (cyclicCommonBaseMeasure π D) R hmeas C hbound)).comp
        (cyclicCommonEmbedding π D).toContinuousLinearMap ∈
      representationVonNeumannAlgebra σ := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.starSubalgebraCommutant, OAI.KadisonSimilarity.ScalarHilbertCoordinates, OAI.KadisonSimilarity.cyclicCommonBaseMeasure, OAI.KadisonSimilarity.cyclicCommonEmbedding, OAI.KadisonSimilarity.boundedFieldOperator