OAI/Combinatorics/ContingencyTables/Dense/DenseScales.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integer bin widths for dense blocks

The free-cell width is the actual integer quotient floor(s/B), where s=min(Rᵢ,Pⱼ). Large margins give the two-sided scale comparison used in the dense rejection sampler.

  1. theorem OAI.ContingencyTables.DenseAffine.integer_width_bounds line 16
  2. theorem OAI.ContingencyTables.DenseAffine.dense_width_positive line 28
  3. theorem OAI.ContingencyTables.DenseAffine.dense_width_bounds line 36
  4. theorem OAI.ContingencyTables.DenseAffine.dense_exponent_change_scale line 52

    Source documentation

    The product A*d/B=d⁻³ is at most one with the actual integer parameter choices. This controls the density within each unit bin.

    theorem dense_exponent_change_scale (d : ℕ) (hd : 14 ≤ d) :
    (d : ℝ) ^ 4 * d / (d : ℝ) ^ 8 ≤ 1 := by
…