OAI/Analysis/FactorGeneration/LaurentMoments.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Generator.Tracial.traceClosedSpan line 19
2. theorem OAI.Generator.Tracial.sandwich_trace_inner line 22
3. theorem OAI.Generator.Tracial.sandwich_trace_closedSpan line 26
4. def OAI.Generator.Tracial.integerValueWord line 46
5. theorem OAI.Generator.Tracial.integerValueWord_indexed line 50
6. theorem OAI.Generator.Tracial.integerValueWord_closedSpan line 59

   Source documentation

   All internal coefficients are extended one at a time, with the other factors fixed. Uniform bounds on simultaneous approximants are unnecessary.

   theorem integerValueWord_closedSpan (v : unitary (Q τ ω)) (x : ℕ → Q τ ω)
       (a b : Q τ ω) (n : ℤ) (xs : List (Q τ ω × ℤ))
       (hxs : ∀ z ∈ xs,z.1 ∈ traceClosedSpan τ ω (Set.range x))
       (hm : ∀ is : List ℕ,is.length=xs.length →
         quotientTrace τ ω (a*integerWord v x n (is.zip (xs.map Prod.snd)) b)=0) :
       quotientTrace τ ω (a*integerValueWord τ ω v n xs b)=0 := by
   …

   Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.traceClosedSpan, OAI.Generator.Tracial.integerWord, OAI.Generator.Tracial.integerValueWord

7. theorem OAI.Generator.Tracial.optionalCoefficient_range line 82

   Source documentation

   The optional endpoints span the unit and the given centered family.

   theorem optionalCoefficient_range (x : ℕ → Q τ ω) :
       Set.range (optionalCoefficient x)=insert 1 (Set.range x) := by
   …

   Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.optionalCoefficient

8. theorem OAI.Generator.Tracial.integerWord_right_factor line 93
9. theorem OAI.Generator.Tracial.integerWord_closed_endpoints line 103
10. theorem OAI.Generator.Tracial.reduced_integer_moment_closedSpan line 131
11. theorem OAI.Generator.Tracial.exists_centered_dense_quotient_family line 157
12. theorem OAI.Generator.Tracial.subalgebra_mem_centered_closedSpan line 171
13. theorem OAI.Generator.Tracial.included_haar_endpoint_moments_of_dense_family line 202
14. theorem OAI.Generator.Tracial.exists_included_haar_endpoint_moments line 224
15. theorem OAI.Generator.Tracial.trace_product_closedSpan line 246
16. def OAI.Generator.Tracial.nonzeroPowerSet line 270
17. def OAI.Generator.Tracial.alternatingFactors line 273
18. def OAI.Generator.Tracial.alternatingPowerSets line 277
19. theorem OAI.Generator.Tracial.alternatingFactors_closedSpan line 281
20. theorem OAI.Generator.Tracial.alternatingPowerSets_integerWord line 294
21. theorem OAI.Generator.Tracial.endpoint_moments_laurent_closure line 330

    Source documentation

    Extends the actual nonzero-exponent formula to arbitrary closed-span combinations in every Haar slot, while retaining arbitrary endpoints in D.

    theorem endpoint_moments_laurent_closure (D : Subalgebra ℂ (Q τ ω))
        (v : unitary (Q τ ω))
        (hm : ∀ a ∈ D,∀ b ∈ D,∀ n : ℤ,n ≠ 0 → ∀ xs : List (Q τ ω × ℤ),
          (∀ z ∈ xs,z.1 ∈ D ∧ quotientTrace τ ω z.1=0 ∧ z.2 ≠ 0) →
          quotientTrace τ ω (a*integerValueWord τ ω v n xs b)=0)
        (a b q : Q τ ω) (ha : a ∈ D) (hb : b ∈ D)
        (hq : q ∈ traceClosedSpan τ ω (nonzeroPowerSet τ ω v))
        (xs : List (Q τ ω × Q τ ω))
        (hxs : ∀ z ∈ xs,z.1 ∈ D ∧ quotientTrace τ ω z.1=0 ∧
          z.2 ∈ traceClosedSpan τ ω (nonzeroPowerSet τ ω v)) :
        quotientTrace τ ω (a*(alternatingFactors τ ω q xs b).prod)=0 := by
    …

    Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.integerValueWord, OAI.Generator.Tracial.traceClosedSpan, OAI.Generator.Tracial.nonzeroPowerSet, OAI.Generator.Tracial.alternatingFactors

22. theorem OAI.Generator.Tracial.exists_included_haar_laurent_moments line 370
23. theorem OAI.Generator.Tracial.alternating_tail_normal_form line 393
24. theorem OAI.Generator.Tracial.endpoint_all_alternating line 412