DenseGeometry.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Feasible region and interior point of the dense block

These statements use the actual integer margins and quotient widths. Every feasible real completion lies in the declared scaled cube, and one scaled completion has normalized slack at least 1/(2d) in every cell.

def OAI.ContingencyTables.DenseAffine.Feasible line 20
theorem OAI.ContingencyTables.DenseAffine.denseWidth_pos line 25
theorem OAI.ContingencyTables.DenseAffine.table_entry_upper line 33
theorem OAI.ContingencyTables.DenseAffine.feasible_in_cube line 44

theorem OAI.ContingencyTables.DenseAffine.dense_interior_exists line 67

Source documentation

Real residual completion constructs the strict interior point.

theorem dense_interior_exists (R : Option I → ℕ) (P : Option J → ℕ) (d : ℕ)
    (hd : 14 ≤ d) (hR : ∀ i, d ^ 12 ≤ R i) (hP : ∀ j, d ^ 12 ≤ P j)
    (hdimR : Fintype.card (Option I) ≤ d) (hdimP : Fintype.card (Option J) ≤ d)
    (htotal : ∑ i, R i = ∑ j, P j) :
    ∃ u : I × J → ℝ, Feasible R P d u ∧
      (∀ p, 0 ≤ u p ∧ u p ≤ 2 * (d : ℝ) ^ 8) ∧
      ∀ g : Option I × Option J,
        1 / (2 * (d : ℝ)) ≤
          table (fun i => (R i : ℝ)) (fun j => (P j : ℝ)) (denseWidth R P d) u g.1 g.2 /
            cellScale (fun i => (R i : ℝ)) (fun j => (P j : ℝ)) g := by
…

Mentions: OAI.ContingencyTables.DenseAffine.Feasible, OAI.ContingencyTables.DenseAffine.table, OAI.ContingencyTables.DenseAffine.denseWidth, OAI.ContingencyTables.DenseAffine.cellScale

theorem OAI.ContingencyTables.DenseAffine.densePenalty_eq_zero_of_feasible line 101