EndpointCoefficientTest.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Pushing the second endpoint's fair split onto its coefficient

def OAI.JointDickman.endpointCoefficientTest line 12
theorem OAI.JointDickman.endpointCoefficientTest_nonneg line 16
theorem OAI.JointDickman.endpointCoefficientTest_ge line 24
theorem OAI.JointDickman.endpointCoefficientTest_mean line 36
Source documentation
This identity uses the exact prime-product pushforward, so no local limit or independence beyond the already constructed endpoint law is assumed.
```
theorem endpointCoefficientTest_mean (B b j q : ℕ) :
    (∑ A ∈ (auxiliaryPrimes B).powerset,
      bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1/2 : ℝ)/p) A*
        endpointCoefficientTest B b j q (∏ p ∈ A, p)) =
      endpointCoefficientMass B b j q := by
…
```
Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.endpointCoefficientTest, OAI.JointDickman.endpointCoefficientMass

theorem OAI.JointDickman.independent_endpoint_coefficient_average line 67

Source documentation

The weighted, independently averaged second endpoint costs B times its half-prime coefficient mass.

theorem independent_endpoint_coefficient_average {B L : ℕ} {τ C : ℝ}
    (hB : 1 < B) (b j q : ℕ) :
    (∑ 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)*
            endpointCoefficientTest B b j q (∏ p ∈ A, p)) ≤
      (B : ℝ)*endpointCoefficientMass B b j q := by
…

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