OAI/Analysis/FactorGeneration/LocalQuantization.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

An actual irreducible subalgebra and its constructed conditional expectation give finite pinching partitions with energy arbitrarily close to the expectation energy. No partition or expectation is supplied.

  1. theorem OAI.Generator.Tracial.exists_expectation_energy_partition line 18
  2. theorem OAI.Generator.Tracial.exists_decreasing_centered_pinching_partition line 54
  3. theorem OAI.Generator.Tracial.exists_decreasing_scalar_pinching_partition line 75

    Source documentation

    Center arbitrary elements by their actual scalar trace before selecting one partition for the whole finite family.

    theorem exists_decreasing_scalar_pinching_partition (A : ℕ → VonNeumannAlgebra H)
    (hAM : ∀ n,A n ≤ M) (hA : Antitone A)
    (hirr : ∀ n,∀ c : M.toStarSubalgebra,
      (∀ a : insideAlgebra (M := M) (P := A n),
…

    Mentions: OAI.Generator.Tracial.insideAlgebra

  4. def OAI.Generator.Tracial.CornerPartition.restrictPiece line 118
  5. theorem OAI.Generator.Tracial.CornerPartition.restrictPiece_le line 121
  6. def OAI.Generator.Tracial.CornerPartition.restrictTo line 125
  7. theorem OAI.Generator.Tracial.CornerPartition.restrictTo_mem line 135
  8. theorem OAI.Generator.Tracial.CornerPartition.restrictTo_pinch line 140
  9. theorem OAI.Generator.Tracial.CornerPartition.restrictTo_pinch_of_supported line 152
  10. def OAI.Generator.Tracial.CornerPartition.splitUnit line 158

    Source documentation

    The binary partition selecting p and its complement.

    def splitUnit (p : AlgebraProjection M) : CornerPartition (identityProjection M) :=
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.CornerPartition, OAI.Generator.Tracial.identityProjection

  11. theorem OAI.Generator.Tracial.CornerPartition.splitUnit_mem line 161
  12. theorem OAI.Generator.Tracial.CornerPartition.refines_splitUnit_commutes line 171
  13. def OAI.Generator.Tracial.CornerPartition.completionPiece line 206
  14. theorem OAI.Generator.Tracial.CornerPartition.completionPiece_orthogonal line 209
  15. theorem OAI.Generator.Tracial.CornerPartition.completionPiece_total line 225
  16. def OAI.Generator.Tracial.CornerPartition.completeUnit line 233
  17. theorem OAI.Generator.Tracial.CornerPartition.completeUnit_mem line 236
  18. theorem OAI.Generator.Tracial.CornerPartition.completeUnit_pinch line 245
  19. theorem OAI.Generator.Tracial.CornerPartition.completeUnit_pinch_supported line 251
  20. theorem OAI.Generator.Tracial.CornerPartition.completeUnit_refines_split line 255
  21. def OAI.Generator.Tracial.CornerPartition.mapInclusion line 292
  22. theorem OAI.Generator.Tracial.CornerPartition.include_pinch line 302
  23. theorem OAI.Generator.Tracial.CornerPartition.include_piece_mem line 309
  24. def OAI.Generator.Tracial.CornerPartition.includeUnit line 314

    Source documentation

    Unit partitions use the ambient identity, with no transport of the underlying finite index set.

    def includeUnit (Q : CornerPartition (identityProjection N)) (hNM : N ≤ M) :
    CornerPartition (identityProjection M) where
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.CornerPartition, OAI.Generator.Tracial.identityProjection

  25. theorem OAI.Generator.Tracial.CornerPartition.includeUnit_pinch line 321
  26. theorem OAI.Generator.Tracial.CornerPartition.includeUnit_energy line 326
  27. theorem OAI.Generator.Tracial.exists_nested_chain_centered_partition line 345
  28. theorem OAI.Generator.Tracial.CornerPartition.exists_indexed_local_L2_piece line 398

    Source documentation

    Finite pinching energy selects one nonzero projection with simultaneous strict squared-L2 bounds, with the actual trace as the weight.

    theorem CornerPartition.exists_indexed_local_L2_piece
    {p : AlgebraProjection M} (Q : CornerPartition p)
    {ι : Type*} (F : Finset ι) (x : ι → M.toStarSubalgebra)
    (ε : ℝ) (hE : (∑ i ∈ F,τ.norm₂ (Q.pinch (x i))^2) < ε*(τ.trace p.val).re) :
    ∃ j : Fin Q.size,(Q.piece j).val ≠ 0 ∧
      ∀ i ∈ F,τ.norm₂ ((Q.piece j).val*x i*(Q.piece j).val)^2 <
        ε*(τ.trace (Q.piece j).val).re := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.Q, OAI.Generator.Tracial.CornerPartition

  29. theorem OAI.Generator.Tracial.exists_nested_chain_local_piece line 421
  30. theorem OAI.Generator.Tracial.exists_matrix_generated_ambient_centered_partition line 459
  31. theorem OAI.Generator.Tracial.exists_irreducible_centered_partition line 502
  32. theorem OAI.Generator.Tracial.exists_irreducible_local_piece line 522