Padding.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Padding and the successful-table bijection

Padding a designated rectangle by a fixed amount gives a bijection from original tables to enlarged-margin tables whose entries dominate the padding. Each successful joint object therefore yields exactly one table.

def OAI.ContingencyTables.paddedRows line 22
def OAI.ContingencyTables.paddedColumns line 23
def OAI.ContingencyTables.padTable line 25
def OAI.ContingencyTables.unpadTable line 36
def OAI.ContingencyTables.paddingEquiv line 54
Source documentation
Successful enlarged tables are in exact bijection with original tables.
```
def paddingEquiv (r : I → ℕ) (c : J → ℕ) (P : I → J → ℕ) :
    Table r c ≃ {Y : Table (paddedRows r P) (paddedColumns c P) //
      ∀ i j, P i j ≤ Y.val i j} where
…
```
Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.paddedRows, OAI.ContingencyTables.paddedColumns
theorem OAI.ContingencyTables.successful_card line 71
theorem OAI.ContingencyTables.card_exists_le_sum line 79
Source documentation
The union bound as an injection with a deterministically chosen bad cell label. This counts each bad table once, even if several entries fail.
```
theorem card_exists_le_sum {α K : Type*} [Fintype α] [Fintype K]
    (P : K → α → Prop) :
    Fintype.card {x : α // ∃ k, P k x} ≤ ∑ k, Fintype.card {x : α // P k x} := by
…
```
theorem OAI.ContingencyTables.fraction_not_exists line 93
def OAI.ContingencyTables.largePadding line 126
theorem OAI.ContingencyTables.large_padding_good_card line 129

theorem OAI.ContingencyTables.padding_success_fraction line 158

Source documentation

The successful enlarged-table fraction is bounded using the proved small-entry estimate and the exact padding bijection. This is the counting part of paper 200-01's stationary-success proposition.

theorem padding_success_fraction (r : I → ℕ) (c : J → ℕ)
    (htotal : ∑ i, r i = ∑ j, c j) (K : Finset (I × J)) (L U d : ℕ)
    (hd : 0 < d) (hrows : Fintype.card I ≤ d) (hcols : Fintype.card J ≤ d)
    (hrow : ∀ p ∈ K, U ≤ r p.1) (hcol : ∀ p ∈ K, U ≤ c p.2)
    (hU : 4 * d ≤ U) (hL : 2 * L ≤ U) :
    1 - K.card * (4 * L * (d : ℝ) ^ 3 / U) ≤
      (Fintype.card (Table r c) : ℝ) /
        Fintype.card (Table (paddedRows r (largePadding K L))
          (paddedColumns c (largePadding K L))) := by
…

Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.paddedRows, OAI.ContingencyTables.largePadding, OAI.ContingencyTables.paddedColumns