AmplificationPartition.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The actual diagonal partition in a matrix amplification

Outer row indices and inner matrix-unit indices give n*k mutually orthogonal diagonal projections. Relabeling by finProdFinEquiv matches the phase multiset supports with the concrete support projections used in the clipped-column estimate.

def OAI.KadisonKastler.amplificationPartition line 36
Source documentation
The diagonal partition indexed by a single finite label set.
```
def amplificationPartition (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (a : Fin (n * k)) : Algebra (matrixVonNeumann (ι := Fin n) M) :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.amplificationPartition_projection line 40
theorem OAI.KadisonKastler.amplificationPartition_orthogonal line 45
theorem OAI.KadisonKastler.amplificationPartition_total line 52
theorem OAI.KadisonKastler.amplificationPartition_trace line 62
Source documentation
Every atom has normalized trace 1/(n*k).
```
theorem amplificationPartition_trace [NeZero n]
    (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (τ : FaithfulTracialState (Algebra M)) (a : Fin (n * k)) :
    (matrixVonNeumannTrace (ι := Fin n) M τ).toLinearMap (amplificationPartition E a) =
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.matrixVonNeumannTrace, OAI.KadisonKastler.amplificationPartition
def OAI.KadisonKastler.amplificationSupport line 79
Source documentation
A multiset of phase labels names the corresponding outer/inner support atoms.
```
def amplificationSupport (s : Multiset (Fin (n * k))) : Finset (Fin n × Fin k) :=
…
```
theorem OAI.KadisonKastler.mem_amplificationSupport line 83
theorem OAI.KadisonKastler.amplificationSupport_card_le line 95
theorem OAI.KadisonKastler.amplificationSupport_sym_card_le line 100
theorem OAI.KadisonKastler.amplificationSupport_small line 104
theorem OAI.KadisonKastler.concreteMatrixEntries_amplificationPartition line 109
Source documentation
Matrix entries of one relabeled atom are exactly the original operator atom.
```
theorem concreteMatrixEntries_amplificationPartition
    (E : Generator.MatrixUnitSystem (Fin k) (Algebra M)) (a : Fin (n * k)) :
    concreteMatrixEntries (M := M) (n := n) (amplificationPartition E a) =
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.concreteMatrixEntries, OAI.KadisonKastler.amplificationPartition
theorem OAI.KadisonKastler.concreteMatrixEntries_phaseSupport line 124
Source documentation
Phase supports coincide with the support projections in the small-column lemma.
```
theorem concreteMatrixEntries_phaseSupport
    (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (s : Multiset (Fin (n * k))) :
    concreteMatrixEntries (M := M) (n := n) (phaseSupport (amplificationPartition E) s) =
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.concreteMatrixEntries, OAI.KadisonKastler.phaseSupport, OAI.KadisonKastler.amplificationPartition

theorem OAI.KadisonKastler.amplificationSupport_weight_sum_eq line 135

Source documentation

Reindexing the support budget gives exactly the through-label sum.

theorem amplificationSupport_weight_sum_eq {r : ℕ} (C : ℝ) (p : Fin n × Fin k) :
    (∑ s : Sym (Fin (n * k)) r,
      if p ∈ amplificationSupport (s : Multiset (Fin (n * k)))
      then projectionWordWeight C s ^ 2 else 0) =
      ∑ s : ThroughLabel (finProdFinEquiv p) r, projectionWordWeight C s.val ^ 2 := by
…

Mentions: OAI.KadisonKastler.amplificationSupport, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.ThroughLabel

theorem OAI.KadisonKastler.amplificationSupport_weight_sum_le line 148
theorem OAI.KadisonKastler.amplificationProjectionWordWeight_pos line 159
Source documentation
The actual clipping thresholds are strictly positive.
```
theorem amplificationProjectionWordWeight_pos [NeZero n] [NeZero k]
    {r : ℕ} (s : Sym (Fin (n * k)) r) :
    0 < projectionWordWeight (freeWordC r) s := by
…
```
Mentions: OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC
theorem OAI.KadisonKastler.exists_amplification_partition_size line 175
Source documentation
One inner matrix size suffices for every degree up to N, including both the free-word norm bounds and the through-label square-sum budget.
```
theorem exists_amplification_partition_size (n N : ℕ) (hn : 0 < n) :
    ∃ k : ℕ, 0 < k ∧ N ≤ k ∧
      (∀ r ≤ N, freeWordThreshold r ≤ n * k) ∧
      ∀ r : ℕ, 1 ≤ r → r ≤ N → ∀ a : Fin (n * k),
        (∑ s : ThroughLabel a r, projectionWordWeight (freeWordC r) s.val ^ 2) ≤ 64 := by
…
```
Mentions: OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.ThroughLabel, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC

theorem OAI.KadisonKastler.exists_amplification_partition_matrixUnits line 192

Source documentation

A factor supplies the chosen inner matrix units at the same uniform size.

theorem exists_amplification_partition_matrixUnits
    (hM : Generator.IsII1Factor M.toStarSubalgebra) (n N : ℕ) (hn : 0 < n) :
    ∃ k : ℕ, 0 < k ∧ N ≤ k ∧
      Nonempty (Generator.MatrixUnitSystem (Fin k) (Algebra M)) ∧
      (∀ r ≤ N, freeWordThreshold r ≤ n * k) ∧
      ∀ r : ℕ, 1 ≤ r → r ≤ N → ∀ a : Fin (n * k),
        (∑ s : ThroughLabel a r, projectionWordWeight (freeWordC r) s.val ^ 2) ≤ 64 := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.ThroughLabel, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC