OAI/Combinatorics/ContingencyTables/Transport/TableTightening.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous tightening and translation by attained cell minima

The hypotheses here are exactly the extremum properties proved for the executed searches. The maps preserve all tables, with explicit inverse addition and with both endpoints of every translated interval attained.

  1. def OAI.ContingencyTables.TableTightening.subtract line 18
  2. def OAI.ContingencyTables.TableTightening.add line 19
  3. def OAI.ContingencyTables.TableTightening.rows line 21
  4. def OAI.ContingencyTables.TableTightening.columns line 22
  5. def OAI.ContingencyTables.TableTightening.bounds line 24
  6. lemma OAI.ContingencyTables.TableTightening.add_subtract line 26
  7. lemma OAI.ContingencyTables.TableTightening.subtract_add line 31
  8. lemma OAI.ContingencyTables.TableTightening.subtract_margins line 35
  9. lemma OAI.ContingencyTables.TableTightening.lower_sums line 56
  10. lemma OAI.ContingencyTables.TableTightening.add_margins line 67
  11. def OAI.ContingencyTables.TableTightening.Feasible line 78
  12. def OAI.ContingencyTables.TableTightening.TightFeasible line 80
  13. theorem OAI.ContingencyTables.TableTightening.subtract_feasible line 84

    Source documentation

    A feasible table lies in every attained coordinate interval.

    theorem subtract_feasible (hl : ∀ X,Feasible r c b X→∀ i j,l i j≤X i j)
    (hu : ∀ X,Feasible r c b X→∀ i j,X i j≤u i j)
    {X : Fin m→Fin n→ℕ} (hX : Feasible r c b X) :
    TightFeasible r c l u (subtract X l) := by
…

    Mentions: OAI.ContingencyTables.TableTightening.Feasible, OAI.ContingencyTables.TableTightening.TightFeasible, OAI.ContingencyTables.TableTightening.subtract

  14. theorem OAI.ContingencyTables.TableTightening.add_feasible line 92
  15. theorem OAI.ContingencyTables.TableTightening.endpoints line 110

    Source documentation

    Both translated endpoints are actual table entries, including when an interval has width zero.

    theorem endpoints (hl : ∀ X,Feasible r c b X→∀ i j,l i j≤X i j)
    (hu : ∀ X,Feasible r c b X→∀ i j,X i j≤u i j)
    (hlo : ∀ i j,∃ X,Feasible r c b X ∧ X i j=l i j)
    (hup : ∀ i j,∃ X,Feasible r c b X ∧ X i j=u i j) :
    (∀ i j,∃ Y,TightFeasible r c l u Y ∧ Y i j=0) ∧
      (∀ i j,∃ Y,TightFeasible r c l u Y ∧ Y i j=bounds l u i j) := by
…

    Mentions: OAI.ContingencyTables.TableTightening.Feasible, OAI.ContingencyTables.TableTightening.TightFeasible, OAI.ContingencyTables.TableTightening.bounds