OAI/Analysis/FactorGeneration/HaarPatches.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The same ordered signed words in any star algebra, with exact transport through bounded sequence evaluation and the actual quotient homomorphism.

  1. def OAI.Generator.Tracial.algebraSignedLetter line 14
  2. def OAI.Generator.Tracial.algebraPatchingWord line 17
  3. def OAI.Generator.Tracial.optionalCoefficient line 22
  4. theorem OAI.Generator.Tracial.map_algebraPatchingWord line 26
  5. theorem OAI.Generator.Tracial.algebraPatchingWord_eq line 43
  6. def OAI.Generator.Tracial.boundedEvaluation line 50
  7. theorem OAI.Generator.Tracial.bounded_word_evaluation line 59
  8. theorem OAI.Generator.Tracial.patchingTolerance_scale line 80
  9. def OAI.Generator.Tracial.diagonalCoefficientFamily line 86
  10. theorem OAI.Generator.Tracial.exists_finite_partial_independence line 101
  11. theorem OAI.Generator.Tracial.exists_diagonal_partial_independence line 127

    Source documentation

    A genuine diagonal sequence for a countable family of varying centered contractions; the coefficient at stage j may depend on j. This is still a partial-unitary construction, not a full free Haar unitary.

    theorem exists_diagonal_partial_independence
    (x : ℕ → ℕ → M.toStarSubalgebra) (hx : ∀ i j,‖x i j‖ ≤ 1)
    (hc : ∀ i j,τ.trace (x i j)=0) :
    ∃ v : ℕ → PartialUnitary M,∀ j,
      (v j).val.val ∈ N ∧ 1/4 < (τ.trace (v j).support.val).re ∧
      ∀ a ∈ (diagonalCoefficientFamily x j : Set M.toStarSubalgebra) ∪ {1},
      ∀ xs : List (Bool × M.toStarSubalgebra),
        1 ≤ xs.length → xs.length ≤ j+1 →
        patchingCoefficients (diagonalCoefficientFamily x j : Set M.toStarSubalgebra) xs →
        ‖τ.trace (a*patchingWord (v j).val xs)‖ ≤ 1/((j : ℝ)+1) := by
…

    Mentions: OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.diagonalCoefficientFamily, OAI.Generator.Tracial.patchingCoefficients, OAI.Generator.Tracial.patchingWord

  12. def OAI.Generator.Tracial.indexedCoefficient line 167
  13. theorem OAI.Generator.Tracial.eventually_list_indices line 172
  14. theorem OAI.Generator.Tracial.eventually_indexedCoefficient line 182
  15. theorem OAI.Generator.Tracial.exists_countable_partial_independence line 205

    Source documentation

    Every nonempty source word is encoded by its internal index list, final sign and two optional endpoint indices. None represents exactly the unit.

    theorem exists_countable_partial_independence
    (x : ℕ → ℕ → M.toStarSubalgebra) (hx : ∀ i j,‖x i j‖ ≤ 1)
    (hc : ∀ i j,τ.trace (x i j)=0) :
    ∃ v : ℕ → PartialUnitary M,
      (∀ j,(v j).val.val ∈ N) ∧ (∀ j,1/4 < (τ.trace (v j).support.val).re) ∧
      ∀ first last : Option ℕ,∀ xs : List (Bool × ℕ),∀ s : Bool,
        Tendsto (fun j => τ.trace (indexedCoefficient x j first * patchingWord (v j).val
          (xs.map (fun a => (a.1,x a.2 j)) ++ [(s,indexedCoefficient x j last)]))) atTop (𝓝 0) := by
…

    Mentions: OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.indexedCoefficient, OAI.Generator.Tracial.patchingWord

  16. def OAI.Generator.Tracial.boundedPartialUnitary line 242
  17. def OAI.Generator.Tracial.boundedPartialSupport line 245
  18. theorem OAI.Generator.Tracial.boundedPartialSupport_projection line 248
  19. theorem OAI.Generator.Tracial.boundedPartialUnitary_initial line 258
  20. theorem OAI.Generator.Tracial.boundedPartialUnitary_final line 264
  21. theorem OAI.Generator.Tracial.boundedPartialUnitary_inclusion line 270
  22. theorem OAI.Generator.Tracial.quotient_ordered_moment_zero line 277
  23. theorem OAI.Generator.Tracial.algebraPatchingWord_scale line 318
  24. theorem OAI.Generator.Tracial.optionalCoefficient_scale line 332
  25. theorem OAI.Generator.Tracial.ordered_moment_scale line 337