MathlibNt.SieveTheory.LiLiuGoldbachB8FibreSieve

@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB8FibreSieve (P : Prop) :

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB8FibreSieve P = Classical.propDecidable P

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusSupport (N : ℕ) :

Finset ℕ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusSupport N = Finset.image (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutput N) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusAtoms N)

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusWeight (N p : ℕ) :

ℝ

Every output carries its full labelled fibre, not unit weight.

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusWeight N p = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutputFiber N p).card

Instances For

Inspect dependencies

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

source

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

ℕ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusDivCount N d = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusAtoms N | d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusOutput N x}.card

Instances For

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusMainMass (N : ℕ) :

ℝ

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusMainMass N = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductSupport N, MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑m)

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductSupport_one_lt_and_coprime {N m : ℕ} (hm : m ∈ goldbachC8ProductSupport N) :

1 < m ∧ m.Coprime N

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC8ProductSupport_two_le_quotient {N m : ℕ} (hm : m ∈ goldbachC8ProductSupport N) :

2 ≤ ↑N / ↑m

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusMainMass_nonneg (N : ℕ) :

0 ≤ goldbachB8PlusMainMass N

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusWeight_sum_eq_card_atoms (N : ℕ) :

∑ p ∈ goldbachB8PlusSupport N, goldbachB8PlusWeight N p = ↑(goldbachB8PlusAtoms N).card

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusNu :

ArithmeticFunction ℝ

Reciprocal totient on all moduli; it agrees with goldbachNu on squarefree moduli.

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusNu = { toFun := fun (d : ℕ) => 1 / ↑d.totient, map_zero' := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusNu._proof_1 }

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusNu_isMultiplicative :

goldbachB8PlusNu.IsMultiplicative

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusNu_eq_goldbachNu_of_squarefree {d : ℕ} (hd : Squarefree d) :

goldbachB8PlusNu d = AnalyticNumberTheory.Sieve.goldbachNu d

Inspect dependencies

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

source

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve (N : ℕ) (hEven : Even N) (Z : ℝ) :

BoundingSieve

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve N hEven Z = { support := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusSupport N, prodPrimes := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z, prodPrimes_squarefree := ⋯, weights := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusWeight N, weights_nonneg := ⋯, totalMass := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusMainMass N, nu := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusNu, nu_mult := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusNu_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

Instances For

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve_multSum_eq_divCount (N : ℕ) (hEven : Even N) (Z : ℝ) (d : ℕ) :

BoundingSieve.multSum d = ↑(goldbachB8PlusDivCount N d)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve_siftedSum_eq_card (N : ℕ) (hEven : Even N) (Z : ℝ) :

BoundingSieve.siftedSum = ↑(goldbachB8PlusSiftedAtoms N Z).card

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve_nu_eq_inv_totient (N : ℕ) (hEven : Even N) (Z : ℝ) (d : ℕ) :

(goldbachB8PlusBoundingSieve N hEven Z).nu d = 1 / ↑d.totient

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve_rem_eq_divCount_sub (N : ℕ) (hEven : Even N) (Z : ℝ) (d : ℕ) :

BoundingSieve.rem d = ↑(goldbachB8PlusDivCount N d) - goldbachB8PlusMainMass N / ↑d.totient

Inspect dependencies

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