OAI/NumberTheory/JointDickman/Amplification/AmplificationEnvelope.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The independent-model amplification envelope and its second moment

  1. def OAI.JointDickman.independentAmplificationEnvelope line 13
  2. theorem OAI.JointDickman.independentAmplificationEnvelope_second_identity line 19
  3. theorem OAI.JointDickman.independentAmplificationEnvelope_second_bound line 47

    Source documentation

    The B-normalized fair-split envelope has a bounded second moment.

    theorem independentAmplificationEnvelope_second_bound
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∀ (L : ℕ) (τ C : ℝ), ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop,
      ∀ T : ℕ, 0 < T → (T : ℝ) ≤ Real.exp ((1 / 10 : ℝ) * B) →
      (∑ S ∈ (auxiliaryPrimes B).powerset,
        bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1 / (p : ℝ)) S *
      ∑ R ∈ (auxiliaryPrimes B).powerset,
        bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1 / (p : ℝ)) R *
        (independentAmplificationEnvelope B L T τ C S R)^2) ≤ K := by
…

    Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.independentAmplificationEnvelope