Exponential control from the constructed JR hat producer

The factor s is cancelled against the denominator of the actual hat formula. The all-depth theorem is used only in its moving range and at its rounded natural cutoff. Constants are selected before the sieve, density, and depth.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.jrHatDecayConstant : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.jrHatDecayConstant = Real.exp 2 * (1 + Real.exp 1)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.jrHatDecayConstant_pos : 0 < jrHatDecayConstant

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.jr_hat_mul_coordinate_le_exp (sign : SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) {s : ℝ} (hs : 2 ≤ s) : s * JurkatRichert1965ChenGammaOneQOne.jr1965Section13HatLayers.T sign s ≤ jrHatDecayConstant * Real.exp (-s)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.jr_errorEnvelope_le_exp (N : ℕ) {R s : ℝ} (hs : 2 ≤ s) (hbudget : s ^ 13 ≤ Real.log R) : SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope JurkatRichert1965ChenGammaOneQOne.jr1965Section13HatLayers N R 12 s ≤ Real.exp 1 * (jrHatDecayConstant * Real.exp (-s))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.exists_jr_finiteSourceLayer_exp_bound : ∃ (A : ℝ), 0 < A ∧ ∀ (N : ℕ) (s : ℝ), 1 ≤ N → 2 ≤ s → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N → SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s ≤ A * Real.exp (-s)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.sourceParameters_twelve_third_five : SuzukiClaim145SourceParameters 12 (1 / 3) 5

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.SmallRosser.exists_actualT_exp_bound : ∃ (A : ℝ) (B : ℝ), 0 < A ∧ 0 < B ∧ ∀ (S : BoundingSieve) (K : ℝ) (N R : ℕ) (s : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 1 ≤ N → 2 ≤ R → 2 ≤ s → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N → s ^ 13 ≤ Real.log ↑R → Real.exp 1 ≤ Real.log ↑R → 2 ≤ ⌈↑R ^ (1 / s)⌉₊ → suzukiActualT S N R ⌈↑R ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑R ^ (1 / s)⌉₊ * (A * Real.exp (-s) + B * Real.exp √K * Real.exp (-s) * Real.log ↑R ^ (-(1 / 3)))

Genuine all-depth exponential estimate, from the constructed source producer. The numerical budget implies, rather than removes, its moving range.