OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperContextChildren.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Child-mass minimum for the actual first-paper context

Ordinary unexposed pairs are summed with their actual balances before applying the proved two-coordinate removal inequality and its hard limit.

  1. theorem OAI.ContingencyTables.FirstPaperContextTransport.context_child_minimum line 21