OAI/Analysis/FactorGeneration/SpectralDimension.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Generator.Tracial.traceFreeDimension_finsetSum line 23
2. theorem OAI.Generator.Tracial.traceFreeDimension_sum_of_total line 55
3. theorem OAI.Generator.Tracial.traceFreeDimension_spectralWeight_norm_le line 68

   Source documentation

   A finite orthogonal spectral value has the required operator-norm bound.

   theorem traceFreeDimension_spectralWeight_norm_le
       (hunit : (1 : M.toStarSubalgebra) ≠ 0)
       {I : Type*} [Fintype I] (q : I → AlgebraProjection M)
       (ho : ∀ i j, i≠j → (q i).val*(q j).val=0) (c : I → ℂ) :
       ‖∑ i, c i*(traceFreeDimension hfactor hdiff (q i) : ℂ)‖ ≤
         ‖∑ i, c i • (q i).val‖ := by
   …

   Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

4. theorem OAI.Generator.Tracial.traceFreeDimension_spectralWeight_sub_norm_le line 109

   Source documentation

   In a fixed orthogonal partition, the spectral-value map is contractive.

   theorem traceFreeDimension_spectralWeight_sub_norm_le
       (hunit : (1 : M.toStarSubalgebra) ≠ 0)
       {I : Type*} [Fintype I] (q : I → AlgebraProjection M)
       (ho : ∀ i j, i≠j → (q i).val*(q j).val=0) (c d : I → ℂ) :
       ‖(∑ i, c i*(traceFreeDimension hfactor hdiff (q i) : ℂ))-
         (∑ i, d i*(traceFreeDimension hfactor hdiff (q i) : ℂ))‖ ≤
         ‖(∑ i, c i • (q i).val)-(∑ i, d i • (q i).val)‖ := by
   …

   Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceFreeDimension

5. theorem OAI.Generator.Tracial.CornerPartition.dimension_joint_row line 126
6. theorem OAI.Generator.Tracial.CornerPartition.dimension_joint_column line 136
7. theorem OAI.Generator.Tracial.CornerPartition.dimension_weight_joint_left line 147
8. theorem OAI.Generator.Tracial.CornerPartition.dimension_weight_joint_right line 159
9. theorem OAI.Generator.Tracial.CornerPartition.dimension_weight_cross_norm_le line 172

   Source documentation

   Changing between two commuting partitions preserves the norm estimate.

   theorem dimension_weight_cross_norm_le (hunit : (1 : M.toStarSubalgebra) ≠ 0)
       (c : Fin Q.size → ℂ) (d : Fin R.size → ℂ) :
       ‖(∑ i, c i*(traceFreeDimension hfactor hdiff (Q.piece i) : ℂ))-
         (∑ j, d j*(traceFreeDimension hfactor hdiff (R.piece j) : ℂ))‖ ≤
         ‖(∑ i, c i • (Q.piece i).val)-(∑ j, d j • (R.piece j).val)‖ := by
   …

   Mentions: OAI.Generator.Tracial.traceFreeDimension

10. theorem OAI.Generator.Tracial.CornerPartition.dimension_weight_eq_of_commuting_sums_eq line 184
11. def OAI.Generator.Tracial.IsDimensionSpectralValue line 211

    Source documentation

    Approximation specification, not an assumed linear trace.

    def IsDimensionSpectralValue (x : M.toStarSubalgebra) (t : ℂ) : Prop :=
    …

12. theorem OAI.Generator.Tracial.traceFreeDimension_exists_spectral_value line 220

    Source documentation

    Actual finite spectral approximants are Cauchy in their dimension values, and their real limit controls every commuting spectral approximation.

    theorem traceFreeDimension_exists_spectral_value
        (hunit : (1 : M.toStarSubalgebra) ≠ 0)
        (x : M.toStarSubalgebra) (hx : IsSelfAdjoint x) :
        ∃ t : ℂ, t.im=0 ∧ IsDimensionSpectralValue hfactor hdiff x t := by
    …

    Mentions: OAI.Generator.Tracial.IsDimensionSpectralValue

13. theorem OAI.Generator.Tracial.IsDimensionSpectralValue.unique line 278
14. def OAI.Generator.Tracial.dimensionSpectralValue line 304

    Source documentation

    This is a constructed scalar value on self-adjoint operators; it is not yet packaged as a linear functional.

    def dimensionSpectralValue (hunit : (1 : M.toStarSubalgebra) ≠ 0)
        (x : M.toStarSubalgebra) (hx : IsSelfAdjoint x) : ℂ :=
    …

15. theorem OAI.Generator.Tracial.dimensionSpectralValue_spec line 308
16. theorem OAI.Generator.Tracial.IsDimensionSpectralValue.norm_le line 329
17. theorem OAI.Generator.Tracial.IsDimensionSpectralValue.on_projection line 335
18. theorem OAI.Generator.Tracial.dimensionSpectralValue_norm_le line 378
19. theorem OAI.Generator.Tracial.dimensionSpectralValue_projection line 383
20. theorem OAI.Generator.Tracial.dimensionSpectralValue_one line 390
21. theorem OAI.Generator.Tracial.IsDimensionSpectralValue.family_bound line 408
22. theorem OAI.Generator.Tracial.dimensionSpectralValue_eq_of_approximants line 427
23. theorem OAI.Generator.Tracial.dimensionSpectralValue_real_smul line 451
24. theorem OAI.Generator.Tracial.dimensionSpectralValue_zero line 483
25. theorem OAI.Generator.Tracial.dimensionSpectralValue_neg line 489