OAI/Combinatorics/ContingencyTables/Transport/FinitePrefixVariance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Variance telescoping for literal finite coordinate prefixes

  1. def OAI.ContingencyTables.FiniteExposureVariance.restriction line 12
  2. def OAI.ContingencyTables.FiniteExposureVariance.prefixSnocEquiv line 15
  3. lemma OAI.ContingencyTables.FiniteExposureVariance.restriction_snoc line 18
  4. def OAI.ContingencyTables.FiniteExposureVariance.prefixVariance line 28
  5. def OAI.ContingencyTables.FiniteExposureVariance.prefixContribution line 31
  6. theorem OAI.ContingencyTables.FiniteExposureVariance.prefixVariance_step line 34
  7. lemma OAI.ContingencyTables.FiniteExposureVariance.prefixVariance_zero line 48
  8. lemma OAI.ContingencyTables.FiniteExposureVariance.prefixVariance_final line 56
  9. theorem OAI.ContingencyTables.FiniteExposureVariance.variance_le_prefix_budget line 62

    Source documentation

    Each physical exposure depth incurs its own budget once.

    theorem variance_le_prefix_budget (w H : (Fin q → A) → ℝ) (hw : ∀ a,0 ≤ w a)
    (B : ℝ) (hb : ∀ k : Fin q,prefixContribution w H k ≤ B) :
    variance w H ≤ q*B := by
…

    Mentions: OAI.ContingencyTables.FiniteExposureVariance.prefixContribution, OAI.ContingencyTables.FiniteExposureVariance.variance