OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperFullVariance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The source Poincare bound for the full literal physical small graph

  1. theorem OAI.ContingencyTables.SmallGraphProfiles.firstPaper_full_variance line 23

    Source documentation

    The literal physical encoding consists of the balanced transversal words and the positive single-defect profiles. Zero-weight transversal words may be retained; they contribute zero to both variance and energy.

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