RemainderPushforward.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exact selected-and-remaining law behind the candidate error

theorem OAI.JointDickman.selectedRemainingMass_site line 12
theorem OAI.JointDickman.selectedRemainingMass_sum line 25
Source documentation
Replacing a site by its selected set and its complement is an exact change of variables. The test can be a regularity failure indicator.
```
theorem selectedRemainingMass_sum {P A : Finset ℕ} (hA : A ⊆ P)
    (F : Finset ℕ → ℝ) :
    (∑ S ∈ P.powerset, bernoulliSubsetMass P (fun p => 1/(p : ℝ)) S*
      subsetRetentionMass S A*F (S \ A)) =
      ∑ R ∈ P.powerset, fairSelectedRemainingMass P A R*F R := by
…
```
Mentions: OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.subsetRetentionMass, OAI.JointDickman.fairSelectedRemainingMass
theorem OAI.JointDickman.selectedRemainingMass_pair_sum line 78

theorem OAI.JointDickman.remainingPairFailure_site_sum line 110

Source documentation

The bad-remainder event in the site-first expression is exactly the failure mass whose conditional probability is controlled by Mertens.

theorem remainingPairFailure_site_sum (B L : ℕ) (τ C : ℝ) {A D : Finset ℕ}
    (hA : A ⊆ auxiliaryPrimes B) (hD : D ⊆ auxiliaryPrimes B) :
    (∑ S ∈ (auxiliaryPrimes B).powerset, ∑ R ∈ (auxiliaryPrimes B).powerset,
      bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) S*
      bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) R*
      subsetRetentionMass S A*subsetRetentionMass R D*
        (if RegularPrimeSet B L τ C (S \ A) ∧ RegularPrimeSet B L τ C (R \ D)
          then 0 else 1)) = fairRemainingPairFailure B L τ C A D := by
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.subsetRetentionMass, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.fairRemainingPairFailure