DenseGrid.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Conductance geometry for the actual dense penalty

The free table coordinates are reindexed by Fin q. The bin and cut-tube density comparisons below follow from the actual margins and integer widths. Thus the weighted cut theorem has no assumed penalty regularity or bin comparison when used for the dense completion sampler.

def OAI.ContingencyTables.GridBoundary.realCorner line 25
def OAI.ContingencyTables.GridBoundary.denseGridPenalty line 28
theorem OAI.ContingencyTables.GridBoundary.denseGridPenalty_continuous line 32
theorem OAI.ContingencyTables.GridBoundary.denseGridPenalty_convex line 37
theorem OAI.ContingencyTables.GridBoundary.denseGridPenalty_change line 45
theorem OAI.ContingencyTables.GridBoundary.closedBin_distance line 55
theorem OAI.ContingencyTables.GridBoundary.tube_distances line 63
theorem OAI.ContingencyTables.GridBoundary.denseGrid_bin_comparison line 102
theorem OAI.ContingencyTables.GridBoundary.denseGrid_tube_comparison line 116

theorem OAI.ContingencyTables.GridBoundary.denseGrid_weighted_cut line 138

Source documentation

Actual dyadic dense weights satisfy the interpolation cut bound, conditionally only on the published finite-box integral inequality.

theorem denseGrid_weighted_cut (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) (e : I × J ≃ Fin q)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler q)
    {K : ℕ} (Q : (Fin q → ℤ) → Prop) (t : ℝ) (ht : 0 < t) (ht₁ : t < 1)
    (hr : t * K ≤ 1 / 4) (hsize : (q - 1 : ℕ) * (2 * (t * K)) ≤ (1 / 2 : ℝ))
    (hSmass : 0 < ∫ x in selectedBins K Q,
      DenseWeights.density ((d : ℝ) ^ 4) (denseGridPenalty R P d e) x)
    (hcut : 2 * (∫ x in selectedBins K Q,
      DenseWeights.density ((d : ℝ) ^ 4) (denseGridPenalty R P d e) x) ≤
      ∫ x in {x | Cube K x},
…

Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.GridBoundary.selectedBins, OAI.ContingencyTables.DenseWeights.density, OAI.ContingencyTables.GridBoundary.denseGridPenalty, OAI.ContingencyTables.GridBoundary.Cube