Parameters.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Parameter arithmetic for the samplers

The manuscript's padding and rare tabulation estimates give explicit inequalities for successful unpadding and expected correction cost.

theorem OAI.ContingencyTables.padding_error_le_half line 18

theorem OAI.ContingencyTables.padding_success_half line 40

Source documentation

For the actual choices L=d¹², U=d²⁰, the uniform padded table unpads successfully with probability at least one half.

theorem padding_success_half {I J : Type*} [Fintype I] [Fintype J]
    [DecidableEq I] [DecidableEq J]
    (r : I → ℕ) (c : J → ℕ) (htotal : ∑ i, r i = ∑ j, c j)
    (K : Finset (I × J)) (d : ℕ) (hd : 14 ≤ d)
    (hrows : Fintype.card I ≤ d) (hcols : Fintype.card J ≤ d)
    (hK : K.card ≤ d) (hrow : ∀ p ∈ K, d ^ 20 ≤ r p.1)
    (hcol : ∀ p ∈ K, d ^ 20 ≤ c p.2) :
    (1 / 2 : ℝ) ≤ (Fintype.card (Table r c) : ℝ) /
      Fintype.card (Table (paddedRows r (largePadding K (d ^ 12)))
        (paddedColumns c (largePadding K (d ^ 12)))) := by
…

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

theorem OAI.ContingencyTables.rare_tabulation_exponent line 71
Source documentation
The exponentially costly exact tabulation branch has exponentially smaller probability for the manuscript's D=d⁶b².
```
theorem rare_tabulation_exponent (d b : ℕ) (hd : 14 ≤ d) (_hb : 1 ≤ b) :
    500 * d * b ≤ d ^ 6 * b ^ 2 := by
…
```
theorem OAI.ContingencyTables.rare_tabulation_cost line 83