Documentation

MathlibNt.SieveTheory.LiLiuGoldbachB9PanDistribution

source
@[instance_reducible]
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB9PanDistribution (P : Prop) :
Decidable P
Equations
Instances For
    Inspect dependencies

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

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusDivCount (N d : ℕ) :
    ℕ

    The actual labelled zero-prefix divisor count, with output multiplicities.

    Equations
    Instances For
      Inspect dependencies

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

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

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

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

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

          source
          theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9Product_mul_ne_self {N m q : ℕ} (hm : m ∈ goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) :
          m * q ≠ N
          Inspect dependencies

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

          source
          theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9Product_mul_lt_iff_le {N m q : ℕ} (hm : m ∈ goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) :
          m * q < N ↔ m * q ≤ N
          Inspect dependencies

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

          source
          theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusAtom_output_dvd_iff_residue {N d : ℕ} {x : (_ : ℕ × ℕ) × ℕ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hx : x ∈ goldbachB10Atoms N 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) :
          d ∣ goldbachPi10Output N x ↔ (goldbachC10Prod x.fst).Coprime d ∧ ↑x.snd = ↑(N % d) * (↑(goldbachC10Prod x.fst))⁻¹

          The inverse class uses the original N, including its residue zero modulo one.

          Inspect dependencies

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

          source
          theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusProductResidueQFiber_card_eq_prefix {N m d : ℕ} (hm : m ∈ goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) (hc : m.Coprime d) :
          (goldbachB10ProductResidueQFiber N d 0 m).card = AnalyticNumberTheory.Sieve.primesInAPBelow N m d (N % d)
          Inspect dependencies

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

          source
          theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusDivCount_eq_product_sum {N d : ℕ} (hd : 1 ≤ d) (hdN : d.Coprime N) :
          ↑(goldbachB9PlusDivCount N d) = ∑ m ∈ goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)), if m.Coprime d then ↑(AnalyticNumberTheory.Sieve.primesInAPBelow N m d (N % d)) else 0
          Inspect dependencies

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

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

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusDivCount_eq_panAPPrefixCount {N A₁ A₂ d : ℕ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hsupp : goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) ⊆ Finset.Ioc A₁ A₂) :
            ↑(goldbachB9PlusDivCount N d) = goldbachB9PlusPanAPPrefixCount N A₁ A₂ d
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusGatedRemainder_eq_panError {N A₁ A₂ d : ℕ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hsupp : goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) ⊆ Finset.Ioc A₁ A₂) :
            goldbachB9PlusGatedRemainder N d = LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d (N % d) (goldbachC10CoeffReal N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)))

            One absolute value will be taken only after this entire m-sum.

            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9ProductSupport_pan_bounds {N m : ℕ} (hN : 2 ≤ N) (hm : m ∈ goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) :
            ↑N ^ (65 / 159) ≤ ↑m ∧ ↑m ≤ ↑N ^ (2 / 3)
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9ProductSupport_mem_panInterval {N : ℕ} {B : ℝ} (hN : 2 ≤ N) (hlow : LiuWeight.liuPanSourceIntervalLower N B < LiuWeight.liuSourceZ10 N) :
            goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) ⊆ Finset.Ioc (LiuWeight.liuPanSourceIntervalLower N B) (LiuWeight.liuPanSourceIntervalUpper N)
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9ProductSupport_eventually_panInterval (B : ℝ) :
            ∀ᶠ (N : ℕ) in Filter.atTop, goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) ⊆ Finset.Ioc (LiuWeight.liuPanSourceIntervalLower N B) (LiuWeight.liuPanSourceIntervalUpper N)
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusGatedRemainder_eventually_eq_panError (B : ℝ) :
            ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (d : ℕ), 1 ≤ d → d.Coprime N → goldbachB9PlusGatedRemainder N d = LiuWeight.liuMainPanCoprimeIntervalSum (LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) N (LiuWeight.liuPanSourceIntervalLower N B) (LiuWeight.liuPanSourceIntervalUpper N) d (N % d) (goldbachC10CoeffReal N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)))
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusGatedRemainder_abs_le_maxL {N A₁ A₂ d : ℕ} (hd : 1 ≤ d) (hdN : d.Coprime N) (hsupp : goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) ⊆ Finset.Ioc A₁ A₂) :
            |goldbachB9PlusGatedRemainder N d| ≤ LiuWeight.liuMainPanCoprimeIntervalMaxL (LiuWeight.liuLogarithmicIntegral (2 / Real.log 2)) N A₁ A₂ d (goldbachC10CoeffReal N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)))
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusGatedRemainder_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, |goldbachB9PlusGatedRemainder N d| ≤ C * ↑N / Real.log ↑N ^ U
            Inspect dependencies

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