RealCompletion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Real completions with prescribed lower bounds

The dense geometric argument needs one strictly feasible normalized table. Residual nonnegative real margins are completed by a rank-one table; this is enough for the analytic interior-point argument and makes no algorithmic claim about integral flow preprocessing.

theorem OAI.ContingencyTables.real_table_exists line 22
theorem OAI.ContingencyTables.lower_bounded_real_table line 48

theorem OAI.ContingencyTables.strict_real_completion line 74

Source documentation

Assigning min(rᵢ,cⱼ)/(2d) to every cell leaves nonnegative residual margins whenever each dimension is at most d.

theorem strict_real_completion (r : I → ℝ) (c : J → ℝ) (d : ℝ)
    (hd : 0 < d) (hr : ∀ i, 0 ≤ r i) (hc : ∀ j, 0 ≤ c j)
    (hrows : (Fintype.card I : ℝ) ≤ d) (hcols : (Fintype.card J : ℝ) ≤ d)
    (htotal : ∑ i, r i = ∑ j, c j) :
    ∃ X : I → J → ℝ, (∀ i j, min (r i) (c j) / (2 * d) ≤ X i j) ∧
      (∀ i, ∑ j, X i j = r i) ∧ (∀ j, ∑ i, X i j = c j) := by
…