OAI/Analysis/FactorGeneration/ResidualEstimates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Correct residual-corner trace identity for arbitrary f. The first term is trace(f*x), not trace(x); they agree when f=1. This is the distinction at Popa 1308.3982v3 Lemma 3.2, equation (5).

  1. def OAI.Generator.Tracial.residualCorner line 17
  2. theorem OAI.Generator.Tracial.projection_compression_trace line 21
  3. theorem OAI.Generator.Tracial.residualCorner_trace line 25
  4. theorem OAI.Generator.Tracial.residualCorner_compression_trace line 30
  5. theorem OAI.Generator.Tracial.residualCorner_positive line 44
  6. theorem OAI.Generator.Tracial.residualCorner_support_ratio line 52
  7. theorem OAI.Generator.Tracial.residualCorner_scalar_bound line 62

    Source documentation

    This keeps the f-dependent scalar term that cannot be bounded from global centering alone.

    theorem residualCorner_scalar_bound (f : AlgebraProjection M) (hf : f.val ≠ 0)
    (v : PartialUnitary M) (hv : v.support ≤ f)
    (hsmall : (τ.trace v.support.val).re ≤ (τ.trace f.val).re/4)
    (x : M.toStarSubalgebra) :
    ‖cornerScalar τ (residualCorner f v hv) x‖ ≤
      (‖τ.trace (f.val*x)‖+‖τ.trace (star v.val*x*v.val)‖) /
        (τ.trace (residualCorner f v hv).val).re := by
…

    Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.cornerScalar, OAI.Generator.Tracial.residualCorner

  8. def OAI.Generator.Tracial.unitResidual line 83
  9. theorem OAI.Generator.Tracial.unitResidual_trace line 86
  10. theorem OAI.Generator.Tracial.unitResidual_compression_trace line 90
  11. theorem OAI.Generator.Tracial.unitResidual_positive line 97
  12. theorem OAI.Generator.Tracial.unitResidual_scalar_bound line 105

    Source documentation

    A previously controlled length-two moment gives the factor 1/3 in the current residual's scalar expectation. No new centering premise is inferred.

    theorem unitResidual_scalar_bound (v : PartialUnitary M)
    (hsmall : (τ.trace v.support.val).re ≤ 1/4)
    (x : M.toStarSubalgebra) (ht : τ.trace x=0) (δ : ℝ) (hδ : 0 ≤ δ)
    (hmoment : ‖τ.trace (star v.val*x*v.val)‖ ≤ δ*(τ.trace v.support.val).re) :
    ‖cornerScalar τ (unitResidual v) x‖ ≤ δ/3 := by
…

    Mentions: OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.cornerScalar, OAI.Generator.Tracial.unitResidual

  13. theorem OAI.Generator.Tracial.unitResidual_local_L2 line 119

    Source documentation

    The corresponding actual residual compression bound, once a local centered L2 estimate has been proved for q. It retains q and its trace.

    theorem unitResidual_local_L2 (v : PartialUnitary M)
    (hsmall : (τ.trace v.support.val).re ≤ 1/4)
    (x : M.toStarSubalgebra) (ht : τ.trace x=0) (δ η : ℝ) (hδ : 0 ≤ δ)
    (hmoment : ‖τ.trace (star v.val*x*v.val)‖ ≤ δ*(τ.trace v.support.val).re)
    (q : AlgebraProjection M) (hq : q ≤ unitResidual v)
    (hlocal : τ.norm₂ (q.val*cornerCentered τ (unitResidual v) x*q.val) < η*τ.norm₂ q.val) :
    τ.norm₂ (q.val*x*q.val) < (η+δ/3)*τ.norm₂ q.val := by
…

    Mentions: OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.unitResidual, OAI.Generator.Tracial.cornerCentered