OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperExposureVariance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual first-paper per-context exposure variance bound

  1. lemma OAI.ContingencyTables.ExcessContextProfiles.later_card_le_allowance line 20
  2. lemma OAI.ContingencyTables.ExcessContextProfiles.exposure_coefficient line 28
  3. theorem OAI.ContingencyTables.ExcessContextProfiles.firstPaper_exposure_variance line 46

    Source documentation

    The literal source parameters discharge the box, capacity and signature-side conditions. The only remaining conditions describe the chosen bounded prefix and a positive-mass exposure context.

    theorem firstPaper_exposure_variance (r : I → ℕ) (c : J → ℕ)
    (s : I×J) (hs : paperSmall r c s.1 s.2=true) (σ : I×J → ℕ)
    (hσ : ∀ a : Earlier (paperSmall r c) s,
      σ a.val.val ≤ (dimensionAllowance (I := I) (J := J))^20)
…