OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperTransversalVariance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Global transversal variance for the literal first-paper profiles

  1. theorem OAI.ContingencyTables.RowMajorEnumeration.firstPaper_word_context_variance line 21
  2. lemma OAI.ContingencyTables.RowMajorEnumeration.firstPaper_prefixContribution_le line 54
  3. theorem OAI.ContingencyTables.RowMajorEnumeration.firstPaper_transversal_variance line 90

    Source documentation

    Actual first-paper balanced choices, weighted by every physical large completion, satisfy the paper's global transversal variance bound.

    theorem firstPaper_transversal_variance (r : I → ℕ) (c : J → ℕ)
    (H : SmallProfile (paperSmall r c) → ℝ) :
    let d := dimensionAllowance (I := I) (J := J)
…