OAI/Algebra/GroupRing/EntropyStages.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

The actual common-grid block matching of an affine comparison system. Positions are the literal half-integer edge indices within each traversal.

  1. structure OAI.TorsionFreeZeroDivisors.EntropyStages.Pairing line 9
  2. structure OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data line 19
  3. def OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.slice line 35

    Source documentation

    The positions of one comparison side in a pair of occurrence blocks.

    def slice (e : E) (o p : B) : Finset Ω :=
…
  4. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.slice_mem line 38
  5. def OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.reverseSlice line 42
  6. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.slice_card line 53
  7. def OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.Joined line 56
  8. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.joined_symm line 62
  9. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.joined_ne line 67
  10. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.joined_unique line 83
  11. def OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.partner line 97
  12. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.partner_spec line 99
  13. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.partner_involutive line 104
  14. def OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.matching line 111
  15. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.matched_iff line 113
  16. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.unmatched_iff line 123
  17. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.joined_of_small_deficit line 127

    Source documentation

    Explicit error criterion usable with the half-integer alignment lemma.

    theorem joined_of_small_deficit {o p : B} {e : E}
    (hbig_o : 2*D.error < (D.positions o).card) (hbig_p : 2*D.error < (D.positions p).card)
    (hdef_o : (D.positions o).card-(D.slice e o p).card ≤ D.error)
    (hdef_p : (D.positions p).card-(D.slice e o p).card ≤ D.error) : D.Joined o p := by
…
  18. def OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.unmatchedBlocks line 136
  19. def OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.unpairedPositions line 137
  20. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.unmatched_mass line 141

    Source documentation

    The source unmatched-block charge, with every rounding/cut error explicit. Only the stated local geometric coverage of nonexceptional blocks is needed.

    theorem unmatched_mass (s : ℝ) (hs : 0 ≤ s) (exceptional : Finset B)
    (hsize : ∀ o, s-1 ≤ ((D.positions o).card : ℝ))
    (hcover : ∀ o, D.matching.partner o = o → o ∉ exceptional →
      D.positions o ⊆ D.unpairedPositions) :
    s*(D.unmatchedBlocks.card : ℝ) ≤ (D.unpairedPositions.card : ℝ) +
      s*exceptional.card + Fintype.card B := by
…
  21. abbrev OAI.TorsionFreeZeroDivisors.ComparedBlocks.Position line 182
  22. abbrev OAI.TorsionFreeZeroDivisors.ComparedBlocks.Block line 183
  23. def OAI.TorsionFreeZeroDivisors.ComparedBlocks.includeBlock line 187
  24. def OAI.TorsionFreeZeroDivisors.ComparedBlocks.blockPositions line 193
  25. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.mem_blockPositions line 196
  26. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.blockPositions_card line 208
  27. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.blockPositions_disjoint line 212
  28. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.fullIndex line 227

    Source documentation

    Exact full-grid-index converse, rather than clipping a target partner.

    theorem fullIndex {t : T} {k : ℤ} (hk : 0 ≤ k)
    (hfull : ((k : ℝ)+1)*s ≤ len t) :
    ∃ j : Fin (blockCount s (len t)), (j.val : ℤ) = k := by
…
  29. structure OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons line 239

    Source documentation

    Data of the original disjoint signed interval comparisons on traversals. The involution and side predicates retain occurrence indices throughout.

    structure Comparisons where
…
  30. def OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.matchingData line 263
  31. def OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.integerSlice line 275

    Source documentation

    The literal integer slice before making any near-full grid approximation.

    def integerSlice (e : E) (b p : Block s len) : Finset ℤ :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.ComparedBlocks.Block

  32. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.slice_sources line 279
  33. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.slice_integer_card line 289
  34. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.side_of_margin line 321

    Source documentation

    The original side comparison covers this entire source block.

    theorem side_of_margin {b : Block s len} {e : E} (hsource : b.1 = C.source e)
    (hlo : C.lo e ≤ (b.2.val : ℝ)*s-s)
    (hhi : ((b.2.val : ℝ)+1)*s+s ≤ C.hi e)
    {x : Position len} (hx : x ∈ blockPositions s hs len b) : C.side x = some e := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ComparedBlocks.Block, OAI.TorsionFreeZeroDivisors.ComparedBlocks.Position, OAI.TorsionFreeZeroDivisors.ComparedBlocks.blockPositions

  35. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.slice_card_eq line 333

    Source documentation

    The full slice is exactly the algebraic source overlap.

    theorem slice_card_eq {b p : Block s len} {e : E} {ν : ℤ}
    (hsource : b.1 = C.source e) (htarget : p.1 = C.source (C.flip e))
    (hindex : (p.2.val : ℤ) = partnerIndex (C.reverse e) ν b.2.val)
    (hlo : C.lo e ≤ (b.2.val : ℝ)*s-s)
    (hhi : ((b.2.val : ℝ)+1)*s+s ≤ C.hi e) :
    ((C.matchingData s hs len err).slice e b p).card =
      (overlap s (C.reverse e) (C.offset e) b.2.val ν).card := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ComparedBlocks.Block

  36. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.joined_of_margin line 368

    Source documentation

    A block deep inside an actual comparison has a near-full selected partner.

    theorem joined_of_margin {b : Block s len} {e : E} {ν : ℤ}
    (hsource : b.1 = C.source e)
    (hsmall : 2*(err : ℝ) < s-1)
    (herr : 2*|(C.offset e : ℝ)-(ν : ℝ)*s|+4 ≤ err)
    (hlo : C.lo e ≤ (b.2.val : ℝ)*s-s)
    (hhi : ((b.2.val : ℝ)+1)*s+s ≤ C.hi e) :
    ∃ p, (C.matchingData s hs len err).Joined b p := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ComparedBlocks.Block

  37. def OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.nearCutBlocks line 413
  38. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.nearCutBlocks_card line 416
  39. def OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.exceptional line 430
  40. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.exceptional_card line 434
  41. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.unmatched_unpaired line 449

    Source documentation

    No point of a deep unmatched block belongs to any original comparison.

    theorem unmatched_unpaired (ν : E → ℤ)
    (hsmall : 2*(err : ℝ) < s-1)
    (herr : ∀ e, 2*|(C.offset e : ℝ)-(ν e : ℝ)*s|+4 ≤ err)
    {b : Block s len} (hb : (C.matchingData s hs len err).matching.partner b = b)
    (hn : b ∉ C.exceptional s len) :
    blockPositions s hs len b ⊆ (C.matchingData s hs len err).unpairedPositions := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ComparedBlocks.Block, OAI.TorsionFreeZeroDivisors.ComparedBlocks.blockPositions

  42. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.block_mass line 483

    Source documentation

    The full block mass and hence the rounding charge use the total actual traversal length, with no prescribed occurrence-count estimate.

    theorem block_mass : s*(Fintype.card (Block s len) : ℝ) ≤ ∑ t, (len t : ℝ) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ComparedBlocks.Block

  43. theorem OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.unmatched_bound line 491