GridConductance.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Conditional weighted grid-cut estimate

The finite-box Prékopa input is the only published hypothesis here. The shell cover, tube volume, integral cover, and discrete/continuous mass comparison yield the discrete cut estimate.

theorem OAI.ContingencyTables.GridBoundary.weighted_cut_of_interpolation line 22
Source documentation
The actual weighted cut bound before the proposal probability is inserted. The selected side is the smaller continuous side; the conclusion uses its own discrete weight and therefore also bounds the smaller discrete side without identifying the two notions of smaller side.
```
theorem weighted_cut_of_interpolation {q K : ℕ}
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler q)
    (P : (Fin q → ℤ) → Prop) (t : ℝ) (ht : 0 < t) (ht₁ : t < 1)
    (hr : t * K ≤ 1 / 4) (hsize : (q - 1 : ℕ) * (2 * (t * K)) ≤ (1 / 2 : ℝ))
    (ρ : (Fin q → ℝ) → ℝ) (w : Grid (I := Fin q) K → ℝ)
…
```
Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.GridBoundary.Grid