noncomputable def MathlibNt.SieveTheory.LinearSieve.M (z x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LinearSieve.M z x = Real.log z / Real.log x

noncomputable def MathlibNt.SieveTheory.LinearSieve.dens (z x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LinearSieve.dens z x = Real.log z / (x * Real.log x ^ 2)

theorem MathlibNt.SieveTheory.LinearSieve.deriv_M {z x : ℝ} (hx : 1 < x) : HasDerivAt (M z) (-dens z x) x

theorem MathlibNt.SieveTheory.LinearSieve.dens_continuousOn {z x y : ℝ} (hx : 1 < x) (hxy : x ≤ y) : ContinuousOn (dens z) (Set.uIcc x y)

theorem MathlibNt.SieveTheory.LinearSieve.M_sub_M_eq_integral {z x y : ℝ} (hx : 1 < x) (hxy : x ≤ y) : M z x - M z y = ∫ (t : ℝ) in x..y, dens z t

theorem MathlibNt.SieveTheory.LinearSieve.integrand_intervalIntegrable {z x y : ℝ} {g : ℝ → ℝ} (hx : 1 < x) (hxy : x ≤ y) (hg : MonotoneOn g (Set.Icc x y)) : IntervalIntegrable (fun (t : ℝ) => g t * dens z t) MeasureTheory.volume x y

theorem MathlibNt.SieveTheory.LinearSieve.local_mainRatio_le_integral {z x y : ℝ} {g : ℝ → ℝ} (hx : 1 < x) (hxy : x ≤ y) (hz : 1 < z) (hg : MonotoneOn g (Set.Icc x y)) : g x * (M z x - M z y) ≤ ∫ (t : ℝ) in x..y, g t * dens z t

theorem MathlibNt.SieveTheory.LinearSieve.finiteNodeMainRatioSum_le_integral {w z : ℝ} (g : ℝ → ℝ) (interior : List ℝ) (hw : 1 < w) (hwz : w ≤ z) (hnodes : List.Pairwise (fun (x1 x2 : ℝ) => x1 ≤ x2) (w :: interior ++ [z])) (hg : MonotoneOn g (Set.Icc w z)) : finiteNodeMainRatioSum z g (w :: interior ++ [z]) ≤ ∫ (x : ℝ) in w..z, g x * (Real.log z / (x * Real.log x ^ 2))

A finite left-node Stieltjes sum for log z / log x is bounded by the corresponding continuous main integral. The list includes the genuine endpoints, and only sortedness and monotonicity are used.