Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiLemma144ExplicitRemaindersSourceOrder

Lemma 14.4, Case I: explicit remainder source order #

This file separates the three literal remainders at σ = sourceSigma D d and τ = s. It proves the elementary cutoff and logarithmic normalisations and freezes the first genuinely analytic comparison which is not supplied by the reachable production cone. In particular no source-order inequality is made a premise of an absorption theorem.

source
noncomputable def MathlibNt.SieveTheory.caseISigmaZeroDirectRemainder (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N D : ℕ) (C145 K d Δ : ℝ) :
ℝ

The direct Claim-14.5 packet used for Σ₀ at the moving endpoint.

Equations
Instances For
    source
    theorem MathlibNt.SieveTheory.suzukiVProduct_mono_antitone (S : BoundingSieve) {x y : ℝ} (hxy : x ≤ y) :
    SwitchingPrinciple.suzukiVProduct S y ≤ SwitchingPrinciple.suzukiVProduct S x

    The Euler product decreases when its cutoff increases.

    source
    theorem MathlibNt.SieveTheory.log_rpow_one_div_sourceSigma {D d : ℝ} (hD : 0 < D) :
    Real.log (D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) = Real.log D / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d

    The logarithm in both Lemma-8.7 endpoints is exactly log D / σ.

    source
    theorem MathlibNt.SieveTheory.caseISigmaZeroDirectRemainder_le_sourceOrder (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D z : ℕ} {C C145 K d Δ : ℝ} (hD : 1 < ↑D) (hll : 0 < Real.log (Real.log ↑D)) (hlllog : Real.log (Real.log ↑D) ≤ Real.log ↑D) (hzD : ↑z ≤ ↑D) (hσ : 0 < SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) (hC : 0 < C) (hC145 : 0 ≤ C145) (hE : 0 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) :
    caseISigmaZeroDirectRemainder S H N D C145 K d Δ ≤ caseISourceOrderCoefficient (C145 / C) (↑D) d * sigma12InheritedBudget S H N D z C K d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)

    The direct Claim-14.5 packet already has (indeed, is smaller than) the required 1/(loglog D * σ) source order. This is the complete Σ₀ normalisation; its hypotheses are only positivity/range data.

    source
    def MathlibNt.SieveTheory.CaseISigma11FiniteLayerEnvelopeFactor :
    Prop

    First concrete missing factor in the Σ₁₁ route. It is exactly the source comparison needed after expanding the endpoint denominator, not a renamed source-order or absorption inequality.

    Equations
    Instances For
      source
      def MathlibNt.SieveTheory.CaseISigma12QDEnvelopeFactor :
      Prop

      First concrete missing factor in the Σ₁₂ endpoint route. This is the literal pointwise q_D^∓(s) versus inherited envelope comparison.

      Equations
      Instances For
        source
        def MathlibNt.SieveTheory.CaseIEndpointSourceScalarFactors (d Δ : ℝ) :
        Prop

        The remaining common scalar factor after either Lemma-8.7 endpoint has been reduced to the inherited envelope. This is the precise asymptotic calculation still required: σ² loglog D / log D, with the extra (log D)^Δ only for Σ₁₁.

        Equations
        Instances For
          source
          theorem MathlibNt.SieveTheory.eventually_caseISigmaZeroCoefficient_le_sameC_gap {C C145 d Δ : ℝ} (hC : 0 < C) (hC145 : 0 ≤ C145) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) :
          ∀ᶠ (D : ℝ) in Filter.atTop, ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) Δ) / 2 ∧ caseISourceOrderCoefficient (C145 / C) D d ≤ 1 - q.ρ

          Once the direct Σ₀ packet has been normalised with coefficient C145 / C, the accepted scalar gap theorem absorbs that coefficient.