OAI/Combinatorics/BinaryEdit/SegmentMatchingCount.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TreeEdit.BinaryLower.RandomMatching.IncreasingPositions line 8

   Source documentation

   A choice of positions for a subsequence, in their original order.

   abbrev IncreasingPositions (a s : ℕ) := {f : Fin s → Fin a // StrictMono f}

2. def OAI.TreeEdit.BinaryLower.RandomMatching.increasingPositionsEquiv line 10
3. theorem OAI.TreeEdit.BinaryLower.RandomMatching.card_increasingPositions line 29
4. def OAI.TreeEdit.BinaryLower.RandomMatching.segmentMatchingEvent line 36

   Source documentation

   The event that two fixed windows admit a matching of size s.

   noncomputable def segmentMatchingEvent {K P a : ℕ} (s : ℕ)
       (i j : Fin K) (u v : Fin a → Fin P) :
       Finset (Fin K → Fin P → Bool) := by
   …

5. theorem OAI.TreeEdit.BinaryLower.RandomMatching.card_segmentMatchingEvent_le line 44

   Source documentation

   Finite union estimate for one pair of unequal-label windows.

   theorem card_segmentMatchingEvent_le {K P a s : ℕ}
       (i j : Fin K) (hne : i ≠ j) (u v : Fin a → Fin P)
       (hv : Function.Injective v) :
       (segmentMatchingEvent s i j u v).card ≤
         (a.choose s) ^ 2 * 2 ^ (K * P - s) := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.RandomMatching.segmentMatchingEvent

6. theorem OAI.TreeEdit.BinaryLower.RandomMatching.segmentMatchingEvent_fraction_le line 76

   Source documentation

   The fixed-window union bound in normalized counting-measure form.

   theorem segmentMatchingEvent_fraction_le {K P a s : ℕ}
       (i j : Fin K) (hne : i ≠ j) (u v : Fin a → Fin P)
       (hv : Function.Injective v) (hs : s ≤ a) :
       ((segmentMatchingEvent s i j u v).card : ℝ) / (2 : ℝ) ^ (K * P) ≤
         ((a.choose s : ℝ) ^ 2) / (2 : ℝ) ^ s := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.RandomMatching.segmentMatchingEvent