Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG11LinkedDistribution

G11 geometric prime-window distribution from a proved common profile #

The two complete prime-count-centered prefixes use the same effective support, coefficient and source constants. No output-prime condition is inserted into the coefficient.

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_balanced_support {N m : ℕ} {ε : ℝ} (hm : m ∈ goldbachG11EffectiveProductSupport N ε) :
↑N ^ (4 / 53) ≤ ↑m ∧ ↑m ≤ ↑N ^ (1 - 4 / 53)
Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_balanced_support · compiled type and proof/definition references.

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_profiles_and_coefficient {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hz : 2 ≤ ↑N ^ (4 / 53)) (hm : m ∈ goldbachG11EffectiveProductSupport N ε) :
(2 ≤ goldbachG11PiLiHi N m ∧ ↑m * goldbachG11PiLiHi N m ≤ ↑N) ∧ (2 ≤ goldbachG11PiLiLo N ε m ∧ ↑m * goldbachG11PiLiLo N ε m ≤ ↑N) ∧ |goldbachG11EffectiveProductCoefficient N ε m| ≤ 1
Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_profiles_and_coefficient · compiled type and proof/definition references.

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual (N : ℕ) (ε : ℝ) (d b : ℕ) :
ℝ
Equations
Instances For
    Inspect dependencies

    MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual · compiled type and proof/definition references.

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual_eq_prefix_sub {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (d b : ℕ) :
    goldbachG11LinkedWindowResidual N ε d b = Wu2004MeanValue.primeCenteredAPSum (goldbachG11EffectiveProductSupport N ε) (goldbachG11EffectiveProductCoefficient N ε) (goldbachG11PiLiHi N) d b - Wu2004MeanValue.primeCenteredAPSum (goldbachG11EffectiveProductSupport N ε) (goldbachG11EffectiveProductCoefficient N ε) (goldbachG11PiLiLo N ε) d b
    Inspect dependencies

    MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual_eq_prefix_sub · compiled type and proof/definition references.

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual_weighted (A : ℝ) (hA : 0 < A) :
    ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (Q : ℕ) (b : ℕ → ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → (∀ d ∈ Finset.Icc 1 Q, (b d).Coprime d) → ∑ d ∈ Finset.Icc 1 Q, Wu2004MeanValue.wuModulusWeight d * |goldbachG11LinkedWindowResidual N ε d (b d)| ≤ C * ↑N / Real.log ↑N ^ A

    A single source witness pays for both complete prefixes, uniformly in epsilon.

    Inspect dependencies

    MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual_weighted · compiled type and proof/definition references.

    source
    def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedCompletedResidue (N d : ℕ) :
    ℕ
    Equations
    Instances For
      Inspect dependencies

      MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedCompletedResidue · compiled type and proof/definition references.

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedCompletedResidue_coprime (N d : ℕ) :
      (goldbachG11LinkedCompletedResidue N d).Coprime d
      Inspect dependencies

      MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedCompletedResidue_coprime · compiled type and proof/definition references.

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedCompletedResidue_eq {N d : ℕ} (h : N.Coprime d) :
      goldbachG11LinkedCompletedResidue N d = N
      Inspect dependencies

      MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedCompletedResidue_eq · compiled type and proof/definition references.

      source
      def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli (N Q : ℕ) :
      Finset ℕ
      Equations
      Instances For
        Inspect dependencies

        MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedModuli · compiled type and proof/definition references.

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_one_le_weight {d : ℕ} (hd : Squarefree d) :
        1 ≤ Wu2004MeanValue.wuModulusWeight d
        Inspect dependencies

        MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_one_le_weight · compiled type and proof/definition references.

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual_squarefree (A : ℝ) (hA : 0 < A) :
        ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG11LinkedWindowResidual N ε d N| ≤ C * ↑N / Real.log ↑N ^ A

        Unweighting is restricted to squarefree moduli; the on-carrier residue stays N.

        Inspect dependencies

        MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual_squarefree · compiled type and proof/definition references.

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual_epsilon_one (N d b : ℕ) :
        goldbachG11LinkedWindowResidual N 1 d b = 0
        Inspect dependencies

        MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedWindowResidual_epsilon_one · compiled type and proof/definition references.