OAI/Analysis/FactorGeneration/CoordinatePerturbation.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Group-ring maps from actual bounded unitary coordinates, with quotient transport and coordinate Gram limits.

  1. def OAI.Generator.Tracial.boundedToSequence line 18
  2. theorem OAI.Generator.Tracial.boundedToSequence_map line 21
  3. theorem OAI.Generator.Tracial.boundedToSequence_apply line 24
  4. def OAI.Generator.Tracial.boundedUnitarySequence line 27
  5. def OAI.Generator.Tracial.sequenceUnitaryQuotient line 39
  6. theorem OAI.Generator.Tracial.sequenceUnitaryQuotient_bounded line 44
  7. def OAI.Generator.Tracial.coordinateGroupRing line 51
  8. theorem OAI.Generator.Tracial.coordinateGroupRing_single line 56
  9. theorem OAI.Generator.Tracial.freeGroup_quotient line 60
  10. theorem OAI.Generator.Tracial.coordinateGroupRing_quotient_single line 67
  11. theorem OAI.Generator.Tracial.coordinateGroupRing_gram_limits line 74
  12. theorem OAI.Generator.Tracial.coordinateGroupRing_orthonormal line 88
  13. theorem OAI.Generator.Tracial.coordinateGroupRing_isometry line 99
  14. theorem OAI.Generator.Tracial.unitaryRepresentation_prefix line 122
  15. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.labelUnitary line 136
  16. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.targetUnitary line 140
  17. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.conjugateUnitary line 144
  18. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.label_mem line 148
  19. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.label_ratio_zero line 172
  20. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.conjugate_trace line 183
  21. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.conjugate_injective line 191
  22. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.conjugate_gram line 196
  23. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.conjugate_orthonormal line 206
  24. theorem OAI.Generator.Tracial.orthonormal_of_coordinate_moments line 231
  25. def OAI.Generator.Tracial.remainderSequence line 244
  26. theorem OAI.Generator.Tracial.tracial_remainder_of_coordinate_moments line 250

    Source documentation

    The actual quotient two-norm estimate from coordinate word moments.

    theorem tracial_remainder_of_coordinate_moments (n : ℕ) (hn : 0 < n)
    (Φ : MonoidAlgebra ℂ (FreeGroup (PrefixLabel n)) →ₐ[ℂ] Sequences M)
    (hmom : ∀ g h : FreeGroup (PrefixLabel n),
      Tendsto (fun k => τ.trace (star (Φ (MonoidAlgebra.single g 1) k)*
        Φ (MonoidAlgebra.single h 1) k)) (ω : Filter ℕ)
        (𝓝 (if g = h then 1 else 0)))
    (α : ℝ) (hα : 0 < α) (hhalf : α < 1/2) :
    ‖sequenceQuotient τ ω (remainderSequence n α Φ)‖ ≤ 4*α^2/(1-2*α) := by
…

    Mentions: OAI.Generator.PrefixLabel, OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.sequenceQuotient, OAI.Generator.Tracial.remainderSequence

  27. theorem OAI.Generator.Tracial.coordinate_remainder_eventually line 268

    Source documentation

    The remainder bound holds with any positive slack on an ultrafilter-large set of actual coordinates, once the displayed word moments are constructed.

    theorem coordinate_remainder_eventually (n : ℕ) (hn : 0 < n)
    (Φ : MonoidAlgebra ℂ (FreeGroup (PrefixLabel n)) →ₐ[ℂ] Sequences M)
    (hmom : ∀ g h : FreeGroup (PrefixLabel n),
      Tendsto (fun k => τ.trace (star (Φ (MonoidAlgebra.single g 1) k)*
        Φ (MonoidAlgebra.single h 1) k)) (ω : Filter ℕ)
        (𝓝 (if g = h then 1 else 0)))
    (α : ℝ) (hα : 0 < α) (hhalf : α < 1/2) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ k in (ω : Filter ℕ), τ.norm₂ (remainderSequence n α Φ k) < 4*α^2/(1-2*α)+ε := by
…

    Mentions: OAI.Generator.PrefixLabel, OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.remainderSequence

  28. def OAI.Generator.Tracial.constantSequenceUnitary line 291
  29. def OAI.Generator.Tracial.constantQuotientUnitary line 294
  30. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.haarSequence line 299
  31. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.haarSequence_apply line 304
  32. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.haarSequence_quotient line 309
  33. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinateVariables line 317
  34. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinateVariables_quotient line 322
  35. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinateLabels line 333
  36. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinateTarget line 337
  37. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinateConjugates line 341
  38. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinateLabels_quotient line 345
  39. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinateTarget_quotient line 352
  40. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinateConjugates_quotient line 366
  41. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbationMap line 381
  42. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbationMap_gram line 386
  43. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbationMap_isometry line 398
  44. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbation_remainder line 409
  45. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinate_remainder line 419
  46. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinatePrefix line 441
  47. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.commonPerturbation line 445
  48. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.commonPerturbation_skew line 452
  49. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.coordinateLabels_pair line 477
  50. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbationMap_row line 487
  51. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbingUnitary line 517
  52. def OAI.Generator.Tracial.SuccessiveCoordinateHaar.perturbedUnitary line 524
  53. theorem OAI.Generator.Tracial.sequence_exp_conjugate line 528
  54. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.exponential_row line 538