OAI/Analysis/FactorGeneration/EnergyDescent.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Quantitative descent for a finite spectral pinching, and actual unitary displacement from irreducibility. A compatible spectral partition in a residual corner is not postulated as a local-quantization theorem.

  1. theorem OAI.Generator.Tracial.exists_centered_unitary_displacement line 20

    Source documentation

    Irreducibility supplies displacement for every nonzero centered operator, without any orthogonality-to-P premise.

    theorem exists_centered_unitary_displacement
    (P : StarSubalgebra ℂ M.toStarSubalgebra) [CompleteSpace P]
    (hirr : ∀ c : M.toStarSubalgebra,
      (∀ a : P, (a : M.toStarSubalgebra)*c = c*(a : M.toStarSubalgebra)) →
      ∃ z : ℂ, c = z • (1 : M.toStarSubalgebra))
    (x : M.toStarSubalgebra) (hx : x ≠ 0) (ht : τ.trace x = 0)
    (r : ℝ) (hr : r < 1) :
    ∃ u : subalgebraUnitaries P, r*τ.norm₂ x < τ.norm₂ (conjugateLinear u.val x-x) := by
…

    Mentions: OAI.Generator.Tracial.subalgebraUnitaries, OAI.Generator.Tracial.conjugateLinear

  2. theorem OAI.Generator.Tracial.exists_strict_centered_displacement line 38

    Source documentation

    The strict displacement used before finite spectral approximation in Popa A.1.1, Step 1, in the scalar-commutant case.

    theorem exists_strict_centered_displacement
    (P : StarSubalgebra ℂ M.toStarSubalgebra) [CompleteSpace P]
    (hirr : ∀ c : M.toStarSubalgebra,
      (∀ a : P, (a : M.toStarSubalgebra)*c = c*(a : M.toStarSubalgebra)) →
      ∃ z : ℂ, c = z • (1 : M.toStarSubalgebra))
    (x : M.toStarSubalgebra) (hx : x ≠ 0) (ht : τ.trace x = 0) :
    ∃ u : subalgebraUnitaries P, τ.norm₂ x < τ.norm₂ (conjugateLinear u.val x-x) := by
…

    Mentions: OAI.Generator.Tracial.subalgebraUnitaries, OAI.Generator.Tracial.conjugateLinear

  3. theorem OAI.Generator.Tracial.CornerPartition.pinch_commutes_diagonal line 83
  4. theorem OAI.Generator.Tracial.CornerPartition.pinch_fixed_of_commutes line 93
  5. theorem OAI.Generator.Tracial.CornerPartition.displacement_le_twice_residual line 99
  6. theorem OAI.Generator.Tracial.CornerPartition.displacement_energy_bound line 115

    Source documentation

    The exact squared displacement bound behind the partition descent.

    theorem displacement_energy_bound (u : unitary M.toStarSubalgebra)
    (x : M.toStarSubalgebra) (hfixed : conjugateLinear u (Q.pinch x) = Q.pinch x) :
    τ.norm₂ (conjugateLinear u x-x)^2 ≤ 4*(τ.norm₂ x^2-τ.norm₂ (Q.pinch x)^2) := by
…

    Mentions: OAI.Generator.Tracial.conjugateLinear

  7. theorem OAI.Generator.Tracial.CornerPartition.three_quarters_energy line 125

    Source documentation

    The factor 3/4 in Popa A.1.1, Step 2, for the actual finite spectral pinching and its displayed displacement estimate.

    theorem three_quarters_energy (u : unitary M.toStarSubalgebra)
    (x : M.toStarSubalgebra) (hfixed : conjugateLinear u (Q.pinch x) = Q.pinch x)
    (hdisplace : τ.norm₂ x ≤ τ.norm₂ (conjugateLinear u x-x)) :
    (∑ i, τ.norm₂ ((Q.piece i).val*x*(Q.piece i).val)^2) ≤ (3/4 : ℝ)*τ.norm₂ x^2 := by
…

    Mentions: OAI.Generator.Tracial.conjugateLinear

  8. theorem OAI.Generator.Tracial.CornerPartition.spectral_sum_commutes_pinch line 138
  9. theorem OAI.Generator.Tracial.CornerPartition.commutator_le_residual line 143
  10. theorem OAI.Generator.Tracial.commutator_perturbation line 161
  11. theorem OAI.Generator.Tracial.displacement_le_commutator line 172
  12. theorem OAI.Generator.Tracial.CornerPartition.energy_descent_of_spectral_approximation line 186

    Source documentation

    Energy decrease from a spectral approximation, with the actual partition and approximation error exposed.

    theorem CornerPartition.energy_descent_of_spectral_approximation
    {p : AlgebraProjection M} (Q : CornerPartition p)
    (u : unitary M.toStarSubalgebra) (x : M.toStarSubalgebra) (c : Fin Q.size → ℂ)
    (hd : τ.norm₂ x ≤ τ.norm₂ (conjugateLinear u x-x))
    (hclose : ‖(u : M.toStarSubalgebra)-∑ i,c i • (Q.piece i).val‖ < 1/4) :
    (∑ i,τ.norm₂ ((Q.piece i).val*x*(Q.piece i).val)^2) ≤
      (63/64 : ℝ)*τ.norm₂ x^2 := by
…

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

  13. theorem OAI.Generator.Tracial.exists_partition_energy_descent line 215

    Source documentation

    A displaced operator has a genuinely constructed finite partition with energy at most 63/64 of its original energy. This is one step, not iteration.

    theorem exists_partition_energy_descent (u : unitary M.toStarSubalgebra)
    (x : M.toStarSubalgebra)
    (hd : τ.norm₂ x ≤ τ.norm₂ (conjugateLinear u x-x)) :
    ∃ Q : CornerPartition (identityProjection M),
      (∑ i, τ.norm₂ ((Q.piece i).val*x*(Q.piece i).val)^2) ≤
        (63/64 : ℝ)*τ.norm₂ x^2 := by
…

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

  14. theorem OAI.Generator.Tracial.exists_subalgebra_partition_energy_descent line 234
  15. theorem OAI.Generator.Tracial.exists_irreducible_partition_energy_descent line 247

    Source documentation

    One actual finite partition decreases every given nonzero centered operator's energy. This does not assert an arbitrary target budget or permit iteration through uncentered residual blocks.

    theorem exists_irreducible_partition_energy_descent (h : N ≤ M)
    (P : StarSubalgebra ℂ M.toStarSubalgebra) [CompleteSpace P]
    (hP : ∀ a : M.toStarSubalgebra,a ∈ P ↔ a.val ∈ N)
    (hirr : ∀ c : M.toStarSubalgebra,
      (∀ a : P,(a : M.toStarSubalgebra)*c=c*(a : M.toStarSubalgebra)) →
      ∃ z : ℂ,c=z • (1 : M.toStarSubalgebra))
    (x : M.toStarSubalgebra) (hx : x ≠ 0) (ht : τ.trace x=0) :
    ∃ Q : CornerPartition (identityProjection M),
      (∀ i,(Q.piece i).val ∈ P) ∧
      (∑ i,τ.norm₂ ((Q.piece i).val*x*(Q.piece i).val)^2) < τ.norm₂ x^2 := by
…

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

  16. theorem OAI.Generator.Tracial.exists_strict_displacement_of_zero_orbitHull line 274
  17. theorem OAI.Generator.Tracial.CornerPartition.exists_compatible_orthogonal_descent line 325
  18. theorem OAI.Generator.Tracial.CornerPartition.exists_orthogonal_geometric_refinement line 392
  19. theorem OAI.Generator.Tracial.CornerPartition.exists_orthogonal_refinement_budget line 411
  20. theorem OAI.Generator.Tracial.CornerPartition.exists_finite_orthogonal_refinement_budget line 428

    Source documentation

    One actual finite compatible partition gives an arbitrarily small SUM of energies for the whole finite orthogonal family.

    theorem exists_finite_orthogonal_refinement_budget
    (Q : CornerPartition (identityProjection M))
    (hN : ∀ i,(Q.piece i).val.val ∈ N)
    (F : Finset M.toStarSubalgebra)
    (hF : ∀ x ∈ F,TraceOrthogonal τ (insideAlgebra (M := M) (P := N)) x)
…

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

  21. theorem OAI.Generator.Tracial.CornerPartition.exists_indexed_orthogonal_refinement_budget line 450
  22. theorem OAI.Generator.Tracial.exists_component_controlled_refinement line 486

    Source documentation

    Any previously established coarse component budget survives the actual finite-family quantization of the orthogonal residual.

    theorem exists_component_controlled_refinement (hNM : N ≤ M)
    (hirr : ∀ c : M.toStarSubalgebra,
      (∀ a : insideAlgebra (M := M) (P := N),
…

    Mentions: OAI.Generator.Tracial.insideAlgebra