RequiredSubsetTail.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Prescribed inclusions with a remaining prefix-count restriction

theorem OAI.JointDickman.bernoulliSubsetMass_required_test line 13

Source documentation

Conditioning on prescribed independent inclusions leaves the other parameters unchanged. The test remains inside the finite expectation.

theorem bernoulliSubsetMass_required_test (P A : Finset ℕ) (q : ℕ → ℝ)
    (hA : A ⊆ P) (F : Finset ℕ → ℝ) :
    (∑ S ∈ P.powerset, if A ⊆ S then bernoulliSubsetMass P q S*F S else 0) =
      (∏ p ∈ A, q p)*∑ R ∈ (P \ A).powerset,
        bernoulliSubsetMass (P \ A) q R*F (A ∪ R) := by
…

Mentions: OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.bernoulliSubsetMass_required_prefix_tail line 54

Source documentation

Lower-tail Chernoff bound with the prescribed inclusions retained. This is the finite estimate used for numeric additions in moments.tex.

theorem bernoulliSubsetMass_required_prefix_tail (P A Q : Finset ℕ) (q : ℕ → ℝ)
    (hA : A ⊆ P) (hAQ : A ⊆ Q) (hq : ∀ p ∈ P, 0 ≤ q p ∧ q p ≤ 1)
    {t : ℝ} (ht : 0 ≤ t) (r : ℝ) :
    (∑ S ∈ P.powerset, if A ⊆ S ∧ ((S ∩ Q).card : ℝ) ≤ r then
      bernoulliSubsetMass P q S else 0) ≤
      (∏ p ∈ A, q p)*Real.exp (t*(r-A.card)+
        (Real.exp (-t)-1)*∑ p ∈ (P \ A) ∩ Q, q p) := by
…

Mentions: OAI.JointDickman.bernoulliSubsetMass