SmoothGiantIntervalBridge.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The normalized giant prior and its complete logarithmic cell

theorem OAI.Ostmann.smoothGiant_nonzero_in_log_cell line 11

theorem OAI.Ostmann.smoothGiant_unnormalized_interval line 29

Source documentation

The finite support may include extra endpoints, but those have zero smooth weight; every contributing prime lies in the complete cell.

theorem smoothGiant_unnormalized_interval (φ : ℝ → ℝ) (G : ℝ)
    (hout : ∀ x, 1 ≤ |x| → φ x = 0) (F : ℕ → ℂ) :
    (∑ p ∈ smoothGiantPrimeRange G,
      (φ (Real.log p - G) : ℂ) * F p * ((p : ℝ)⁻¹ : ℂ)) =
    complexPrimeInterval 1 0 (G - 1) (G + 1)
      (fun x => (φ (x - G) : ℂ) * F ⌊Real.exp x⌋₊) := by
…

Mentions: OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.complexPrimeInterval

theorem OAI.Ostmann.smoothGiantPrior_interval line 64

Source documentation

The normalizer is retained explicitly when the original giant law is written as a prime logarithmic integral.

theorem smoothGiantPrior_interval (φ : ℝ → ℝ) (G : ℝ)
    (hout : ∀ x, 1 ≤ |x| → φ x = 0) (F : ℕ → ℂ) :
    (∑ p : smoothGiantPrimeRange G,
      (smoothGiantPrior (smoothGiantPrimeRange G) φ G p : ℂ) * F p) =
    (Real.exp (smoothGiantLogNormalizer (smoothGiantPrimeRange G) φ G) : ℂ) *
      complexPrimeInterval 1 0 (G - 1) (G + 1)
        (fun x => (φ (x - G) : ℂ) * F ⌊Real.exp x⌋₊) := by
…

Mentions: OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.smoothGiantPrior, OAI.Ostmann.smoothGiantLogNormalizer, OAI.Ostmann.complexPrimeInterval