SmallEntries.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Four-cycle moves for the small-entry estimate

The move raises the marked cell, lowers one donor in its row and one in its column, and raises the opposite corner. No upper cell bound is used.

def OAI.ContingencyTables.fourCycleInt line 24
Source documentation
The signed four-cycle update, before converting back to natural entries.
```
def fourCycleInt (X : I → J → ℕ) (a b : I) (s t : J) (v : ℕ) (i : I) (j : J) : ℤ :=
…
```
theorem OAI.ContingencyTables.fourCycleInt_nonnegative line 29
theorem OAI.ContingencyTables.fourCycleInt_rows line 57
theorem OAI.ContingencyTables.fourCycleInt_columns line 63

def OAI.ContingencyTables.fourCycle line 69

Source documentation

A nonnegative four-cycle is again a table with precisely the same margins.

def fourCycle {r : I → ℕ} {c : J → ℕ} (X : Table r c)
    (a b : I) (s t : J) (v : ℕ) (hab : a ≠ b) (hst : s ≠ t)
    (hrow : v ≤ X.val a t) (hcol : v ≤ X.val b s) : Table r c := by
…

Mentions: OAI.ContingencyTables.Table

theorem OAI.ContingencyTables.fourCycle_cast line 87
theorem OAI.ContingencyTables.fourCycle_marked line 94

theorem OAI.ContingencyTables.fourCycle_injective line 103

Source documentation

With the donor labels and step fixed, the target determines the source.

theorem fourCycle_injective {r : I → ℕ} {c : J → ℕ}
    (X Y : Table r c) (a b : I) (s t : J) (v : ℕ) (hab : a ≠ b) (hst : s ≠ t)
    (hXrow : v ≤ X.val a t) (hXcol : v ≤ X.val b s)
    (hYrow : v ≤ Y.val a t) (hYcol : v ≤ Y.val b s)
    (heq : fourCycle X a b s t v hab hst hXrow hXcol =
      fourCycle Y a b s t v hab hst hYrow hYcol) : X = Y := by
…

Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.fourCycle

theorem OAI.ContingencyTables.small_entry_count_of_donors line 119
Source documentation
Double counting the four-cycle moves. The source marked value and two donor labels suffice to reverse a move: the target marked value determines the step. The donor-existence condition is separated from the injection so that the margin estimate can be checked independently.
```
theorem small_entry_count_of_donors {r : I → ℕ} {c : J → ℕ}
    (a : I) (s : J) (t V : ℕ)
    (hdonors : ∀ X : Table r c, X.val a s < t →
      ∃ p : I × J, a ≠ p.1 ∧ s ≠ p.2 ∧ V ≤ X.val a p.2 ∧ V ≤ X.val p.1 s) :
    Fintype.card {X : Table r c // X.val a s < t} * V ≤
      Fintype.card (Table r c) * (Fintype.card I * Fintype.card J * t) := by
…
```
Mentions: OAI.ContingencyTables.Table
theorem OAI.ContingencyTables.donor_from_line line 163

theorem OAI.ContingencyTables.small_entry_count line 194

Source documentation

Margin lower bounds supply the donors for each small marked entry. d * V + t ≤ a₀ is the discrete form of the manuscript's choice V = floor (a₀/(2d)) with 2t ≤ a₀.

theorem small_entry_count {r : I → ℕ} {c : J → ℕ}
    (a : I) (s : J) (a₀ d t V : ℕ)
    (hrows : Fintype.card I ≤ d) (hcols : Fintype.card J ≤ d)
    (hrow : a₀ ≤ r a) (hcol : a₀ ≤ c s)
    (hV : 0 < V) (hscale : d * V + t ≤ a₀) :
    Fintype.card {X : Table r c // X.val a s < t} * V ≤
      Fintype.card (Table r c) * (Fintype.card I * Fintype.card J * t) := by
…

Mentions: OAI.ContingencyTables.Table

theorem OAI.ContingencyTables.small_entry_probability line 214

Source documentation

The complete small-entry estimate of paper 200-01, expressed as the uniform finite counting probability. It also covers zero rows or columns away from the marked cell.

theorem small_entry_probability {r : I → ℕ} {c : J → ℕ}
    (htotal : ∑ i, r i = ∑ j, c j)
    (a : I) (s : J) (a₀ d t : ℕ) (hd : 0 < d)
    (hrows : Fintype.card I ≤ d) (hcols : Fintype.card J ≤ d)
    (hrow : a₀ ≤ r a) (hcol : a₀ ≤ c s)
    (ha₀ : 4 * d ≤ a₀) (ht : 2 * t ≤ a₀) :
    (Fintype.card {X : Table r c // X.val a s < t} : ℝ) /
        Fintype.card (Table r c) ≤ 4 * t * (d : ℝ) ^ 3 / a₀ := by
…

Mentions: OAI.ContingencyTables.Table