IntermediatePrefixClass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.DivisorMoment.IntermediatePrefixWitness line 14
Source documentation
Prime-factor prefix data defining one intermediate dyadic band. This does not assume either a divisor-count estimate or a lower bound on the prefix.
```
def IntermediatePrefixWitness (n d p : ℕ) (Y v t : ℝ) : Prop :=
…
```
Mentions: OAI.Problem337.v

theorem OAI.Problem337.DivisorMoment.intermediate_selected_prefix_moment_bound line 24

Source documentation

The actual intermediate prefix class: the lower-prefix and pointwise moment hypotheses of the Rankin class bound are derived from factorization data and the crossing of the square-root cutoff.

theorem intermediate_selected_prefix_moment_bound (r : ℝ) (hr : 0 ≤ r) :
    ∃ C : ℝ, 0 < C ∧ ∀ (N : ℕ) (X Y v t W : ℝ) (H : Finset ℕ),
      1 < X → Real.log X = v → 1 ≤ Y → v / 2 ≤ Real.log Y →
      1 ≤ t → t ≤ v → Real.log (v / t) / (10 * t) ≤ 1 / 4 →
      v ^ (15 / 16 : ℝ) ≤ v / 20 → v ≤ W →
      H ⊆ Finset.Icc 1 ⌊Y⌋₊ →
      (∀ h ∈ H, Real.log ((N + h : ℕ) : ℝ) ≤ W) →
      (∀ h ∈ H, ∃ d p : ℕ, IntermediatePrefixWitness (N + h) d p Y v t) →
      (∑ h ∈ H, (truncatedDivisorCount X (N + h) : ℝ) ^ r) ≤ 2 * Y *
        Real.exp (r * ((1 + Real.log (W / v)) * v / t) -
          (v / t) * Real.log (v / t) / 50 +
          C * (v / t) ^ (1 / 5 : ℝ) * Real.log (2 * t)) := by
…

Mentions: OAI.Problem337.v, OAI.Problem337.DivisorMoment.IntermediatePrefixWitness, OAI.Problem337.truncatedDivisorCount

theorem OAI.Problem337.DivisorMoment.eventually_intermediate_selected_prefix_moment_bound line 73

Source documentation

Uniform scale version with both the Rankin admissibility and the lower prefix size discharged. This is ready for a finite dyadic union.

theorem eventually_intermediate_selected_prefix_moment_bound (r : ℝ) (hr : 0 ≤ r) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ S : ℝ in atTop,
      ∀ (N : ℕ) (X Y v t W : ℝ) (H : Finset ℕ),
      1 < X → Real.log X = v → 1 ≤ Y → v / 2 ≤ Real.log Y →
      S / (2 * Real.log S) ≤ v → v ≤ S ^ 2 →
      1 ≤ t → t ≤ v → 4 * Real.log S ≤ t → v ≤ W →
      H ⊆ Finset.Icc 1 ⌊Y⌋₊ →
      (∀ h ∈ H, Real.log ((N + h : ℕ) : ℝ) ≤ W) →
      (∀ h ∈ H, ∃ d p : ℕ, IntermediatePrefixWitness (N + h) d p Y v t) →
      (∑ h ∈ H, (truncatedDivisorCount X (N + h) : ℝ) ^ r) ≤ 2 * Y *
        Real.exp (r * ((1 + Real.log (W / v)) * v / t) -
          (v / t) * Real.log (v / t) / 50 +
…

Mentions: OAI.Problem337.v, OAI.Problem337.DivisorMoment.IntermediatePrefixWitness, OAI.Problem337.truncatedDivisorCount