OAI/Analysis/Cuntz/Commutative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.CuntzDimensionState.continuousDimension line 20

   Source documentation

   Transport the existing regularized dimension through a real star algebra homomorphism. On negative functions the auxiliary value is zero and is unused.

   def CuntzDimensionState.continuousDimension (d : CuntzDimensionState A) {n : ℕ}
       (φ : C(X, ℝ) →⋆ₐ[ℝ] CStarMatrix (Fin n) (Fin n) A) : PositiveDimensionFunctional X where
   …

   Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.PositiveDimensionFunctional

2. theorem OAI.Kaplansky.CuntzDimensionState.continuousDimension_apply line 35
3. def OAI.Kaplansky.CuntzDimensionState.commutativeContent line 42

   Source documentation

   A compact content constructed from the SAME ambient dimension state.

   def CuntzDimensionState.commutativeContent (d : CuntzDimensionState A) [NormalSpace X] {n : ℕ}
       (φ : C(X, ℝ) →⋆ₐ[ℝ] CStarMatrix (Fin n) (Fin n) A) : MeasureTheory.Content X :=
   …

   Mentions: OAI.Kaplansky.CuntzDimensionState

4. theorem OAI.Kaplansky.CuntzDimensionState.continuousDimension_one line 46
5. theorem OAI.Kaplansky.CuntzDimensionState.continuousDimension_scaleInvariant line 67
6. theorem OAI.Kaplansky.CuntzDimensionState.continuousDimension_lowerSemicontinuous line 78
7. theorem OAI.Kaplansky.CuntzDimensionState.continuousDimension_measure_positive_support line 97

   Source documentation

   The measure of a positive support is the actual regularized ambient Cuntz dimension of its image, with no functional or measure-existence premise.

   theorem continuousDimension_measure_positive_support (d : CuntzDimensionState A) {n : ℕ}
       (φ : C(X, ℝ) →⋆ₐ[ℝ] CStarMatrix (Fin n) (Fin n) A) (hφ : Continuous φ)
       (f : C(X, ℝ)) (hf : 0 ≤ f) :
       (d.continuousDimension φ).measure {x | 0 < f x} =
         ENNReal.ofReal (d.regularized ⟨n, CStarMatrix.ofMatrix.symm (φ f), map_nonneg φ hf⟩) := by
   …

   Mentions: OAI.Kaplansky.CuntzDimensionState