Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG12BuchstabUpperMass

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_canonical_cofactor_lower_bound {N : ℕ} {v : GoldbachG11Label} (hN : 2 ≤ N) (hv : v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) :
↑N ^ (4 / 11) ≤ ↑N / ↑(goldbachG11LabelProd v)

The cross has three lower prime labels and one upper label.

Inspect dependencies

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

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_rough_upper_buchstab (η : ℝ) (hη : 0 < η) :
∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), ↑(LiLiuPrereqBuchstab.roughCount (↑N / ↑(goldbachG11LabelProd v)) ↑v.snd.snd.snd) ≤ goldbachG11BuchstabMass (↑N / ↑(goldbachG11LabelProd v)) ↑v.snd.snd.snd + η * (↑N / ↑(goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd

Buchstab on the unconditioned rough cofactor mother, on the ORIGINAL cross. This is not the output-prime sieve and does not itself supply the second logarithm.

Inspect dependencies

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

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

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

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

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12FullRoughMass_le_buchstabUpper (η : ℝ) (hη : 0 < η) :
      ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG12FullRoughMass N ≤ goldbachG12BuchstabUpperMass N η
      Inspect dependencies

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