GridMinCut.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Every nontrivial cut of the actual dense grid

Choosing the smaller continuous side and then comparing its own discrete mass gives a lower bound using the smaller discrete side. No assumption identifying those two choices is made.

def OAI.ContingencyTables.GridBoundary.cutComplementEquiv line 25
theorem OAI.ContingencyTables.GridBoundary.cut_complement_sum line 32
theorem OAI.ContingencyTables.GridBoundary.weighted_min_cut line 37

theorem OAI.ContingencyTables.GridBoundary.denseGrid_min_cut line 83

Source documentation

The actual dense sampler's dyadic weights satisfy every nontrivial cut bound, with the manuscript interpolation parameter.

theorem denseGrid_min_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) (hK : 1 ≤ K)
    (Q : (Fin q → ℤ) → Prop)
    (hne : Nonempty (Selected K Q)) (hne' : Nonempty (Selected K (fun a => ¬ Q a))) :
    (1 / (128 * (d : ℝ) * K)) * min
        (∑ a : Selected K Q, DenseWeights.binWeight ((d : ℝ) ^ 4)
          (denseGridPenalty R P d e) (realCorner a.val))
        (∑ a : Selected K (fun b => ¬ Q b), DenseWeights.binWeight ((d : ℝ) ^ 4)
          (denseGridPenalty R P d e) (realCorner a.val)) ≤
…

Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.GridBoundary.Selected, OAI.ContingencyTables.DenseWeights.binWeight, OAI.ContingencyTables.GridBoundary.denseGridPenalty, OAI.ContingencyTables.GridBoundary.realCorner