SmoothGiantSupport.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite support for the actual positive-integer giant extension

def OAI.Ostmann.smoothGiantIntegerRange line 11
def OAI.Ostmann.smoothGiantPrimeRange line 14
theorem OAI.Ostmann.smoothGiantPrimeRange_prime line 17
theorem OAI.Ostmann.smoothGiantPrimeRange_subset line 20
theorem OAI.Ostmann.smoothGiantIntegerRange_pos line 23
theorem OAI.Ostmann.smoothGiant_weight_zero_outside line 30
Source documentation
No positive integer outside this range contributes to the extension. The endpoints are retained in the finite set.
```
theorem smoothGiant_weight_zero_outside (φ : ℝ → ℝ) (G : ℝ)
    (hout : ∀ x, 1 ≤ |x| → φ x = 0) (p : ℕ) (hp : 0 < p)
    (hpI : p ∉ smoothGiantIntegerRange G) : φ (Real.log p - G) = 0 := by
…
```
Mentions: OAI.Ostmann.smoothGiantIntegerRange

theorem OAI.Ostmann.smoothGiant_prime_support line 44

Source documentation

The smooth normalizer has the exact finite support stipulated in (7.3).

theorem smoothGiant_prime_support (φ : ℝ → ℝ) (G : ℝ)
    (hout : ∀ x, 1 ≤ |x| → φ x = 0) (p : ℕ) (hp : p.Prime)
    (hφp : φ (Real.log p - G) ≠ 0) : p ∈ smoothGiantPrimeRange G := by
…

Mentions: OAI.Ostmann.smoothGiantPrimeRange

theorem OAI.Ostmann.smoothGiantMass_lower line 54

Source documentation

A lower bound on the bump in a retained central prime interval gives an actual lower bound for its normalizer.

theorem smoothGiantMass_lower (P S : Finset ℕ) (hSP : S ⊆ P)
    (φ : ℝ → ℝ) (G a : ℝ) (hφ : ∀ x, 0 ≤ φ x)
    (ha : ∀ p ∈ S, a ≤ φ (Real.log p - G)) :
    a * (∑ p ∈ S, (p : ℝ)⁻¹) ≤ smoothGiantMass P φ G := by
…

Mentions: OAI.Ostmann.smoothGiantMass