RegularPairChangeOfMeasure.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact first-representation mass with both regularity tests

theorem OAI.JointDickman.coefficient_tilt_mass line 13
Source documentation
The forced coefficient and tilted normalization together give exactly the half-prime subset law, scaled by B.
```
theorem coefficient_tilt_mass {B : ℕ} (hB : 1 < B) {A : Finset ℕ}
    (hA : A ⊆ auxiliaryPrimes B) :
    coefficientWeight B (∏ p ∈ A, p)*(remainderTiltNormalizer B A/(∏ p ∈ A, p : ℕ)) =
      (B : ℝ)*bernoulliSubsetMass (auxiliaryPrimes B) (fun p => (1/2 : ℝ)/p) A := by
…
```
Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.coefficientWeight, OAI.JointDickman.remainderTiltNormalizer, OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.regular_pair_change_of_measure line 33

Source documentation

Regularity is kept inside the changed probability measure. In particular, this identity makes no division by a regularity probability.

theorem regular_pair_change_of_measure {B L : ℕ} {τ C : ℝ} {A D : Finset ℕ}
    (hA : A ⊆ auxiliaryPrimes B) (hD : D ⊆ auxiliaryPrimes B)
    (F : Finset ℕ → Finset ℕ → ℝ) :
    (∑ S ∈ (auxiliaryPrimes B).powerset, ∑ R ∈ (auxiliaryPrimes B).powerset,
      if A ⊆ S ∧ D ⊆ R then
        bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) S*
        bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) R*
        regularResidueWeight B L τ C (S \ A)*regularResidueWeight B L τ C (R \ D)*F S R
      else 0) =
      (remainderTiltNormalizer B A/(∏ p ∈ A, p : ℕ))*
      (remainderTiltNormalizer B D/(∏ p ∈ D, p : ℕ))*
      regularTiltAverage B L τ C A (fun U => regularTiltAverage B L τ C D
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.regularResidueWeight, OAI.JointDickman.remainderTiltNormalizer, OAI.JointDickman.regularTiltAverage