noncomputable def AnalyticNumberTheory.LargeSieve.dampedPerronMajorantIntegrand (ε L t : ℝ) : ℝ

A totalized version of the damped Perron majorant. The explicit zero branch keeps the paper expression honest even though division by zero is totalized in Lean.

Equations

• AnalyticNumberTheory.LargeSieve.dampedPerronMajorantIntegrand ε L t = if t = 0 then 0 else Real.exp (-ε * t) * min 1 (L * t) / t

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorantIntegrand_measurable (ε L : ℝ) : Measurable (dampedPerronMajorantIntegrand ε L)

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorantIntegrand_nonneg {ε L t : ℝ} (hL : 0 ≤ L) (ht : 0 ≤ t) : 0 ≤ dampedPerronMajorantIntegrand ε L t

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorantIntegrand_le_head {ε L t : ℝ} (hL : 0 ≤ L) (hε : 0 ≤ ε) (ht : t ∈ Set.Ioc 0 1) : dampedPerronMajorantIntegrand ε L t ≤ L

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorantIntegrand_le_inv {ε L t : ℝ} (hε : 0 ≤ ε) (hL : 0 ≤ L) (ht : 1 ≤ t) : dampedPerronMajorantIntegrand ε L t ≤ t⁻¹

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorantIntegrand_le_tail {ε L t : ℝ} (hε : 0 < ε) (_hL : 0 ≤ L) (ht : ε⁻¹ ≤ t) : dampedPerronMajorantIntegrand ε L t ≤ ε * Real.exp (-ε * t)

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorant_integrableOn_head {ε L : ℝ} (hL : 0 ≤ L) (hε : 0 ≤ ε) : MeasureTheory.IntegrableOn (dampedPerronMajorantIntegrand ε L) (Set.Ioc 0 1) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorant_integrableOn_tail {ε L : ℝ} (hε : 0 < ε) (hL : 0 ≤ L) : MeasureTheory.IntegrableOn (dampedPerronMajorantIntegrand ε L) (Set.Ioi 1) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorant_integrableOn_Ioi {ε L : ℝ} (hε : 0 < ε) (hL : 0 ≤ L) : MeasureTheory.IntegrableOn (dampedPerronMajorantIntegrand ε L) (Set.Ioi 0) MeasureTheory.volume

Integrability on the positive half-line, obtained without any unproved limiting assertion.

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorant_integral_head_le {ε L : ℝ} (hε : 0 < ε) (hL : 0 ≤ L) : ∫ (t : ℝ) in Set.Ioc 0 1, dampedPerronMajorantIntegrand ε L t ≤ L

The (0,1] contribution.

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorant_integral_middle_le {ε L : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hL : 0 ≤ L) : ∫ (t : ℝ) in Set.Ioc 1 ε⁻¹, dampedPerronMajorantIntegrand ε L t ≤ Real.log ε⁻¹

The [1,1/ε] logarithmic contribution.

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorant_integral_tail_le_one {ε L : ℝ} (hε : 0 < ε) (hL : 0 ≤ L) : ∫ (t : ℝ) in Set.Ioi ε⁻¹, dampedPerronMajorantIntegrand ε L t ≤ 1

The exponentially damped tail beginning at 1/ε.

theorem AnalyticNumberTheory.LargeSieve.dampedPerronMajorant_integral_Ioi_le {ε L : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hL : 0 ≤ L) : ∫ (t : ℝ) in Set.Ioi 0, dampedPerronMajorantIntegrand ε L t ≤ L + Real.log (1 / ε) + 1

The full damped Perron majorant bound.