Documentation

MathlibNt.SieveTheory.LiLiuGoldbachB9HighFirstDistribution

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

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

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

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

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

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

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

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

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

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachX9High_eq_gated_add_deleted (N d : ℕ) :
            goldbachX9High N = goldbachX9HighGated N d + goldbachX9HighDeleted N d
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstCommonRemainder_eq (N d : ℕ) :
            goldbachB9HighFirstCommonRemainder N d = goldbachB9HighFirstGatedRemainder N d - goldbachX9HighDeleted N d / ↑d.totient
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstCommonRemainder_one (N : ℕ) :
            goldbachX9HighDeleted N 1 = 0 ∧ goldbachB9HighFirstCommonRemainder N 1 = goldbachB9HighFirstGatedRemainder N 1
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstSupport_eventually_panInterval (B : ℝ) :
            ∀ᶠ (N : ℕ) in Filter.atTop, goldbachB9HighFirstSupport N ⊆ Finset.Ioc (LiuWeight.liuPanSourceIntervalLower N B) (LiuWeight.liuPanSourceIntervalUpper N)
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstDivCount_eq_product_sum {N d : ℕ} (hN : 2 ≤ N) (hd : 1 ≤ d) (hdN : d.Coprime N) :
            ↑(goldbachB9HighFirstDivCount N d) = ∑ m ∈ goldbachB9HighFirstSupport N, if m.Coprime d then ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N m d (N % d)) else 0

            Generic inverse residue geometry and the strict/closed prime prefix are reused pointwise.

            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstGatedRemainder_eq_panError {N A₁ A₂ d : ℕ} (hN : 2 ≤ N) (hd : 1 ≤ d) (hdN : d.Coprime N) (hs : goldbachB9HighFirstSupport N ⊆ Finset.Ioc A₁ A₂) :
            goldbachB9HighFirstGatedRemainder N d = LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d (N % d) (goldbachC10CoeffReal N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)))

            The entire high m-sum equals PanError before any absolute value is taken.

            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstGatedRemainder_log_saving (U : ℝ) (hU : 0 < U) :
            ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∑ d ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N B) with d.Coprime N, |goldbachB9HighFirstGatedRemainder N d| ≤ C * ↑N / Real.log ↑N ^ U

            Bounded Pan is called again with the actual high coefficient, bounded by one.

            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.abs_goldbachB9HighFirstCommonRemainder_le (N d : ℕ) :
            |goldbachB9HighFirstCommonRemainder N d| ≤ |goldbachB9HighFirstGatedRemainder N d| + gateLoss N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) (goldbachB9PlusLiWeight N) d
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstCommonRemainder_log_saving (U : ℝ) (hU : 0 < U) :
            ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∑ d ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N B) with d.Coprime N, |goldbachB9HighFirstCommonRemainder N d| ≤ C * ↑N / Real.log ↑N ^ U
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstBoundingSieve_rem_eq {N d : ℕ} (hEven : Even N) {Z : ℝ} (hd : d ∣ goldbachB10ProdPrimes N Z) :
            BoundingSieve.rem d = goldbachB9HighFirstCommonRemainder N d
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirst_upperErrSum_log_saving (U : ℝ) (hU : 0 < U) :
            ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (Z : ℝ), have Δ := ↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1); have S := goldbachB10BoundingSieve N hEven 0 (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) Z (goldbachX9High N); LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) ≤ C * ↑N / Real.log ↑N ^ U

            The actual strict Rosser support and |lambda| <= 1, with d=1 retained.

            Inspect dependencies

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