RootedOracleCut.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The selected-root density satisfies the actual weighted grid cut bound

lemma OAI.ContingencyTables.RootedOracleDensity.tube_comparison line 16

theorem OAI.ContingencyTables.RootedOracleDensity.weighted_min_cut line 33

Source documentation

The companion bin weights satisfy the source cut bound directly from their actual forest density and the precise published PL input.

theorem weighted_min_cut (A : Instance I J) (S : RootedCompletion.Selection A.T) (C a : ℝ) (hC : 0 < C)
    (ha : 0 ≤ a) (haH : a ≤ height A C) (z : View A → ℕ)
    (K : ℕ) (hK : 1 ≤ K)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (Q : (Fin (dimension A) → ℤ) → Prop)
    (hne : Nonempty (Selected K Q)) (hne' : Nonempty (Selected K (fun x => ¬Q x))) :
    (1/(128*(A.d:ℝ)*K))*min
        (∑ v : Selected K Q,V A S C a z (realCorner v.val))
        (∑ v : Selected K (fun x => ¬Q x),V A S C a z (realCorner v.val)) ≤
      ∑ e : CutEdge K Q,min (V A S C a z (realCorner e.val.1))
        (V A S C a z (realCorner e.val.2.1)) := by
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.RootedOracleDensity.V