Documentation

LeanPool.IwaniecLinearSieve.LinearSieve.Calculus

Calculus identities for the majorants of [I71, §4] #

mainMaj #

source
@[simp]
theorem IwaniecLinearSieve.mainMaj_true (s : ℝ) :
mainMaj true s = fSieve s
source
@[simp]
theorem IwaniecLinearSieve.mainMaj_false (s : ℝ) :
mainMaj false s = FSieve s + max (3 - s) 0
source
theorem IwaniecLinearSieve.continuous_mainMaj (lower : Bool) :
Continuous (mainMaj lower)
source
theorem IwaniecLinearSieve.mainMaj_nonneg (lower : Bool) (s : ℝ) :
0 ≤ mainMaj lower s
source
theorem IwaniecLinearSieve.mainMaj_antitone (lower : Bool) :
Antitone (mainMaj lower)
source
theorem IwaniecLinearSieve.mainMaj_le_MSieve (lower : Bool) (s : ℝ) :
mainMaj lower s ≤ MSieve s
source
theorem IwaniecLinearSieve.g_two_eq_integral {s : ℝ} (hs : 2 ≤ s) :
MeasureTheory.IntegrableOn (fun (t : ℝ) => max (3 - (t - 1)) 0 / (t - 1)) (Set.Ioi s) MeasureTheory.volume ∧ g 2 s = ∫ (t : ℝ) in Set.Ioi s, max (3 - (t - 1)) 0 / (t - 1)

g₂(s) = ∫_s^∞ (3 - (t-1))⁺/(t-1) dt for s ≥ 2.

source
theorem IwaniecLinearSieve.integrableOn_mainMaj_false_shift {s : ℝ} (hs : 2 ≤ s) :
MeasureTheory.IntegrableOn (fun (t : ℝ) => mainMaj false (t - 1) / (t - 1)) (Set.Ioi s) MeasureTheory.volume
source
theorem IwaniecLinearSieve.fSieve_eq_integral_mainMaj {s : ℝ} (hs : 2 ≤ s) :
fSieve s = ∫ (t : ℝ) in Set.Ioi s, mainMaj false (t - 1) / (t - 1)

f(s) = ∫_s^∞ M⁺(t-1)/(t-1) dt for s ≥ 2, with M⁺ = F + (3 - ·)⁺ ((3.6) together with g_two_eq_integral).

source
theorem IwaniecLinearSieve.mainMaj_false_eq_integral (s : ℝ) :
mainMaj false s = max (3 - s) 0 + ∫ (t : ℝ) in Set.Ioi (max s 3), fSieve (t - 1) / (t - 1)

M⁺(s) = (3 - s)⁺ + ∫_{max s 3}^∞ f(t-1)/(t-1) dt for every s ((3.7)).

source
theorem IwaniecLinearSieve.mainMaj_false_of_three_le {s : ℝ} (hs : 3 ≤ s) :
mainMaj false s = FSieve s

mainMaj in terms of fr: M true = f and, on s ≥ 3, M false = F.

errMaj #

source
@[simp]
theorem IwaniecLinearSieve.errMaj_true :
errMaj true = majf
source
@[simp]
theorem IwaniecLinearSieve.errMaj_false :
errMaj false = majF
source
def IwaniecLinearSieve.errLower :
Bool → ℝ

The left end of the domain of the identities (3.13), (3.14): 2 for 𝔣, 3 for 𝔉.

Equations
Instances For
    source
    @[simp]
    theorem IwaniecLinearSieve.errLower_true :
    errLower true = 2
    source
    @[simp]
    theorem IwaniecLinearSieve.errLower_false :
    errLower false = 3
    source
    theorem IwaniecLinearSieve.two_le_errLower (lower : Bool) :
    2 ≤ errLower lower
    source
    theorem IwaniecLinearSieve.errLower_le_three (lower : Bool) :
    errLower lower ≤ 3
    source
    theorem IwaniecLinearSieve.sMin_le_errLower (lower : Bool) :
    sMin lower ≤ errLower lower
    source
    theorem IwaniecLinearSieve.errMaj_eq_majG {lower : Bool} {r : ℕ} (h : Even r ↔ lower = true) :
    errMaj lower = majG r
    source
    theorem IwaniecLinearSieve.majG_add_two (r : ℕ) :
    majG (r + 2) = majG r
    source
    theorem IwaniecLinearSieve.continuous_errMaj (lower : Bool) :
    Continuous (errMaj lower)
    source
    theorem IwaniecLinearSieve.errMaj_pos (lower : Bool) (s : ℝ) :
    0 < errMaj lower s
    source
    theorem IwaniecLinearSieve.errMaj_antitone (lower : Bool) :
    Antitone (errMaj lower)
    source
    theorem IwaniecLinearSieve.errMaj_mem (lower : Bool) (s : ℝ) :
    bigM s / 3 ≤ errMaj lower s ∧ errMaj lower s ≤ 2 * bigM s / 3
    source
    theorem IwaniecLinearSieve.errMaj_le_two (lower : Bool) (s : ℝ) :
    errMaj lower s ≤ 2
    source
    theorem IwaniecLinearSieve.errMaj_false_of_le_three {s : ℝ} (hs : s ≤ 3) :
    errMaj false s = 1
    source
    theorem IwaniecLinearSieve.hasDerivAt_errMaj (lower : Bool) {t : ℝ} :
    errLower lower < t → HasDerivAt (errMaj lower) (-(errMaj (!lower) (t - 1) * t / (t - 1) ^ 2)) t

    The derivative of G lower is -G (!lower) (t-1) t/(t-1)² for t > 2 (𝔣) and t > 3 (𝔉).

    source
    theorem IwaniecLinearSieve.tendsto_errMaj_atTop (lower : Bool) :
    Filter.Tendsto (errMaj lower) Filter.atTop (nhds 0)
    source
    theorem IwaniecLinearSieve.errMaj_shift_pos (lower : Bool) {t : ℝ} (ht : 1 < t) :
    0 < errMaj lower (t - 1) * t / (t - 1) ^ 2
    source
    theorem IwaniecLinearSieve.errMaj_eq_integral (lower : Bool) {s : ℝ} (hs : errLower lower ≤ s) :
    MeasureTheory.IntegrableOn (fun (t : ℝ) => errMaj (!lower) (t - 1) * t / (t - 1) ^ 2) (Set.Ioi s) MeasureTheory.volume ∧ errMaj lower s = ∫ (t : ℝ) in Set.Ioi s, errMaj (!lower) (t - 1) * t / (t - 1) ^ 2

    (3.13), (3.14): for s ≥ 2 (lower = true) or s ≥ 3 (lower = false), G lower (s) = ∫_s^∞ G (!lower) (t-1) t/(t-1)² dt, the integrand being integrable.

    source
    theorem IwaniecLinearSieve.integral_errMaj_shift (lower : Bool) {s b : ℝ} (hs : errLower lower ≤ s) (hsb : s ≤ b) :
    ∫ (t : ℝ) in s..b, errMaj (!lower) (t - 1) * t / (t - 1) ^ 2 = errMaj lower s - errMaj lower b

    The finite-interval form: ∫_s^b G (!lower) (t-1) t/(t-1)² dt = G lower (s) - G lower (b).