MathlibNt.SieveTheory.LiLiuGoldbachG12RoughElementary

source

theorem G12RoughBoundary.integer_band_reciprocal {a : ℝ} (ha : 1 ≤ a) {r : ℕ} (hr : 0 < r) :

∑ q ∈ Finset.Icc r ⌊a * ↑r⌋₊, 1 / ↑q ≤ a - 1 + 1 / ↑r

The closed integer interval pays its endpoint by 1/r.

Inspect dependencies

G12RoughBoundary.integer_band_reciprocal · compiled type and proof/definition references.

source

noncomputable def G12RoughBoundary.primes (N : ℕ) :

Finset ℕ

Equations

G12RoughBoundary.primes N = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeInterval N (4 / 53) (3 / 11)

Instances For

Inspect dependencies

G12RoughBoundary.primes · compiled type and proof/definition references.

source

noncomputable def G12RoughBoundary.harmonic (N : ℕ) :

ℝ

Equations

G12RoughBoundary.harmonic N = ∑ p ∈ G12RoughBoundary.primes N, 1 / ↑p

Instances For

Inspect dependencies

G12RoughBoundary.harmonic · compiled type and proof/definition references.

source

noncomputable def G12RoughBoundary.harmonicBound :

ℝ

Equations

G12RoughBoundary.harmonicBound = |Real.log (3 / 11 / (4 / 53))| + 1

Instances For

Inspect dependencies

G12RoughBoundary.harmonicBound · compiled type and proof/definition references.

source

theorem G12RoughBoundary.harmonicBound_pos :

0 < harmonicBound

Inspect dependencies

G12RoughBoundary.harmonicBound_pos · compiled type and proof/definition references.

source

theorem G12RoughBoundary.harmonic_nonneg (N : ℕ) :

0 ≤ harmonic N

Inspect dependencies

G12RoughBoundary.harmonic_nonneg · compiled type and proof/definition references.

source

theorem G12RoughBoundary.harmonic_eventually :

∃ (K : ℕ), ∀ (N : ℕ), K ≤ N → harmonic N ≤ harmonicBound

Inspect dependencies

G12RoughBoundary.harmonic_eventually · compiled type and proof/definition references.

source

noncomputable def G12RoughBoundary.labels (N : ℕ) :

Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label

Equations

G12RoughBoundary.labels N = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))

Instances For

Inspect dependencies

G12RoughBoundary.labels · compiled type and proof/definition references.

source

noncomputable def G12RoughBoundary.nearLabels (N : ℕ) (a : ℝ) :

Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label

Equations

G12RoughBoundary.nearLabels N a = {v ∈ G12RoughBoundary.labels N | ↑v.snd.snd.snd ≤ a * ↑v.snd.snd.fst}

Instances For

Inspect dependencies

G12RoughBoundary.nearLabels · compiled type and proof/definition references.

source

noncomputable def G12RoughBoundary.nearMass (N : ℕ) (a : ℝ) :

ℝ

Equations

G12RoughBoundary.nearMass N a = ∑ v ∈ G12RoughBoundary.nearLabels N a, ↑(LiLiuPrereqBuchstab.roughCount (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)) ↑v.snd.snd.snd)

Instances For

Inspect dependencies

G12RoughBoundary.nearMass · compiled type and proof/definition references.

source

noncomputable def G12RoughBoundary.nearReciprocal (N : ℕ) (a : ℝ) :

ℝ

Equations

G12RoughBoundary.nearReciprocal N a = ∑ v ∈ G12RoughBoundary.nearLabels N a, 1 / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)

Instances For

Inspect dependencies

G12RoughBoundary.nearReciprocal · compiled type and proof/definition references.

source

theorem G12RoughBoundary.labels_primes {N : ℕ} (hN : 1 ≤ N) {v : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label} (hv : v ∈ labels N) :

v.fst ∈ primes N ∧ v.snd.fst ∈ primes N ∧ v.snd.snd.fst ∈ primes N

All three unexpanded prime coordinates stay in the original exponent range.

Inspect dependencies

G12RoughBoundary.labels_primes · compiled type and proof/definition references.

source

theorem G12RoughBoundary.nearReciprocal_le {N : ℕ} (hN : 1 ≤ N) {a : ℝ} (ha : 1 ≤ a) :

nearReciprocal N a ≤ harmonic N ^ 3 * (a - 1 + 1 / ↑N ^ (4 / 53))

Expand q to integers, never any of r,s,t. All repeated labels remain.

Inspect dependencies

G12RoughBoundary.nearReciprocal_le · compiled type and proof/definition references.

source

theorem G12RoughBoundary.cofactor_eventually :

∃ (K : ℕ), 4 ≤ K ∧ ∀ (N : ℕ), K ≤ N → ∀ v ∈ labels N, ↑(LiLiuPrereqBuchstab.roughCount (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)) ↑v.snd.snd.snd) ≤ 2 * (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd

True uniform Buchstab, with a deliberately coarse fixed constant 2.

Inspect dependencies

G12RoughBoundary.cofactor_eventually · compiled type and proof/definition references.

source

theorem G12RoughBoundary.normalized_cofactor_le {N : ℕ} (hN : 4 ≤ N) {v : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label} (hv : v ∈ labels N) (hb : ↑(LiLiuPrereqBuchstab.roughCount (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)) ↑v.snd.snd.snd) ≤ 2 * (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd) :

Real.log ↑N / ↑N * ↑(LiLiuPrereqBuchstab.roughCount (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)) ↑v.snd.snd.snd) ≤ 53 / 2 * (1 / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v))

The log is the cofactor log, not a second output-prime saving.

Inspect dependencies

G12RoughBoundary.normalized_cofactor_le · compiled type and proof/definition references.