DenseRegularity.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Regularity of the dense sampler's actual penalty

The natural margins, maximum pivots, integer quotient widths, and actual parameters A=d⁴, B=d⁸ determine the penalty. Its regularity and scaled change bounds follow from the normalized affine coefficients.

def OAI.ContingencyTables.DenseAffine.denseWidth line 18
def OAI.ContingencyTables.DenseAffine.densePenalty line 21
theorem OAI.ContingencyTables.DenseAffine.dense_cellScale_pos line 31
theorem OAI.ContingencyTables.DenseAffine.dense_normalized_coeff_bound line 41
theorem OAI.ContingencyTables.DenseAffine.densePenalty_continuous line 56
theorem OAI.ContingencyTables.DenseAffine.densePenalty_convex line 59

theorem OAI.ContingencyTables.DenseAffine.densePenalty_scaled_change line 66

Source documentation

A coordinate displacement at most r changes the actual scaled penalty A*p by at most r. In particular this is at most one in a bin and at most two in the cut-face tubes.

theorem densePenalty_scaled_change (R : Option I → ℕ) (P : Option J → ℕ)
    (d : ℕ) (hd : 14 ≤ d) (hR : ∀ i, d ^ 12 ≤ R i) (hP : ∀ j, d ^ 12 ≤ P j)
    (hRmax : ∀ i, R (some i) ≤ R none) (hPmax : ∀ j, P (some j) ≤ P none)
    (hfree : Fintype.card (I × J) ≤ d) (x y : I × J → ℝ) (r : ℝ) (hr : 0 ≤ r)
    (hxy : ∀ p, |x p - y p| ≤ r) :
    |(d : ℝ) ^ 4 * densePenalty R P d x - (d : ℝ) ^ 4 * densePenalty R P d y| ≤ r := by
…

Mentions: OAI.ContingencyTables.DenseAffine.densePenalty