OAI/Algebra/GroupRing/PatternUniform.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.PatternUniform.Ready line 14

    Source documentation

    Numerical conditions shared by every bounded pattern, with the threshold chosen before its carrier types, lengths, offsets, words or bin profile.

    def Ready (K M Q J rep : ℕ) : Prop :=
…
  2. theorem OAI.TorsionFreeZeroDivisors.PatternUniform.eventually_ready line 24
  3. theorem OAI.TorsionFreeZeroDivisors.PatternUniform.Ready.residual line 51
  4. def OAI.TorsionFreeZeroDivisors.ActualPatternEvent.Realized line 82

    Source documentation

    The fixed-pattern event before any scale or bins are chosen.

    def Realized (cmp : Comparisons (E:=E) (traversalLength len m)) (r : Match rep) : Prop :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.ActualPatternEvent.Match

  5. lemma OAI.TorsionFreeZeroDivisors.ActualPatternEvent.unbinned_iff line 95
  6. def OAI.TorsionFreeZeroDivisors.ActualPatternEvent.defect line 106
  7. lemma OAI.TorsionFreeZeroDivisors.ActualPatternEvent.uncovered_eq line 110
  8. theorem OAI.TorsionFreeZeroDivisors.ActualPatternEvent.uniform_probability_bound line 119

    Source documentation

    Uniform probability bound with no entropy, moment or scale hypothesis. The ready threshold is independent of all carrier types and pattern data.

    theorem uniform_probability_bound (K Q M J : ℕ) (hM : 0<M)
    (hready : PatternUniform.Ready K M Q J rep)
    (cmp : Comparisons (E:=E) (traversalLength len m))
…

    Mentions: OAI.TorsionFreeZeroDivisors.PatternUniform.Ready

  9. def OAI.TorsionFreeZeroDivisors.OriginalPattern.Realized line 184

    Source documentation

    Literal whole-path comparisons, before cutting at the marked vertices.

    def Realized (patCmp : Comparisons (E:=E) pl) (r : Match rep) : Prop :=
…
  10. def OAI.TorsionFreeZeroDivisors.OriginalPattern.cut line 199

    Source documentation

    The actual cut comparison data, with its carrier exposed once.

    def cut (patCmp : Comparisons (E:=E) pl) (lo hi : E → ℤ)
…
  11. lemma OAI.TorsionFreeZeroDivisors.OriginalPattern.normalized line 205
  12. lemma OAI.TorsionFreeZeroDivisors.OriginalPattern.totalLength_eq line 214
  13. lemma OAI.TorsionFreeZeroDivisors.OriginalPattern.defect_eq line 223
  14. theorem OAI.TorsionFreeZeroDivisors.OriginalPattern.probability_bound line 236

    Source documentation

    The fixed original-path event has the source exponential bound; cuts and orientations are deterministic and do not add any probability factor.

    theorem probability_bound (patCmp : Comparisons (E:=E) pl) (lo hi : E → ℤ)
…
  15. def OAI.TorsionFreeZeroDivisors.ComparisonGeometry.position line 279
  16. structure OAI.TorsionFreeZeroDivisors.ComparisonGeometry.Iso line 282
  17. lemma OAI.TorsionFreeZeroDivisors.ComparisonGeometry.Iso.side_some line 296
  18. lemma OAI.TorsionFreeZeroDivisors.ComparisonGeometry.Iso.side_eq line 302
  19. lemma OAI.TorsionFreeZeroDivisors.ComparisonGeometry.Iso.partner_eq line 315
  20. structure OAI.TorsionFreeZeroDivisors.PortSubdivision.Iso line 335
  21. def OAI.TorsionFreeZeroDivisors.PortSubdivision.Iso.symm line 343
  22. def OAI.TorsionFreeZeroDivisors.PortSubdivision.Iso.trans line 353