AmplificationEnvelopeFirst.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The positive first moment of the independent amplification envelope

theorem OAI.JointDickman.independentAmplificationEnvelope_first_identity line 13

theorem OAI.JointDickman.independentAmplificationEnvelope_first_lower line 62

Source documentation

A positive first moment, uniformly after choosing the regularity cutoff.

theorem independentAmplificationEnvelope_first_lower
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput) :
    ∃ d : ℝ, 0 < d ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
      ∃ C₀ : ℝ, 0 ≤ C₀ ∧ ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (T : ℕ), C₀ ≤ C →
        0 < T → (T : ℝ) ≤ Real.exp ((1 / 10 : ℝ) * B) →
        d ≤ ∑ S ∈ (auxiliaryPrimes B).powerset,
          bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1 / (p : ℝ)) S *
          ∑ R ∈ (auxiliaryPrimes B).powerset,
            bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1 / (p : ℝ)) R *
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass