CornerTrace.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Trace estimates in the actual ambient algebra. The corner scalar uses its normalized trace. These estimates do not assume or assert the existence of a local-quantizing projection.

theorem OAI.Generator.Tracial.cornerTrace_add line 20
theorem OAI.Generator.Tracial.trace_sub line 23
theorem OAI.Generator.Tracial.cornerTrace_smul line 26
theorem OAI.Generator.Tracial.norm_trace_mul_le line 29
def OAI.Generator.Tracial.cornerScalar line 44
Source documentation
The scalar conditional expectation in pMp, expressed in ambient coordinates.
```
def cornerScalar (p : AlgebraProjection M) (x : M.toStarSubalgebra) : ℂ :=
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
def OAI.Generator.Tracial.cornerCentered line 47
theorem OAI.Generator.Tracial.cornerCentered_support line 50
theorem OAI.Generator.Tracial.cornerCentered_trace line 57
theorem OAI.Generator.Tracial.compress_cornerCentered line 66
theorem OAI.Generator.Tracial.supported_trace_test_le line 77
Source documentation
A supported compression has the trace scale sqrt(trace(q)), even against an arbitrary bounded ambient test operator.
```
theorem supported_trace_test_le (q : AlgebraProjection M) (x y : M.toStarSubalgebra)
    (hx : x*q.val=x) :
    ‖τ.trace (x*y)‖ ≤ τ.norm₂ x * (τ.norm₂ q.val * ‖y‖) := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.compression_trace_test_le line 85
def OAI.Generator.Tracial.traceAbs line 110
def OAI.Generator.Tracial.norm₁ line 111
theorem OAI.Generator.Tracial.traceAbs_selfAdjoint line 113
theorem OAI.Generator.Tracial.traceAbs_sq line 116
theorem OAI.Generator.Tracial.traceAbs_norm₂ line 119
theorem OAI.Generator.Tracial.trace_nonneg_of_nonneg line 126
theorem OAI.Generator.Tracial.norm₁_nonneg line 135
theorem OAI.Generator.Tracial.norm₁_le_norm₂ line 138
theorem OAI.Generator.Tracial.traceAbs_support line 142
Source documentation
Right support passes to the positive square root without a polar decomposition.
```
theorem traceAbs_support (q : AlgebraProjection M) (x : M.toStarSubalgebra)
    (hx : x*q.val=x) : traceAbs x*q.val=traceAbs x := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.traceAbs
theorem OAI.Generator.Tracial.norm₁_le_support_norm₂ line 157
Source documentation
The trace scale needed in corner local quantization.
```
theorem norm₁_le_support_norm₂ (q : AlgebraProjection M) (x : M.toStarSubalgebra)
    (hx : x*q.val=x) : norm₁ τ x ≤ τ.norm₂ x * τ.norm₂ q.val := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.norm₁
theorem OAI.Generator.Tracial.compression_norm₁_le line 164

theorem OAI.Generator.Tracial.compression_norm₁_lt_of_norm₂ line 170

Source documentation

A strict corner L2 estimate supplies the manuscript's actual L1 estimate.

theorem compression_norm₁_lt_of_norm₂ (q : AlgebraProjection M) (hq : q.val ≠ 0)
    (x : M.toStarSubalgebra) (ε : ℝ)
    (h : τ.norm₂ (q.val*x*q.val) < ε*τ.norm₂ q.val) :
    norm₁ τ (q.val*x*q.val) < ε*(τ.trace q.val).re := by
…

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

theorem OAI.Generator.Tracial.exists_small_energy_piece line 191

theorem OAI.Generator.Tracial.exists_corner_L1_of_partition_energy line 214

Source documentation

The aggregate squared L2 budget has exactly the trace weighting required for simultaneous strict L1 estimates on a nonzero subprojection.

theorem exists_corner_L1_of_partition_energy {I : Type*}
    (s : Finset I) (p : AlgebraProjection M) (q : I → AlgebraProjection M)
    (hq : ∀ i ∈ s, q i ≤ p) (F : Finset M.toStarSubalgebra)
    (ε : ℝ) (hε : 0 < ε)
    (henergy : ∑ i ∈ s, ∑ x ∈ F,
      τ.norm₂ ((q i).val*cornerCentered τ p x*(q i).val)^2 <
      ε^2 * ∑ i ∈ s, (τ.trace (q i).val).re) :
    ∃ r : AlgebraProjection M, r ≤ p ∧ r.val ≠ 0 ∧ (∃ i ∈ s, r=q i) ∧ ∀ x ∈ F,
      norm₁ τ (r.val*cornerCentered τ p x*r.val) < ε*(τ.trace r.val).re := by
…

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

theorem OAI.Generator.Tracial.CornerUnitary.norm₂_eq_support line 252
theorem OAI.Generator.Tracial.two_patch_trace_le line 260

theorem OAI.Generator.Tracial.two_patch_centered_trace_lt line 284

Source documentation

The middle compression may be corner-centered with respect to a larger residual support. This is the scalar version of the multiple-patch estimate.

theorem two_patch_centered_trace_lt (p q : AlgebraProjection M) (hq : q.val ≠ 0)
    (v w : CornerUnitary q) (a x b : M.toStarSubalgebra) (ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1)
    (ε : ℝ) (h : τ.norm₂ (q.val*cornerCentered τ p x*q.val) < ε*τ.norm₂ q.val) :
    ‖τ.trace (a*v.val*cornerCentered τ p x*w.val*b)‖ < ε*(τ.trace q.val).re := by
…

Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.CornerUnitary, OAI.Generator.Tracial.cornerCentered