Pinching.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

Finite pinching in the actual ambient algebra. The squared L2 energy is a sum of the energies of the mutually orthogonal compression blocks. These identities do not postulate a local-quantizing partition.

structure OAI.Generator.Tracial.CornerPartition line 19
Source documentation
A finite projection partition of a corner, allowing zero pieces.
```
structure CornerPartition (p : AlgebraProjection M) where
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.CornerPartition.piece_le line 28
def OAI.Generator.Tracial.CornerPartition.pinch line 35
theorem OAI.Generator.Tracial.CornerPartition.pinch_add line 38
theorem OAI.Generator.Tracial.CornerPartition.pinch_sub line 42
theorem OAI.Generator.Tracial.CornerPartition.pinch_smul line 46
theorem OAI.Generator.Tracial.CornerPartition.pinch_support line 50
theorem OAI.Generator.Tracial.CornerPartition.pinch_left line 57
theorem OAI.Generator.Tracial.CornerPartition.pinch_right line 66
theorem OAI.Generator.Tracial.CornerPartition.pinch_idempotent line 75
theorem OAI.Generator.Tracial.CornerPartition.pinch_trace line 83
theorem OAI.Generator.Tracial.norm₂_sq_trace line 104
theorem OAI.Generator.Tracial.trace_compression_pairing line 108
theorem OAI.Generator.Tracial.baseVector_inner_trace line 114
theorem OAI.Generator.Tracial.CornerPartition.pinch_pairing line 123
theorem OAI.Generator.Tracial.CornerPartition.pinch_residual_orthogonal line 130
theorem OAI.Generator.Tracial.CornerPartition.pinch_pythagoras line 136
theorem OAI.Generator.Tracial.CornerPartition.pinch_norm₂_le line 146
theorem OAI.Generator.Tracial.CornerPartition.pinch_block_orthogonal line 151
theorem OAI.Generator.Tracial.CornerPartition.pinch_energy line 159
theorem OAI.Generator.Tracial.CornerPartition.pinch_family_energy line 175
Source documentation
The precise finite energy input is the squared norm of the pinched corner-centered family; orthogonality proves this equality.
```
theorem pinch_family_energy (F : Finset M.toStarSubalgebra) :
    (∑ i, ∑ x ∈ F, τ.norm₂ ((Q.piece i).val*cornerCentered τ p x*(Q.piece i).val)^2) =
      ∑ x ∈ F, τ.norm₂ (Q.pinch (cornerCentered τ p x))^2 := by
…
```
Mentions: OAI.Generator.Tracial.cornerCentered
theorem OAI.Generator.Tracial.CornerPartition.pinch_corner line 186
theorem OAI.Generator.Tracial.CornerPartition.pinch_corner_compression line 194
theorem OAI.Generator.Tracial.CornerPartition.pinch_cornerCentered line 204
theorem OAI.Generator.Tracial.CornerPartition.pinch_compress_of_le line 208
def OAI.Generator.Tracial.CornerPartition.Refines line 220
theorem OAI.Generator.Tracial.CornerPartition.pinch_refinement line 222
theorem OAI.Generator.Tracial.CornerPartition.refinement_energy_le line 230
theorem OAI.Generator.Tracial.CornerPartition.trace_total line 237

theorem OAI.Generator.Tracial.CornerPartition.exists_local_piece_of_pinching_energy line 245

Source documentation

Converting a genuine pinching budget into the requested nonzero local piece. The budget is explicit; this theorem does not claim to construct it.

theorem exists_local_piece_of_pinching_energy
    (P : StarSubalgebra ℂ M.toStarSubalgebra) (hP : ∀ i, (Q.piece i).val ∈ P)
    (F : Finset M.toStarSubalgebra) (ε : ℝ) (hε : 0 < ε)
    (henergy : (∑ x ∈ F, τ.norm₂ (Q.pinch (cornerCentered τ p x))^2) <
      ε^2 * (τ.trace p.val).re) :
    ∃ q : AlgebraProjection M, q ≤ p ∧ q.val ≠ 0 ∧ q.val ∈ P ∧ ∀ x ∈ F,
      norm₁ τ (q.val*x*q.val-cornerScalar τ p x • q.val) < ε*(τ.trace q.val).re := by
…

Mentions: OAI.Generator.Tracial.cornerCentered, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.norm₁, OAI.Generator.Tracial.cornerScalar

def OAI.Generator.Tracial.CornerPartition.ofFamily line 275
Source documentation
Reindex an explicitly finite orthogonal family by Fin.
```
def ofFamily {ι : Type*} [Fintype ι] (a : ι → AlgebraProjection M)
    (ha : ∀ i j, i ≠ j → (a i).val*(a j).val=0)
    (ht : ∑ i, (a i).val=p.val) : CornerPartition p where
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.CornerPartition
theorem OAI.Generator.Tracial.CornerPartition.ofFamily_pinch line 283
def OAI.Generator.Tracial.CornerPartition.single line 290
Source documentation
The partition with its corner as its only piece.
```
def single (p : AlgebraProjection M) : CornerPartition p where
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.CornerPartition
theorem OAI.Generator.Tracial.CornerPartition.single_pinch line 296
theorem OAI.Generator.Tracial.CornerPartition.blockFamily_orthogonal line 303
theorem OAI.Generator.Tracial.CornerPartition.blockFamily_total line 314
def OAI.Generator.Tracial.CornerPartition.refineBlocks line 320
Source documentation
All blocks are replaced by their chosen finite subpartitions.
```
def refineBlocks : CornerPartition p :=
…
```
Mentions: OAI.Generator.Tracial.CornerPartition
theorem OAI.Generator.Tracial.CornerPartition.refineBlocks_refines line 324
theorem OAI.Generator.Tracial.CornerPartition.refineBlocks_mem line 329
theorem OAI.Generator.Tracial.CornerPartition.refineBlocks_pinch line 335
theorem OAI.Generator.Tracial.CornerPartition.refineBlocks_energy line 341
Source documentation
Energy splits into the actual energies of the independently refined blocks.
```
theorem refineBlocks_energy (τ : TracialRepresentation M) (x : M.toStarSubalgebra) :
    τ.norm₂ ((Q.refineBlocks R).pinch x)^2 = ∑ i, τ.norm₂ ((R i).pinch x)^2 := by
…
```
Mentions: OAI.Generator.Tracial.CornerPartition.pinch
theorem OAI.Generator.Tracial.CornerPartition.refines_refl line 357
theorem OAI.Generator.Tracial.CornerPartition.refines_trans line 359
theorem OAI.Generator.Tracial.cornerCentered_trace_all line 378
theorem OAI.Generator.Tracial.CornerPartition.pinch_centered_trace line 388
theorem OAI.Generator.Tracial.CornerPartition.pinch_centered_orthogonal line 393
theorem OAI.Generator.Tracial.CornerPartition.pinch_scalar_energy line 401
Source documentation
Pinching energy is centered energy plus the unchanged corner scalar energy.
```
theorem pinch_scalar_energy (x : M.toStarSubalgebra) :
    τ.norm₂ (Q.pinch x)^2 = τ.norm₂ (Q.pinch (cornerCentered τ p x))^2 +
      ‖cornerScalar τ p x‖^2 * (τ.trace p.val).re := by
…
```
Mentions: OAI.Generator.Tracial.cornerCentered, OAI.Generator.Tracial.cornerScalar
theorem OAI.Generator.Tracial.CornerPartition.scalar_energy_le_pinch line 419
def OAI.Generator.Tracial.CornerPartition.scalarEnergy line 439
Source documentation
The part of the compression energy fixed by the current block traces.
```
def scalarEnergy (x : M.toStarSubalgebra) : ℝ :=
…
```
theorem OAI.Generator.Tracial.CornerPartition.scalarEnergy_nonneg line 442
theorem OAI.Generator.Tracial.CornerPartition.refineBlocks_scalar_energy line 447
theorem OAI.Generator.Tracial.CornerPartition.scalarEnergy_le_refineBlocks line 454

theorem OAI.Generator.Tracial.CornerPartition.refineBlocks_descent line 461

Source documentation

Compatible descent bounds centered block energies and retains the full coarse scalar term. In particular it does not multiply that term by c.

theorem refineBlocks_descent (x : M.toStarSubalgebra) (c : ℝ)
    (h : ∀ i, τ.norm₂ ((R i).pinch (cornerCentered τ (Q.piece i) x))^2 ≤
      c * τ.norm₂ (cornerCentered τ (Q.piece i) x)^2) :
    τ.norm₂ ((Q.refineBlocks R).pinch x)^2 ≤
      c*(τ.norm₂ (Q.pinch x)^2-Q.scalarEnergy τ x)+Q.scalarEnergy τ x := by
…

Mentions: OAI.Generator.Tracial.CornerPartition.pinch, OAI.Generator.Tracial.cornerCentered

theorem OAI.Generator.Tracial.CornerPartition.no_refineBlocks_budget_below_scalar line 483
Source documentation
A target below the current scalar term cannot be reached by refining these blocks, regardless of the quality of centered local estimates.
```
theorem no_refineBlocks_budget_below_scalar (x : M.toStarSubalgebra) (b : ℝ)
    (hb : b ≤ Q.scalarEnergy τ x) :
    ¬ τ.norm₂ ((Q.refineBlocks R).pinch x)^2 < b :=
…
```
Mentions: OAI.Generator.Tracial.CornerPartition.pinch