OAI/Combinatorics/ContingencyTables/Transport/NestedReindex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Physical coordinate reindexing of the first paper's nested penalties

  1. lemma OAI.ContingencyTables.NestedReindex.smallTotal_reindex line 18
  2. lemma OAI.ContingencyTables.NestedReindex.penalty_reindex line 23
  3. lemma OAI.ContingencyTables.NestedReindex.hardWeight_reindex line 30
  4. lemma OAI.ContingencyTables.NestedReindex.softWeight_reindex line 37
  5. lemma OAI.ContingencyTables.NestedReindex.removal_congr_box line 48

    Source documentation

    Box congruence with the ambient equality decision used by the actual physical view type.

    lemma removal_congr_box (f h : (S → ℕ) → ℝ) (m z : S → ℕ) (hz : InBox m z)
    (heq : ∀ x, InBox m x → f x=h x) :
    FactorialSignatures.integerRemovalMatrix f z=FactorialSignatures.integerRemovalMatrix h z := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.integerRemovalMatrix

  6. theorem OAI.ContingencyTables.NestedReindex.physical_soft_marginal_slices line 59
  7. theorem OAI.ContingencyTables.NestedReindex.physical_hard_marginal_removal line 77
  8. theorem OAI.ContingencyTables.NestedReindex.physical_hard_marginal_reflected line 91