OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleCut.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.CompanionOracleDensity.closedBin_distances line 15
2. lemma OAI.ContingencyTables.CompanionOracleDensity.tube_distances line 23
3. lemma OAI.ContingencyTables.CompanionOracleDensity.tube_comparison line 56
4. lemma OAI.ContingencyTables.CompanionOracleDensity.interpolation_bounds line 71
5. theorem OAI.ContingencyTables.CompanionOracleDensity.weighted_min_cut line 95

   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) (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 C a z (realCorner v.val))
           (∑ v : Selected K (fun x => ¬Q x),V A C a z (realCorner v.val)) ≤
         ∑ e : CutEdge K Q,min (V A C a z (realCorner e.val.1))
           (V A C a z (realCorner e.val.2.1)) := by
   …

   Mentions: OAI.ContingencyTables.CompanionOracleDensity.height, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.CompanionOracleDensity.V