def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Proposition131MovingDelayedCurrentRatio (H : Section13HatLayers) (sign : ErrorSign) (d M : ℝ) : Prop

The pp. 90--91 input from Proposition 13.1(i),(iii), stated before the perturbation calculus. It is only a delayed/current DDE ratio and does not contain the differential certificate's conclusion.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Proposition131MovingDelayedCurrentRatio H sign d M = (0 < d ∧ 1 < M ∧ ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ∧ ∀ (t : ℝ), M ≤ t → 2 * (d + 1) * max 1 (Real.log (1 + t ^ d / Real.log D)) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign t ≤ t * H.T sign.opposite (t - 1))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.moving_perturbationSlope_le_log {D d t : ℝ} (hlog : 0 < Real.log D) (hd : 0 ≤ d) (ht : 0 < t) : perturbationSlope D d 0 t ≤ (d + 1) * Real.log (1 + t ^ d / Real.log D)

Bound the moving perturbation slope by its logarithmic majorant.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.moving_below_cutoff_z_le_one {D d t : ℝ} (hlog : 0 < Real.log D) (hd : 0 < d) (ht : 0 < t) (hcut : t ≤ Real.log D ^ (1 / d)) : t ^ d / Real.log D ≤ 1

Below the moving cutoff, the normalized real power is at most one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.moving_above_cutoff_one_lt_z {D d t : ℝ} (hlog : 0 < Real.log D) (hd : 0 < d) (hcut : Real.log D ^ (1 / d) < t) : 1 < t ^ d / Real.log D

Above the moving cutoff, the normalized real power is strictly greater than one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.movingDDEAsymptoticCertificate_of_proposition131_ratio {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {d M : ℝ} (hratio : Proposition131MovingDelayedCurrentRatio H sign d M) : MovingDDEAsymptoticCertificate H sign d M

The source delayed/current ratio proves the moving differential certificate by splitting at (log D)^(1/d) exactly as on pp. 90--91.