MathlibNt.SieveTheory.LiLiuGoldbachG11SwitchedMother

@[reducible, inline]

abbrev MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11SwitchedBody :

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11SwitchedBody = ((_ : ℕ) × (_ : ℕ) × (_ : ℕ) × ℕ)

Instances For

Inspect dependencies

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

source

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd (u : GoldbachG11SwitchedBody) :

ℕ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u = u.snd.snd.fst * u.snd.fst * u.fst * u.snd.snd.snd

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodies (N : ℕ) (z b : ℝ) :

Finset GoldbachG11SwitchedBody

Equations

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11SwitchedBodies_iff {N t s q k : ℕ} {z b : ℝ} :

⟨t, ⟨s, ⟨q, k⟩⟩⟩ ∈ goldbachG11SwitchedBodies N z b ↔ Nat.Prime q ∧ Nat.Prime s ∧ Nat.Prime t ∧ (q * s * t).Coprime N ∧ z ≤ ↑q ∧ q ≤ s ∧ s ≤ t ∧ ↑t ≤ b ∧ 1 ≤ k ∧ k ≤ N ∧ SurvivesSieve 1 (↑q) k ∧ q * s * t * k < N

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd_pos {N : ℕ} {z b : ℝ} {u : GoldbachG11SwitchedBody} (hu : u ∈ goldbachG11SwitchedBodies N z b) :

0 < goldbachG11SwitchedBodyProd u

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber (N : ℕ) (eps z : ℝ) (u : GoldbachG11SwitchedBody) :

Finset ℕ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber N eps z u = {r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z ↑u.snd.snd.fst | eps * ↑N < ↑(r * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u) ∧ r * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u < N ∧ Nat.Prime (N - r * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u)}

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11FirstPrimeFiber_iff {N r : ℕ} {eps z : ℝ} {u : GoldbachG11SwitchedBody} :

r ∈ goldbachG11FirstPrimeFiber N eps z u ↔ Nat.Prime r ∧ ¬r ∣ N ∧ z ≤ ↑r ∧ r ≤ u.snd.snd.fst ∧ eps * ↑N < ↑(r * goldbachG11SwitchedBodyProd u) ∧ r * goldbachG11SwitchedBodyProd u < N ∧ Nat.Prime (N - r * goldbachG11SwitchedBodyProd u)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber_interval_iff {N r : ℕ} {eps z : ℝ} {u : GoldbachG11SwitchedBody} (hB : 0 < goldbachG11SwitchedBodyProd u) :

r ∈ goldbachG11FirstPrimeFiber N eps z u ↔ r ∈ goldbachClosedPrimes N z ↑u.snd.snd.fst ∧ eps * ↑N / ↑(goldbachG11SwitchedBodyProd u) < ↑r ∧ ↑r < ↑N / ↑(goldbachG11SwitchedBodyProd u) ∧ Nat.Prime (N - r * goldbachG11SwitchedBodyProd u)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber_coprime_iff {N r : ℕ} {eps z : ℝ} {u : GoldbachG11SwitchedBody} (hr : r ∈ goldbachG11FirstPrimeFiber N eps z u) :

(r * goldbachG11SwitchedBodyProd u).Coprime N ↔ (goldbachG11SwitchedBodyProd u).Coprime N

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedBodies (N : ℕ) (z b : ℝ) :

Finset GoldbachG11SwitchedBody

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedBodies N z b = {u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodies N z b | (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u).Coprime N}

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11GoodSwitchedBodies_iff {N : ℕ} {z b : ℝ} {u : GoldbachG11SwitchedBody} :

u ∈ goldbachG11GoodSwitchedBodies N z b ↔ u ∈ goldbachG11SwitchedBodies N z b ∧ (goldbachG11SwitchedBodyProd u).Coprime N

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedTotal (N : ℕ) (eps z b : ℝ) :

ℤ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedTotal N eps z b = ∑ u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodies N z b, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber N eps z u).card

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal (N : ℕ) (eps z b : ℝ) :

ℤ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal N eps z b = ∑ u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedBodies N z b, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber N eps z u).card

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BadSwitchedTotal (N : ℕ) (eps z b : ℝ) :

ℤ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BadSwitchedTotal N eps z b = ∑ u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodies N z b with ¬(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u).Coprime N, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FirstPrimeFiber N eps z u).card

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedTotal_eq_good_add_bad (N : ℕ) (eps z b : ℝ) :

goldbachG11SwitchedTotal N eps z b = goldbachG11GoodSwitchedTotal N eps z b + goldbachG11BadSwitchedTotal N eps z b

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedTotal_sub_good_nonneg (N : ℕ) (eps z b : ℝ) :

0 ≤ goldbachG11SwitchedTotal N eps z b - goldbachG11GoodSwitchedTotal N eps z b

Inspect dependencies

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