RandomMatching.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact finite counting for the prescribed-match probability in polynomial-code.tex, Lemma lem:random-segments. The constraints identify distinct target coordinates with coordinates outside that target set.

def OAI.TreeEdit.BinaryLower.RandomMatching.constraintEquiv line 19

Source documentation

The coordinates outside the prescribed right endpoints are free.

noncomputable def constraintEquiv
    (l : I → A) (r : I ↪ A) (hdisj : ∀ i j, l i ≠ r j) :
    {f : A → B // ∀ i, f (l i) = f (r i)} ≃
      ({a : A // a ∉ Set.range r} → B) := by
…

theorem OAI.TreeEdit.BinaryLower.RandomMatching.card_constraints line 67

Source documentation

Each independent equality removes exactly one free coordinate.

theorem card_constraints [Fintype A] [Fintype I] [Fintype B]
    (l : I → A) (r : I ↪ A) (hdisj : ∀ i j, l i ≠ r j) :
    Nat.card {f : A → B // ∀ i, f (l i) = f (r i)} =
      Fintype.card B ^ (Fintype.card A - Fintype.card I) := by
…

theorem OAI.TreeEdit.BinaryLower.RandomMatching.card_prescribed_matching line 79
Source documentation
The number of Boolean codebooks realizing one prescribed increasing matching in two different codewords. Only injectivity of target positions is needed; increasing matchings in particular satisfy it.
```
theorem card_prescribed_matching {K P s : ℕ}
    (i j : Fin K) (hne : i ≠ j) (u v : Fin s → Fin P)
    (hv : Function.Injective v) :
    Nat.card {c : Fin K × Fin P → Bool //
      ∀ t, c (i, u t) = c (j, v t)} = 2 ^ (K * P - s) := by
…
```

theorem OAI.TreeEdit.BinaryLower.RandomMatching.card_prescribed_matching_curried line 96

Source documentation

Curried codebooks have the same exact count.

theorem card_prescribed_matching_curried {K P s : ℕ}
    (i j : Fin K) (hne : i ≠ j) (u v : Fin s → Fin P)
    (hv : Function.Injective v) :
    Nat.card {c : Fin K → Fin P → Bool //
      ∀ t, c i (u t) = c j (v t)} = 2 ^ (K * P - s) := by
…

theorem OAI.TreeEdit.BinaryLower.RandomMatching.card_prescribed_matching_mul line 110

Source documentation

Denominator-free form of the probability 2^(-s).

theorem card_prescribed_matching_mul {K P s : ℕ}
    (i j : Fin K) (hne : i ≠ j) (u v : Fin s → Fin P)
    (hv : Function.Injective v) :
    Nat.card {c : Fin K → Fin P → Bool //
      ∀ t, c i (u t) = c j (v t)} * 2 ^ s = 2 ^ (K * P) := by
…

theorem OAI.TreeEdit.BinaryLower.RandomMatching.prescribed_matching_fraction line 123

Source documentation

The fraction of all independent uniform Boolean assignments satisfying a fixed prescribed matching equals 1 / 2^s.

theorem prescribed_matching_fraction {K P s : ℕ}
    (i j : Fin K) (hne : i ≠ j) (u v : Fin s → Fin P)
    (hv : Function.Injective v) :
    (Nat.card {c : Fin K → Fin P → Bool //
      ∀ t, c i (u t) = c j (v t)} : ℝ) / (2 : ℝ) ^ (K * P) =
      1 / (2 : ℝ) ^ s := by
…

theorem OAI.TreeEdit.BinaryLower.RandomMatching.filter_card_prescribed_matching line 135

Source documentation

Finset form, suitable for a finite union bound over forbidden matchings.

theorem filter_card_prescribed_matching {K P s : ℕ}
    (i j : Fin K) (hne : i ≠ j) (u v : Fin s → Fin P)
    (hv : Function.Injective v) :
    (Finset.univ.filter (fun c : Fin K → Fin P → Bool =>
      ∀ t, c i (u t) = c j (v t))).card = 2 ^ (K * P - s) := by
…