OAI/Analysis/FactorGeneration/LocalPatches.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Generator.Tracial.unitResidual_scalar_two_moment_bound line 18
2. theorem OAI.Generator.Tracial.exists_unitResidual_local_compression line 46
3. theorem OAI.Generator.Tracial.exists_unitResidual_controlled_patch line 83

   Source documentation

   Choose the patch unitary after q, so the same q controls all two-letter terms and the signed one-letter traces are as small as prescribed.

   theorem exists_unitResidual_controlled_patch
       (v : PartialUnitary M) (hvN : v.val.val ∈ N)
       (hsmall : (τ.trace v.support.val).re ≤ 1/4)
       {ι : Type*} (F : Finset ι) (x : ι → M.toStarSubalgebra) (A B : ι → ℝ)
       (hAB : ∀ i ∈ F,0 ≤ A i+B i)
       (hA : ∀ i ∈ F,‖τ.trace (x i)‖ ≤ A i*(τ.trace v.support.val).re)
       (hB : ∀ i ∈ F,‖τ.trace (star v.val*x i*v.val)‖ ≤ B i*(τ.trace v.support.val).re)
       (L R : Finset M.toStarSubalgebra) (η κ : ℝ) (hη : 0 < η) (hκ : 0 < κ) :
       ∃ (q : AlgebraProjection M) (w : CornerUnitary q),
         q ≤ unitResidual v ∧ q.val ≠ 0 ∧ q.val.val ∈ N ∧ w.val.val ∈ N ∧
         (∀ a ∈ L,∀ b ∈ R,∀ s : Bool,‖τ.trace (a*signedLetter w.val s*b)‖ < κ*(τ.trace q.val).re) ∧
         (∀ i ∈ F,∀ u z : CornerUnitary q,∀ a b : M.toStarSubalgebra,‖a‖ ≤ 1 → ‖b‖ ≤ 1 →
   …

   Mentions: OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.CornerUnitary, OAI.Generator.Tracial.unitResidual, OAI.Generator.Tracial.signedLetter

4. theorem OAI.Generator.Tracial.exists_admissible_family_patch line 138
5. def OAI.Generator.Tracial.signedCornerUnitary line 187
6. theorem OAI.Generator.Tracial.signedCornerUnitary_val line 190
7. theorem OAI.Generator.Tracial.maskedWord_one_decomposition line 193
8. theorem OAI.Generator.Tracial.maskedWord_one_trace_lt line 210
9. theorem OAI.Generator.Tracial.maskedWord_two_trace_lt line 233
10. theorem OAI.Generator.Tracial.unitResidual_orthogonal line 285
11. def OAI.Generator.Tracial.unitResidualPatch line 291
12. theorem OAI.Generator.Tracial.unitResidualPatch_extends line 296
13. theorem OAI.Generator.Tracial.unitResidualPatch_trace line 302
14. theorem OAI.Generator.Tracial.exists_strict_admissible_unit_patch line 322

    Source documentation

    The full extension satisfies every original admissibility inequality and has strictly greater support trace. No patch growth premise is assumed.

    theorem exists_strict_admissible_unit_patch
        (F : Finset M.toStarSubalgebra) (hF : ∀ x ∈ F,‖x‖ ≤ 1)
        (hcenter : ∀ x ∈ F,τ.trace x=0) (n : ℕ) (δ : ℝ) (hδ : 0 < δ)
        (v : PartialUnitary M)
        (hv : PatchingAdmissibleIn (P := N) τ (identityProjection M) F n (patchingTolerance δ) v)
    …

    Mentions: OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.PatchingAdmissibleIn, OAI.Generator.Tracial.identityProjection, OAI.Generator.Tracial.patchingTolerance

15. theorem OAI.Generator.Tracial.exists_large_admissible_partialUnitary line 410

    Source documentation

    The maximal-element contradiction now gives support trace strictly greater than one quarter in the f=1 scalar-commutant setting.

    theorem exists_large_admissible_partialUnitary
        (F : Finset M.toStarSubalgebra) (hF : ∀ x ∈ F,‖x‖ ≤ 1)
        (hcenter : ∀ x ∈ F,τ.trace x=0) (n : ℕ) (δ : ℝ) (hδ : 0 < δ) :
        ∃ v : PartialUnitary M,
          PatchingAdmissibleIn (P := N) τ (identityProjection M) F n (patchingTolerance δ) v ∧
    …

    Mentions: OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.PatchingAdmissibleIn, OAI.Generator.Tracial.identityProjection, OAI.Generator.Tracial.patchingTolerance