WeightedPowerExpansion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Taylor expansion inside the correction convolution

This is the finite-sum expansion before the truncated moments are replaced by their convergent infinite-series values.

def OAI.JointDickman.truncatedLogMoment line 17
theorem OAI.JointDickman.truncatedLogMoment_eq_range line 20
theorem OAI.JointDickman.correction_expansion_reindex line 29

theorem OAI.JointDickman.correction_power_expansion line 44

Source documentation

The actual correction sum has a Taylor expansion with a logarithmic moment controlling the entire remainder.

theorem correction_power_expansion (E : Finset ℕ) (z a : ℝ) (H : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (L : ℝ) (V : ℕ), 0 < L →
      (∀ v ∈ Ioc 0 V, Real.log v ≤ L / 2) →
      |(∑ v ∈ Ioc 0 V, smoothCorrection E z v / (v : ℝ) * (L - Real.log v) ^ a) -
        ∑ k ∈ range (H + 1), rpowShiftCoeff a k * truncatedLogMoment E z V k * L ^ (a - k)| ≤
          C * L ^ (a - (H + 1)) *
            ∑ v ∈ Ioc 0 V, |smoothCorrection E z v| / (v : ℝ) * (Real.log v) ^ (H + 1) := by
…

Mentions: OAI.JointDickman.smoothCorrection, OAI.JointDickman.rpowShiftCoeff, OAI.JointDickman.truncatedLogMoment

theorem OAI.JointDickman.correction_power_expansion_full line 68

Source documentation

Expansion using the full correction moments. Both errors are explicit: the Taylor remainder and the exponentially tilted tails of the moments.

theorem correction_power_expansion_full
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ A : ℝ, 0 < A ∧ ∀ (z a : ℝ) (H : ℕ), 0 ≤ z → z ≤ 1 / 2 →
      ∃ C : ℝ, 0 ≤ C ∧ ∀ (P V : ℕ) (L : ℝ),
        2 ≤ P → 1 ≤ Real.log P → 0 < V → 0 < L →
        (∀ v ∈ Ioc 0 V, Real.log v ≤ L / 2) →
        |(∑ v ∈ Ioc 0 V, smoothCorrection (Nat.primesLE P) z v / (v : ℝ) *
            (L - Real.log v) ^ a) -
          ∑ k ∈ range (H + 1), rpowShiftCoeff a k *
            correctionLogMoment (Nat.primesLE P) z k * L ^ (a - k)| ≤
          C * L ^ (a - (H + 1)) * (Real.log P) ^ (Real.exp 1 + (H + 1 : ℕ)) +
            A * (Real.log P) ^ (Real.exp 1) *
…

Mentions: OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.smoothCorrection, OAI.JointDickman.rpowShiftCoeff, OAI.JointDickman.correctionLogMoment