ConditionalFairSplit.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact conditional law of the remaining half of a prime site

theorem OAI.JointDickman.subsetMass_prod_ite line 11
theorem OAI.JointDickman.subsetMass_tilt_product line 23
def OAI.JointDickman.fairSelectedRemainingMass line 40
Source documentation
A site is sampled at density 1/p and split by fair coins; A and R are its selected and remaining prime sets.
```
noncomputable def fairSelectedRemainingMass (P A R : Finset ℕ) : ℝ :=
…
```
theorem OAI.JointDickman.fairSelectedRemainingMass_factor line 47
Source documentation
The exact joint mass factors into the selected marginal and the independent remaining indicators, including the zero probabilities at A.
```
theorem fairSelectedRemainingMass_factor {P A R : Finset ℕ}
    (hP : ∀ p ∈ P, p.Prime) (hA : A ⊆ P) (hR : R ⊆ P) :
    fairSelectedRemainingMass P A R =
      bernoulliSubsetMass P (fun p => (1 / 2 : ℝ) / p) A *
      bernoulliSubsetMass P (remainingPrimeParameter A) R := by
…
```
Mentions: OAI.JointDickman.fairSelectedRemainingMass, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.remainingPrimeParameter
theorem OAI.JointDickman.fairSelectedRemainingMass_bad line 87
Source documentation
Summing the exact joint split mass over nonregular remainders gives the selected marginal times the failure probability proved above.
```
theorem fairSelectedRemainingMass_bad (B L : ℕ) (τ C : ℝ) {A : Finset ℕ}
    (hA : A ⊆ auxiliaryPrimes B) :
    (∑ R ∈ (auxiliaryPrimes B).powerset,
      if RegularPrimeSet B L τ C R then 0 else fairSelectedRemainingMass (auxiliaryPrimes B) A R) =
      bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1 / 2 : ℝ) / p) A *
        primeRegularityFailureProbability B L τ C (remainingPrimeParameter A) := by
…
```
Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.fairSelectedRemainingMass, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.primeRegularityFailureProbability, OAI.JointDickman.remainingPrimeParameter