@[instance_reducible]

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachEndpointBound P = Classical.propDecidable P

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB6_le_four_hundred_mul_div_y (A : Finset ℕ) (N : ℕ) {κ z y : ℝ} (hN : 1 ≤ N) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hk : 1 / 21 < κ) (hz : z = ↑N ^ κ) (hzy : z ≤ y) : ↑(goldbachB6 A N z y) ≤ 400 * ↑N / y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB6_le_four_hundred_mul_div_z (A : Finset ℕ) (N : ℕ) {κ z y : ℝ} (hN : 1 ≤ N) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hk : 1 / 21 < κ) (hz : z = ↑N ^ κ) (hzy : z ≤ y) : ↑(goldbachB6 A N z y) ≤ 400 * ↑N / z