OAI/NumberTheory/JointDickman/Probability/SplitProbabilityBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite event bounds for the actual two-site split law

  1. theorem OAI.JointDickman.twoSiteSplitProbability_nonneg line 11
  2. theorem OAI.JointDickman.twoSiteSplitProbability_congr line 20
  3. theorem OAI.JointDickman.twoSiteSplitProbability_mono line 28
  4. theorem OAI.JointDickman.twoSiteSplitProbability_or line 40
  5. theorem OAI.JointDickman.twoSiteSplitProbability_cover line 54

    Source documentation

    A finite event cover costs the sum of the actual event probabilities.

    theorem twoSiteSplitProbability_cover {ι : Type*} [DecidableEq ι]
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (I : Finset ι)
    (E N : TwoSiteSplit P → Prop) (F : ι → TwoSiteSplit P → Prop)
    (hcover : ∀ x, E x → N x ∨ ∃ i ∈ I, F i x) :
    twoSiteSplitProbability P E ≤ twoSiteSplitProbability P N +
      ∑ i ∈ I, twoSiteSplitProbability P (F i) := by
…

    Mentions: OAI.JointDickman.TwoSiteSplit, OAI.JointDickman.twoSiteSplitProbability

  6. theorem OAI.JointDickman.twoSiteSplitProbability_four_or line 86