OAI/Combinatorics/ContingencyTables/Transport/IntegerMarginal.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Balanced marginalization of actual integer two-removal matrices

The new pair is summed subject to its exact total M. We identify every old, fresh and cross entry with the balanced summation theorem; thus the signature of the marginal is derived from signatures of the actual unsummed integer matrices, rather than assumed for a binary encoding.

  1. def OAI.ContingencyTables.IntegerMarginal.profile line 23
  2. def OAI.ContingencyTables.IntegerMarginal.marginal line 26
  3. lemma OAI.ContingencyTables.IntegerMarginal.profile_removeOld line 30
  4. lemma OAI.ContingencyTables.IntegerMarginal.profile_removeAA line 36
  5. lemma OAI.ContingencyTables.IntegerMarginal.profile_removeBB line 43
  6. lemma OAI.ContingencyTables.IntegerMarginal.profile_removeAB line 50
  7. lemma OAI.ContingencyTables.IntegerMarginal.profile_removeOldA line 56
  8. lemma OAI.ContingencyTables.IntegerMarginal.profile_removeOldB line 62
  9. def OAI.ContingencyTables.IntegerMarginal.old line 67
  10. def OAI.ContingencyTables.IntegerMarginal.pairMatrix line 72
  11. def OAI.ContingencyTables.IntegerMarginal.innerWeight line 76
  12. def OAI.ContingencyTables.IntegerMarginal.cross line 80
  13. lemma OAI.ContingencyTables.IntegerMarginal.integerRemoval_symm line 87
  14. lemma OAI.ContingencyTables.IntegerMarginal.pairMatrix_aa line 92
  15. lemma OAI.ContingencyTables.IntegerMarginal.pairMatrix_bb line 107
  16. lemma OAI.ContingencyTables.IntegerMarginal.pairMatrix_ab line 122
  17. lemma OAI.ContingencyTables.IntegerMarginal.old_single line 134
  18. lemma OAI.ContingencyTables.IntegerMarginal.old_old line 138
  19. lemma OAI.ContingencyTables.IntegerMarginal.cross_a line 142
  20. lemma OAI.ContingencyTables.IntegerMarginal.cross_b line 156
  21. lemma OAI.ContingencyTables.IntegerMarginal.pairMatrix_old line 182
  22. lemma OAI.ContingencyTables.IntegerMarginal.marginal_old_matrix line 192
  23. lemma OAI.ContingencyTables.IntegerMarginal.marginal_old_block line 199
  24. theorem OAI.ContingencyTables.IntegerMarginal.marginal_removal_onePositive line 213

    Source documentation

    Exact balanced marginal closure for the paper's raw integer matrices.

    theorem marginal_removal_onePositive
    (F : ((I ⊕ Bool) → ℕ) → ℝ) (M : ℕ) (z : I → ℕ) (hM : 2 ≤ M)
    (hsig : ∀ j ≤ M, OnePositiveDirection (integerRemovalMatrix F (profile z j (M-j))).toBilin')
    (hpos : ∀ j, 0 < j → j < M → 0 < F (profile z (j-1) (M-1-j))) :
    OnePositiveDirection (integerRemovalMatrix (marginal F M) z).toBilin' := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.IntegerMarginal.profile, OAI.ContingencyTables.IntegerMarginal.marginal

  25. theorem OAI.ContingencyTables.IntegerMarginal.removal_signature_limit line 239

    Source documentation

    Equality-softening limits preserve the actual raw integer signature. Only the finitely many displayed matrix entries are used.

    theorem removal_signature_limit {K : Type*} {l : Filter K} [l.NeBot]
    (F : K → (I → ℕ) → ℝ) (f : (I → ℕ) → ℝ) (z : I → ℕ)
    (hlim : ∀ n, Filter.Tendsto (fun t => F t n) l (nhds (f n)))
    (hsig : ∀ᶠ t in l, OnePositiveDirection (integerRemovalMatrix (F t) z).toBilin') :
    OnePositiveDirection (integerRemovalMatrix f z).toBilin' := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection