OAI/Combinatorics/BinaryEdit/UnequalCounting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.Code.sum_counts_le_of_large_charge line 9

   Source documentation

   Sum the local large-pair charge, allowing a threshold-sized error for every visited block pair. Small pairs need no separation hypothesis.

   theorem sum_counts_le_of_large_charge {β : Type*} (s : Finset β)
       (a g : β → ℕ) (a₀ : ℕ)
       (hlarge : ∀ b ∈ s, a₀ ≤ a b → a b ≤ 100 * g b) :
       (∑ b ∈ s, a b) ≤ 100 * (∑ b ∈ s, g b) + s.card * a₀ := by
   …

2. theorem OAI.TreeEdit.BinaryLower.Code.block_pair_bad_count_le line 26

   Source documentation

   The unequal-label count estimate once the actual segment separation has been applied to each large block pair. All gap terms here are the concrete interval-span losses, rather than arbitrary charged weights.

   theorem block_pair_bad_count_le {r M P : ℕ} (hP : 0 < P)
       (f g : Fin r → Fin (M * P)) (hf : StrictMono f) (hg : StrictMono g)
       (bad : ℕ × ℕ → Prop) [DecidablePred bad] (a₀ : ℕ)
       (hlarge : ∀ b ∈ (Finset.univ.image (fun i => ((f i).val / P, (g i).val / P))).filter bad,
         a₀ ≤ (Finset.univ.filter (fun i => ((f i).val / P, (g i).val / P) = b)).card →
         (Finset.univ.filter (fun i => ((f i).val / P, (g i).val / P) = b)).card ≤
           100 * (((matchingSpan f (fun i => ((f i).val / P, (g i).val / P)) b).card -
             (Finset.univ.filter (fun i => ((f i).val / P, (g i).val / P) = b)).card) +
             ((matchingSpan g (fun i => ((f i).val / P, (g i).val / P)) b).card -
             (Finset.univ.filter (fun i => ((f i).val / P, (g i).val / P) = b)).card))) :
       (Finset.univ.filter (fun i => bad ((f i).val / P, (g i).val / P))).card ≤
         200 * (M * P - r) + 2 * M * a₀ := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.matchingSpan