EndpointSplitAverage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Averaging a candidate's coefficient and remaining endpoint weight

theorem OAI.JointDickman.endpoint_split_weight_bound line 13

theorem OAI.JointDickman.independent_endpoint_split_average line 42

Source documentation

The independently averaged endpoint split has the exact half-prime marginal, without dividing by the probability of passing regularity.

theorem independent_endpoint_split_average {B L : ℕ} {τ C : ℝ} (hB : 1 < B)
    (F : Finset ℕ → ℝ) (hF : ∀ A ⊆ auxiliaryPrimes B, 0 ≤ F A) :
    (∑ S ∈ (auxiliaryPrimes B).powerset,
      bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) S*
      ∑ A ∈ endpointSplits B L τ C S,
        regularCoefficientWeight B L τ C (∏ p ∈ A, p)*
          regularResidueWeight B L τ C (S \ A)*F A) ≤
      (B : ℝ)*∑ A ∈ (auxiliaryPrimes B).powerset,
        bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1/2 : ℝ)/p) A*F A := by
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.endpointSplits, OAI.JointDickman.regularCoefficientWeight, OAI.JointDickman.regularResidueWeight