MathlibNt.SieveTheory.LiLiuGoldbachG11ProductCoefficient

source

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

(goldbachG11SwitchedBodyProd u).minFac = u.snd.snd.fst

Inspect dependencies

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

source

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

Finset ℕ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductSupport N z b = Finset.image MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedBodies N z b)

Instances For

Inspect dependencies

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

source

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

Finset GoldbachG11SwitchedBody

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFiber N z b m = {u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedBodies N z b | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u = m}

Instances For

Inspect dependencies

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

source

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

ℕ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N z b m = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFiber N z b m).card

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11ProductSupport_iff {N m : ℕ} {z b : ℝ} :

m ∈ goldbachG11ProductSupport N z b ↔ ∃ u ∈ goldbachG11GoodSwitchedBodies N z b, goldbachG11SwitchedBodyProd u = m

Inspect dependencies

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

source

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

u ∈ goldbachG11ProductFiber N z b m ↔ u ∈ goldbachG11GoodSwitchedBodies N z b ∧ goldbachG11SwitchedBodyProd u = m

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductSupport_data {N m : ℕ} {z b : ℝ} (hm : m ∈ goldbachG11ProductSupport N z b) :

0 < m ∧ m < N ∧ m.Coprime N ∧ z ≤ ↑m.minFac

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFiber_nonempty_iff {N m : ℕ} {z b : ℝ} :

(goldbachG11ProductFiber N z b m).Nonempty ↔ m ∈ goldbachG11ProductSupport N z b

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient_pos_iff {N m : ℕ} {z b : ℝ} :

0 < goldbachG11ProductCoefficient N z b m ↔ m ∈ goldbachG11ProductSupport N z b

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient_eq_zero_iff {N m : ℕ} {z b : ℝ} :

goldbachG11ProductCoefficient N z b m = 0 ↔ m ∉ goldbachG11ProductSupport N z b

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient_eq_zero_of_not_mem {N m : ℕ} {z b : ℝ} (hm : m ∉ goldbachG11ProductSupport N z b) :

goldbachG11ProductCoefficient N z b m = 0

Inspect dependencies

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

source

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

ℕ × ℕ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoordinates u = (u.snd.fst, u.fst)

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoordinates_injOn (N m : ℕ) (z b : ℝ) :

Set.InjOn goldbachG11ProductCoordinates ↑(goldbachG11ProductFiber N z b m)

Inspect dependencies

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

source

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

goldbachG11ProductCoordinates u ∈ (largePrimeDivisors m z).product (largePrimeDivisors m z)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient_le_four_hundred (N m : ℕ) :

goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m ≤ 400

Inspect dependencies

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

source

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

ℝ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedProductCoefficient N z b m = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N z b m) / 400

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedProductCoefficient_nonneg (N m : ℕ) (z b : ℝ) :

0 ≤ goldbachG11NormalizedProductCoefficient N z b m

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedProductCoefficient_le_one (N m : ℕ) :

goldbachG11NormalizedProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m ≤ 1

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedProductCoefficient_mul_four_hundred (N m : ℕ) (z b : ℝ) :

400 * goldbachG11NormalizedProductCoefficient N z b m = ↑(goldbachG11ProductCoefficient N z b m)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedProductCoefficient_eq_zero_of_not_mem {N m : ℕ} {z b : ℝ} (hm : m ∉ goldbachG11ProductSupport N z b) :

goldbachG11NormalizedProductCoefficient N z b m = 0

Inspect dependencies

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