OAI/Analysis/FactorGeneration/HaarSequences.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

One constructed Haar extension retains endpoint moments, represented norm-closed freeness, and an actual unitary sequence in the included algebra.

  1. def OAI.Generator.Tracial.HaarEndpoints line 20

    Source documentation

    Full endpoint formula; the internal factors alone must be centered.

    def HaarEndpoints (D : Subalgebra ℂ (Q τ ω)) (t : unitary (Q τ ω)) : Prop :=
…

    Mentions: OAI.Generator.Tracial.Q

  2. theorem OAI.Generator.Tracial.HaarEndpoints.haar line 25
  3. theorem OAI.Generator.Tracial.HaarEndpoints.representedFree line 31
  4. structure OAI.Generator.Tracial.CoordinateHaarData line 43
  5. theorem OAI.Generator.Tracial.nonempty_coordinateHaarData line 62
  6. def OAI.Generator.Tracial.SamePowerSign line 78
  7. def OAI.Generator.Tracial.ReducedIntegerGaps line 80
  8. theorem OAI.Generator.Tracial.integerValueWord_mul_power line 85
  9. theorem OAI.Generator.Tracial.reduced_integer_gap_functional line 93

    Source documentation

    Prefixes are absorbed into an arbitrary linear functional. Its centered endpoint property is preserved when a centered gap is appended.

    theorem reduced_integer_gap_functional (D : Subalgebra ℂ (Q τ ω))
    (t : unitary (Q τ ω)) (L : Q τ ω →ₗ[ℂ] ℂ)
    (hm : ∀ b ∈ D,∀ n : ℤ,n ≠ 0 → ∀ xs : List (Q τ ω × ℤ),
      (∀ z ∈ xs,z.1 ∈ D ∧ quotientTrace τ ω z.1=0 ∧ z.2 ≠ 0) →
      L (integerValueWord τ ω t n xs b)=0)
    (n : ℤ) (hn : n ≠ 0) (xs : List (Q τ ω × ℤ))
    (hx : ReducedIntegerGaps τ ω D n xs) (b : Q τ ω) (hb : b ∈ D) :
    L (integerValueWord τ ω t n xs b)=0 := by
…

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.integerValueWord, OAI.Generator.Tracial.ReducedIntegerGaps

  10. theorem OAI.Generator.Tracial.HaarEndpoints.reduced_gaps line 150
  11. def OAI.Generator.Tracial.signExponent line 163
  12. theorem OAI.Generator.Tracial.signedLetter_integer line 165
  13. def OAI.Generator.Tracial.SignedReducedGaps line 173
  14. theorem OAI.Generator.Tracial.betweenWord_integerValue line 177
  15. theorem OAI.Generator.Tracial.signedReducedGaps_integer line 185
  16. theorem OAI.Generator.Tracial.HaarEndpoints.signed_gaps line 200
  17. theorem OAI.Generator.Tracial.signedReducedGaps_repeat line 209
  18. theorem OAI.Generator.Tracial.signedReducedGaps_blocks line 219
  19. theorem OAI.Generator.Tracial.integerValueWord_blocks line 232
  20. def OAI.Generator.Tracial.absorbedGapList line 251
  21. theorem OAI.Generator.Tracial.betweenWord_absorb_left line 255
  22. theorem OAI.Generator.Tracial.absorbedGapList_reduced line 269
  23. theorem OAI.Generator.Tracial.HaarEndpoints.mul_left_signed line 295
  24. theorem OAI.Generator.Tracial.HaarEndpoints.mul_left line 312
  25. theorem OAI.Generator.Tracial.integerValueWord_inv line 324
  26. theorem OAI.Generator.Tracial.HaarEndpoints.inv line 332
  27. theorem OAI.Generator.Tracial.HaarEndpoints.mul_right line 341
  28. theorem OAI.Generator.Tracial.HaarEndpoints.absorb line 348
  29. structure OAI.Generator.Tracial.SuccessiveCoordinateHaar line 362
  30. theorem OAI.Generator.Tracial.nonempty_successiveCoordinateHaar line 381
  31. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.monotone line 410
  32. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.seed_mem line 417
  33. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.previous_mem line 424
  34. def OAI.Generator.Tracial.prefixVariable line 438
  35. def OAI.Generator.Tracial.prefixProduct line 442
  36. theorem OAI.Generator.Tracial.prefixProduct_formula line 446
  37. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.variable_mem line 458
  38. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.prefix_mem line 465
  39. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.variable_endpoints line 473
  40. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.prefix_endpoints line 481
  41. theorem OAI.Generator.Tracial.SuccessiveCoordinateHaar.target_endpoints line 487
  42. theorem OAI.Generator.Tracial.exists_perturbation_haar_system line 504