OAI/NumberTheory/JointDickman/Amplification/WeightedRemainderLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact measure obtained by weighting the first representation

After requiring a coefficient and weighting the remaining primes by one half, the unforced indicators have probability 1/(2p-1). Regularity tests remain inside the expectation and do not alter its normalization.

  1. theorem OAI.JointDickman.required_prime_mass_factor line 18
  2. theorem OAI.JointDickman.half_weight_tilt line 37
  3. def OAI.JointDickman.remainderTiltNormalizer line 66
  4. theorem OAI.JointDickman.weighted_required_prime_mass line 69
  5. theorem OAI.JointDickman.weighted_remainder_change_of_measure line 88

    Source documentation

    An arbitrary regularity or multiplicity test stays inside the new law.

    theorem weighted_remainder_change_of_measure {B : ℕ} {A : Finset ℕ}
    (hA : A ⊆ auxiliaryPrimes B) (F : Finset ℕ → ℝ) :
    (∑ S ∈ (auxiliaryPrimes B).powerset, if A ⊆ S then
      bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) S*
        residueBaseWeight B (S \ A)*F (S \ A) else 0) =
      remainderTiltNormalizer B A/(∏ p ∈ A, p : ℕ)*
        ∑ R ∈ (auxiliaryPrimes B \ A).powerset,
          bernoulliSubsetMass (auxiliaryPrimes B \ A)
            (fun p => 1/(2*(p : ℝ)-1)) R*F R := by
…

    Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.residueBaseWeight, OAI.JointDickman.remainderTiltNormalizer