OAI/Analysis/FactorGeneration/FreeWords.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Generator.freePrefix line 17
2. def OAI.Generator.prefixRatio line 21
3. def OAI.Generator.exponentCoordinate line 23
4. theorem OAI.Generator.freePrefix_eq_prod line 26
5. theorem OAI.Generator.exponentCoordinate_prefix line 32
6. theorem OAI.Generator.exponentCoordinate_ratio line 42
7. theorem OAI.Generator.indicator_difference_injective line 49

   Source documentation

   Two differences of initial-segment indicators identify their endpoints, provided the first interval is nonempty.

   theorem indicator_difference_injective {k j k' j' : ℕ} (hkj : k ≠ j)
       (h : ∀ i : ℕ, (if i < k then (1 : ℤ) else 0) - (if i < j then 1 else 0) =
         (if i < k' then 1 else 0) - (if i < j' then 1 else 0)) :
       k = k' ∧ j = j' := by
   …

8. theorem OAI.Generator.prefixRatio_injective_offDiagonal line 59
9. theorem OAI.Generator.freePrefix_injective line 66
10. theorem OAI.Generator.prefixRatio_eq_one_iff line 73
11. def OAI.Generator.pairRatio line 82
12. theorem OAI.Generator.pairRatio_eq_one_iff line 85
13. theorem OAI.Generator.pairRatio_injective_offDiagonal line 89
14. def OAI.Generator.multiplicity line 99
15. def OAI.Generator.ratioLabels line 103
16. theorem OAI.Generator.multiplicity_one line 107
17. theorem OAI.Generator.multiplicity_offDiagonal line 115
18. theorem OAI.Generator.ratioLabels_eq_image line 126

    Source documentation

    For n > 0 this is exactly the image of all ordered pairs in the source.

    theorem ratioLabels_eq_image {n : ℕ} (hn : 0 < n) :
        ratioLabels n = (Finset.univ : Finset (Fin n × Fin n)).image pairRatio := by
    …

    Mentions: OAI.Generator.ratioLabels, OAI.Generator.pairRatio

19. theorem OAI.Generator.multiplicity_square_sum line 141

    Source documentation

    n_e = n and every off-diagonal label has multiplicity one.

    theorem multiplicity_square_sum (n : ℕ) :
        ∑ p ∈ ratioLabels n, multiplicity n p ^ 2 = 2 * n ^ 2 - n := by
    …

    Mentions: OAI.Generator.ratioLabels, OAI.Generator.multiplicity

20. def OAI.Generator.prefixes line 170
21. theorem OAI.Generator.conjugate_list_prod line 174
22. theorem OAI.Generator.prefix_perturbation line 183
23. theorem OAI.Generator.prefix_perturbation_terminal line 198

    Source documentation

    The exact prefix cancellation identity with the unperturbed terminal factor.

    theorem prefix_perturbation_terminal (ss : List G) (h terminal : G) :
        ((prefixes ss).map (fun g => g * h * g⁻¹)).prod * (ss.prod * terminal) =
          (ss.map (fun s => s * h)).prod * terminal := by
    …

    Mentions: OAI.Generator.prefixes