Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiSection13PairingComparison

source
noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointPlus (s : ℝ) :
ℝ

The explicit standard adjoint for DDE(2,+1,β) at κ = 1. It is the polynomial standard solution r_{2,1} (up to positive scaling).

Equations
Instances For
    source
    def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointMinus (_s : ℝ) :
    ℝ

    The explicit standard adjoint for DDE(2,-1,β) at κ = 1.

    Equations
    Instances For
      source
      theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointPlus_dde (s : ℝ) :
      HasDerivAt (fun (u : ℝ) => u * section10KappaOneAdjointPlus u) (2 * section10KappaOneAdjointPlus s + section10KappaOneAdjointPlus (s + 1)) s
      source
      theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointMinus_dde (s : ℝ) :
      HasDerivAt (fun (u : ℝ) => u * section10KappaOneAdjointMinus u) (2 * section10KappaOneAdjointMinus s - section10KappaOneAdjointMinus (s + 1)) s
      source
      theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointPlus_pos {s : ℝ} (hs : 2 ≤ s) :
      0 < section10KappaOneAdjointPlus s
      source
      theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneAdjointMinus_pos (s : ℝ) :
      0 < section10KappaOneAdjointMinus s
      source
      theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10KappaOneStandardAdjointPlus :
      Section10StandardAdjoint section10KappaOneAdjointPlus

      Thus the previously missing positive standard-adjoint object is explicit at κ=1; no existence or positivity axiom is needed.

      source
      noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10SignedPairing (b : ℝ) (R r : ℝ → ℝ) (s : ℝ) :
      ℝ

      Signed Iwaniec pairing, retaining the coefficient b.

      Equations
      Instances For
        source
        theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10SignedPairing_hasDerivAt_zero {a b β s : ℝ} {R r : ℝ → ℝ} (hRcont : Continuous R) (hrcont : Continuous r) (_hs : β < s) (hs0 : s ≠ 0) (hR : HasDerivAt R (-(a * R s + b * R (s - 1)) / s) s) (hr : HasDerivAt (fun (u : ℝ) => u * r u) (a * r s + b * r (s + 1)) s) :
        HasDerivAt (section10SignedPairing b R r) 0 s

        Lemma 10.1, pointwise differential form: an original DDE solution paired with an adjoint solution has zero pairing derivative.

        source
        theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10SignedPairing_eq_of_dde {a b β x y : ℝ} {R r : ℝ → ℝ} (hxy : x ≤ y) (hβ : 1 ≤ β) (hx : β < x) (hRcont : Continuous R) (hrcont : Continuous r) (hR : ∀ (s : ℝ), β < s → HasDerivAt R (-(a * R s + b * R (s - 1)) / s) s) (hr : ∀ (s : ℝ), 0 < s → HasDerivAt (fun (u : ℝ) => u * r u) (a * r s + b * r (s + 1)) s) :
        section10SignedPairing b R r y = section10SignedPairing b R r x

        Lemma 10.1 on an interval. This is the actual comparison-side constancy bridge; pairing vanishing is not assumed.

        source
        theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13QhatAdjointCore {H : Section13HatLayers} (_hH : Section13HatContract H 2) :
        Section10StandardAdjoint section10KappaOneAdjointPlus

        The Q̂ DDE and the explicit positive adjoint are now fully constructed. The only omitted field is pairing-zero itself; unlike the old bridge, this record cannot conceal Lemma 10.17 or an adjacent-value estimate.