CopyBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Counting ordered matrix copies through a constrained cell

The counting injection is independent of the host construction.

theorem OAI.Problem348.CopyBound.card_le_card_mul_pow line 15

Source documentation

If one specified row-column pair in every member of a finite family belongs to L, the family is encoded by that cell and all remaining coordinates.

theorem card_le_card_mul_pow {k n : ℕ}
    (S : Finset
      ({f : Fin (k + 1) → Fin n // StrictMono f} ×
       {f : Fin (k + 1) → Fin n // StrictMono f}))
    (i j : Fin (k + 1)) (L : Finset (Fin n × Fin n))
    (hL : ∀ rc ∈ S, (rc.1.val i, rc.2.val j) ∈ L) :
    S.card ≤ L.card * n ^ (2 * k) := by
…

theorem OAI.Problem348.CopyBound.normalized_count_le line 51

Source documentation

Normalize the integer count bound from the leaf-diagonal argument.

theorem normalized_count_le {count d m : ℕ} (hd : 0 < d) (hm : 0 < m)
    (hcount : count ≤ m * (d * m) ^ 130) :
    (count : ℝ) / (((d * m : ℕ) : ℝ) ^ 132) ≤
      (1 / ((d : ℝ) ^ 2)) * (1 / (m : ℝ)) := by
…