OAI/Combinatorics/ContingencyTables/Dense/DenseInteriorVolume.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive volume of the actual dense completion polytope

  1. def OAI.ContingencyTables.DenseAffine.normalizedEntry line 15
  2. theorem OAI.ContingencyTables.DenseAffine.normalizedEntry_change line 20
  3. theorem OAI.ContingencyTables.DenseAffine.dense_change_below_interior_slack line 42
  4. theorem OAI.ContingencyTables.DenseAffine.dense_feasible_volume_pos line 57

    Source documentation

    A full open unit box around the constructed interior point is feasible. Consequently the feasible polytope has positive Lebesgue volume, including the zero-dimensional convention.

    theorem dense_feasible_volume_pos (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)
    (hdimR : Fintype.card (Option I) ≤ d) (hdimP : Fintype.card (Option J) ≤ d)
    (hfree : Fintype.card (I × J) ≤ d) (htotal : ∑ i, R i = ∑ j, P j) :
    0 < volume {u : I × J → ℝ | Feasible R P d u} := by
…

    Mentions: OAI.ContingencyTables.DenseAffine.Feasible