OAI/Analysis/Cuntz/Measure.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.continuousRealInclusion line 22

   Source documentation

   Real continuous functions viewed inside the complex function algebra.

   def continuousRealInclusion : C(X, ℝ) →⋆ₐ[ℝ] C(X, ℂ) where
   …

2. theorem OAI.Kaplansky.continuousRealInclusion_apply line 31
3. theorem OAI.Kaplansky.continuous_continuousRealInclusion line 40
4. theorem OAI.Kaplansky.continuousRealInclusion_cutoff line 45
5. def OAI.Kaplansky.realFunctionHom line 63

   Source documentation

   The real function algebra mapped into the ambient finite matrix algebra.

   def realFunctionHom (ψ : C(X, ℂ) →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A) :
       C(X, ℝ) →⋆ₐ[ℝ] CStarMatrix (Fin n) (Fin n) A :=
   …

6. theorem OAI.Kaplansky.realFunctionHom_continuous line 67
7. theorem OAI.Kaplansky.realFunctionHom_cutoff line 73

   Source documentation

   Genuine CFC naturality identifies the image of a scalar cutoff.

   theorem realFunctionHom_cutoff (ψ : C(X, ℂ) →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A)
       (f : C(X, ℝ)) (hf : 0 ≤ f) (t : ℝ) :
       realFunctionHom ψ (continuousDimensionCutoff f t) = cuntzCutoff (realFunctionHom ψ f) t := by
   …

   Mentions: OAI.Kaplansky.realFunctionHom, OAI.Kaplansky.continuousDimensionCutoff, OAI.Kaplansky.cuntzCutoff

8. def OAI.Kaplansky.CuntzDimensionState.spectralMeasure line 87

   Source documentation

   The single finite Borel measure associated with a commutative representation.

   def spectralMeasure (d : CuntzDimensionState A) {n : ℕ}
       (ψ : C(X, ℂ) →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A) : Measure X :=
   …

   Mentions: OAI.Kaplansky.CuntzDimensionState

9. instance OAI.Kaplansky.CuntzDimensionState.spectralMeasure_finite line 91
10. theorem OAI.Kaplansky.CuntzDimensionState.spectralMeasure_lt line 95
11. theorem OAI.Kaplansky.CuntzDimensionState.spectralMeasure_real_lt line 115
12. theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_eq_measure_integral line 124

    Source documentation

    The original finite spectral integral equals the integral against the constructed measure. No new choice of positive functional is made.

    theorem spectralValue_eq_measure_integral (d : CuntzDimensionState A) {n : ℕ}
        (ψ : C(X, ℂ) →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A)
        (f : C(X, ℝ)) (hf : 0 ≤ f) :
        d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm (realFunctionHom ψ f), map_nonneg (realFunctionHom ψ) hf⟩ =
          ∫ x, f x ∂(d.spectralMeasure ψ) := by
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.realFunctionHom

13. theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_realFunction_add line 147

    Source documentation

    Additivity of the EXISTING spectral value on positive functions in one commutative representation, as a consequence of actual measure integration.

    theorem spectralValue_realFunction_add (d : CuntzDimensionState A) {n : ℕ}
        (ψ : C(X, ℂ) →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A)
        (f g : C(X, ℝ)) (hf : 0 ≤ f) (hg : 0 ≤ g) :
        d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm (realFunctionHom ψ (f+g)), map_nonneg (realFunctionHom ψ) (add_nonneg hf hg)⟩ =
          d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm (realFunctionHom ψ f), map_nonneg (realFunctionHom ψ) hf⟩ +
          d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm (realFunctionHom ψ g), map_nonneg (realFunctionHom ψ) hg⟩ := by
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.realFunctionHom

14. theorem OAI.Kaplansky.continuousRealInclusion_selfAdjoint line 164

    Source documentation

    All real-valued functions give self-adjoint elements, regardless of sign.

    theorem continuousRealInclusion_selfAdjoint (f : C(X, ℝ)) :
        IsSelfAdjoint (continuousRealInclusion f) := by
    …

    Mentions: OAI.Kaplansky.continuousRealInclusion

15. theorem OAI.Kaplansky.continuousRealInclusion_posPart line 170
16. theorem OAI.Kaplansky.realFunctionHom_selfAdjoint line 189
17. theorem OAI.Kaplansky.realFunctionHom_posPart line 193
18. theorem OAI.Kaplansky.realFunctionHom_negPart line 201
19. theorem OAI.Kaplansky.continuousDimensionCutoff_sub line 207
20. theorem OAI.Kaplansky.CuntzDimensionState.signedValue_eq_measure_integral line 223

    Source documentation

    The canonical signed extension agrees with the same measure on all real continuous functions, including those of mixed sign.

    theorem signedValue_eq_measure_integral (d : CuntzDimensionState A) {n : ℕ}
        (ψ : C(X, ℂ) →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A) (f : C(X, ℝ)) :
        d.signedValue (realFunctionHom ψ f) = ∫ x, f x ∂(d.spectralMeasure ψ) := by
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.realFunctionHom

21. theorem OAI.Kaplansky.CuntzDimensionState.complexValue_eq_measure_integral line 241

    Source documentation

    The globally fixed complex spectral value agrees with the same finite measure on EVERY complex continuous function in the representation.

    theorem complexValue_eq_measure_integral (d : CuntzDimensionState A) {n : ℕ}
        (ψ : C(X, ℂ) →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A) (f : C(X, ℂ)) :
        d.complexValue (ψ f) = ∫ x, f x ∂(d.spectralMeasure ψ) := by
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState

22. def OAI.Kaplansky.CuntzDimensionState.complexValueLinearMap line 264

    Source documentation

    Complex linearity for the original spectral value composed with a commutative representation. Agreement is pointwise, ensuring overlap consistency.

    def complexValueLinearMap (d : CuntzDimensionState A) {n : ℕ}
        (ψ : C(X, ℂ) →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A) : C(X, ℂ) →ₗ[ℂ] ℂ where
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState