DivisorMomentAbsorption.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.DivisorMomentAbsorption.large_exponent_majorant_littleO line 10

Source documentation

The large-fiber exponent is negligible compared with the quarter power.

theorem large_exponent_majorant_littleO (A B : ℝ) :
    (fun S : ℝ => A * (S ^ (1 / 16 : ℝ) * Real.log S) + B * Real.log S)
      =o[atTop] (fun S : ℝ => S ^ (1 / 4 : ℝ)) := by
…

theorem OAI.Problem337.DivisorMomentAbsorption.eventually_absorb_large_contribution line 26

Source documentation

A flexible final absorption step: the intermediate/small-fiber term may be any exponential with a nonpositive exponent.

theorem eventually_absorb_large_contribution (A B C : ℝ) (hA : 0 ≤ A) :
    ∀ᶠ S : ℝ in atTop, ∀ u : ℝ, u ≤ 0 →
      Real.exp (A * S ^ (1 / 16 : ℝ) * Real.log (Real.log S) + B * Real.log S) +
        2 * Real.exp u + C * Real.log S ≤ Real.exp (S ^ (1 / 4 : ℝ)) := by
…

theorem OAI.Problem337.DivisorMomentAbsorption.eventually_divisor_moment_absorption line 72

Source documentation

The precise final bound used after summing the moment bands.

theorem eventually_divisor_moment_absorption (A B C : ℝ) (hA : 0 ≤ A) :
    ∀ᶠ S : ℝ in atTop,
      Real.exp (A * S ^ (1 / 16 : ℝ) * Real.log (Real.log S) + B * Real.log S) +
        2 * Real.exp (-S / (200 * Real.log S)) + C * Real.log S ≤
          Real.exp (S ^ (1 / 4 : ℝ)) := by
…

def OAI.Problem337.DivisorMomentAbsorption.largeCoefficient line 86
Source documentation
Explicit coefficients for converting the uniform large-prime class estimate into the form required by eventually_divisor_moment_absorption.
```
def largeCoefficient (D r : ℝ) : ℝ :=
…
```
Mentions: OAI.Problem337.D
def OAI.Problem337.DivisorMomentAbsorption.harmonicCoefficient line 89
theorem OAI.Problem337.DivisorMomentAbsorption.large_contribution_exponent_bound line 92
theorem OAI.Problem337.DivisorMomentAbsorption.largeCoefficient_nonneg line 152
theorem OAI.Problem337.DivisorMomentAbsorption.harmonicCoefficient_nonneg line 158

theorem OAI.Problem337.DivisorMomentAbsorption.eventually_large_contribution_bound line 167

Source documentation

Uniform conversion of the entire large-class budget, including its factor of two and harmonic loss.

theorem eventually_large_contribution_bound (D r C : ℝ)
    (hD : 1 ≤ D) (hr : 0 ≤ r) (hC : 0 ≤ C) :
    ∀ᶠ S : ℝ in atTop, ∀ v Z : ℝ,
      S / (2 * Real.log S) ≤ v → v ≤ D * S → 2 ≤ Z → Real.log Z ≤ D * S →
      2 * Real.exp (r * (1 + Real.log ((D + 1) * S / v)) * v ^ (1 / 16 : ℝ) +
          C * Real.log (1 + Real.log Z)) ≤
        Real.exp (largeCoefficient D r * S ^ (1 / 16 : ℝ) * Real.log (Real.log S) +
          harmonicCoefficient D C * Real.log S) := by
…

Mentions: OAI.Problem337.D, OAI.Problem337.v, OAI.Problem337.DivisorMomentAbsorption.largeCoefficient, OAI.Problem337.DivisorMomentAbsorption.harmonicCoefficient