OAI/Algebra/GroupRing/PartitionEntropy.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TorsionFreeZeroDivisors.PartitionEntropy.mean_bound line 23

   Source documentation

   A complete literal-stage first moment, with its signed vertex exponent and the source denominator, without stage independence.

   theorem mean_bound (cmp : Comparisons (E := E) (traversalLength len m))
   …

2. abbrev OAI.TorsionFreeZeroDivisors.SideRestriction.Vertex line 66
3. abbrev OAI.TorsionFreeZeroDivisors.SideRestriction.Dart line 67
4. def OAI.TorsionFreeZeroDivisors.SideRestriction.graph line 68
5. def OAI.TorsionFreeZeroDivisors.SideRestriction.vertex line 79
6. def OAI.TorsionFreeZeroDivisors.SideRestriction.dart line 80
7. lemma OAI.TorsionFreeZeroDivisors.SideRestriction.origin_map line 83
8. lemma OAI.TorsionFreeZeroDivisors.SideRestriction.reverse_map line 87
9. def OAI.TorsionFreeZeroDivisors.SideRestriction.embedding line 98

   Source documentation

   Restrict a realized prescribed side to an injectively immersed subgraph whose target vertices really lie on that side.

   def embedding (e : RealizationTransport.Embedding (graph Γ side hs b) (fun d => label d.val)
       outgoing pin bar r) (pin' : QV → Option TV)
       (hp : ∀ v y,pin' v=some y → pin (vertex side b fv hf v)=some y) :
       RealizationTransport.Embedding Q (label ∘ fd) outgoing pin' bar r :=
   …

   Mentions: OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding, OAI.TorsionFreeZeroDivisors.SideRestriction.graph, OAI.TorsionFreeZeroDivisors.SideRestriction.vertex

10. abbrev OAI.TorsionFreeZeroDivisors.StageSideEmbedding.Chain line 114
11. abbrev OAI.TorsionFreeZeroDivisors.StageSideEmbedding.Vertex line 115
12. abbrev OAI.TorsionFreeZeroDivisors.StageSideEmbedding.length line 116
13. def OAI.TorsionFreeZeroDivisors.StageSideEmbedding.firstPoint line 118
14. def OAI.TorsionFreeZeroDivisors.StageSideEmbedding.lastPoint line 120
15. abbrev OAI.TorsionFreeZeroDivisors.StageSideEmbedding.graph line 122
16. def OAI.TorsionFreeZeroDivisors.StageSideEmbedding.vertex line 127
17. def OAI.TorsionFreeZeroDivisors.StageSideEmbedding.dart line 131
18. lemma OAI.TorsionFreeZeroDivisors.StageSideEmbedding.vertex_injective line 135
19. lemma OAI.TorsionFreeZeroDivisors.StageSideEmbedding.dart_injective line 155
20. lemma OAI.TorsionFreeZeroDivisors.StageSideEmbedding.point_map line 166
21. lemma OAI.TorsionFreeZeroDivisors.StageSideEmbedding.origin_map line 174
22. lemma OAI.TorsionFreeZeroDivisors.StageSideEmbedding.reverse_map line 183
23. def OAI.TorsionFreeZeroDivisors.StageSideEmbedding.restrictWord line 187

    Source documentation

    Restriction of a full stage string to this prescribed side.

    def restrictWord (F : ComparedBlocks.Position (StageExpectation.activeLen len m j) → WordEstimate.Letter) :
        ComparedBlocks.Position (length len m j side b) → WordEstimate.Letter :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ComparedBlocks.Position, OAI.TorsionFreeZeroDivisors.StageExpectation.activeLen, OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.StageSideEmbedding.length

24. lemma OAI.TorsionFreeZeroDivisors.StageSideEmbedding.label_map line 191
25. lemma OAI.TorsionFreeZeroDivisors.StageSideEmbedding.chain_card line 203

    Source documentation

    Exact partitions; no isolated vertices from inactive stages are introduced.

    lemma chain_card : Fintype.card (Chain m j side true)+Fintype.card (Chain m j side false)=
        Fintype.card {c // j < m c} := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageSideEmbedding.Chain

26. lemma OAI.TorsionFreeZeroDivisors.StageSideEmbedding.vertex_card line 233
27. def OAI.TorsionFreeZeroDivisors.ChainSide.chain line 254
28. lemma OAI.TorsionFreeZeroDivisors.ChainSide.next_side line 257
29. lemma OAI.TorsionFreeZeroDivisors.ChainSide.iterate_side line 263
30. lemma OAI.TorsionFreeZeroDivisors.ChainSide.suppressed_side line 269
31. lemma OAI.TorsionFreeZeroDivisors.ChainSide.first_side line 277
32. lemma OAI.TorsionFreeZeroDivisors.ChainSide.last_side line 279
33. def OAI.TorsionFreeZeroDivisors.ChainSide.vertex line 287
34. lemma OAI.TorsionFreeZeroDivisors.ChainSide.active_first line 289
35. lemma OAI.TorsionFreeZeroDivisors.ChainSide.active_last line 292
36. lemma OAI.TorsionFreeZeroDivisors.ChainSide.stage_internal line 296
37. abbrev OAI.TorsionFreeZeroDivisors.ActualSideRealization.length line 322
38. abbrev OAI.TorsionFreeZeroDivisors.ActualSideRealization.Marked line 323
39. abbrev OAI.TorsionFreeZeroDivisors.ActualSideRealization.graph line 324
40. def OAI.TorsionFreeZeroDivisors.ActualSideRealization.vertexMap line 328
41. def OAI.TorsionFreeZeroDivisors.ActualSideRealization.dartMap line 331
42. lemma OAI.TorsionFreeZeroDivisors.ActualSideRealization.vertex_injective line 334
43. lemma OAI.TorsionFreeZeroDivisors.ActualSideRealization.dart_injective line 337
44. lemma OAI.TorsionFreeZeroDivisors.ActualSideRealization.origin_map line 341
45. lemma OAI.TorsionFreeZeroDivisors.ActualSideRealization.reverse_map line 348
46. lemma OAI.TorsionFreeZeroDivisors.ActualSideRealization.vertex_side line 356
47. def OAI.TorsionFreeZeroDivisors.ActualSideRealization.word line 364
48. lemma OAI.TorsionFreeZeroDivisors.ActualSideRealization.label_eq line 367
49. def OAI.TorsionFreeZeroDivisors.ActualSideRealization.embedding line 384

    Source documentation

    The literal realization of this prescribed-side active stage follows from an actual embedding of the original prescribed side. All labels stay the restrictions of ONE global word.

    def embedding (e : RealizationTransport.Embedding (SideRestriction.graph Γ side hs b)
          (fun d => label d.val) outgoing pin Types.inverse r)
        (hlabel : ∀ d,label (Γ.reverse d)=Types.inverse (label d))
        (pin' : Marked Γ mark h2 side paths j b → Option TV)
        (hp : ∀ v y,pin' v=some y → pin ⟨v.val.val,v.property⟩=some y) :
        RealizationTransport.Embedding (Q)
          (ChainRealization.label l (StageExpectation.readWord l (word Γ mark h2 side paths j b label)))
          outgoing (ChainRealization.pin l pin') Types.inverse r := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding, OAI.TorsionFreeZeroDivisors.SideRestriction.graph, OAI.TorsionFreeZeroDivisors.Types.inverse, OAI.TorsionFreeZeroDivisors.ActualSideRealization.Marked, OAI.TorsionFreeZeroDivisors.ChainRealization.label, OAI.TorsionFreeZeroDivisors.StageExpectation.readWord, OAI.TorsionFreeZeroDivisors.ActualSideRealization.word, OAI.TorsionFreeZeroDivisors.ChainRealization.pin