@[instance_reducible]

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

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightD6_le_goldbachQA (A : Finset ℕ) (N : ℕ) (z b : ℝ) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) : goldbachWeightD6 A N z b ≤ goldbachQA A N z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightD6_real_le_two_mul_div_z (A : Finset ℕ) (N : ℕ) (z b : ℝ) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hz : 2 ≤ z) : ↑(goldbachWeightD6 A N z b) ≤ 2 * ↑N / z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightB6pair_real_le_twenty_mul_div_b (A : Finset ℕ) (N : ℕ) {κ z b : ℝ} (hN : 1 ≤ N) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hk : 1 / 21 < κ) (hz : z = ↑N ^ κ) (_hz2 : 2 ≤ z) (hzb : z ≤ b) : ↑(goldbachWeightB6pair A N z b) ≤ 20 * ↑N / b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightB7_real_le_twenty_mul_div_b (A : Finset ℕ) (N : ℕ) {κ z b c : ℝ} (hN : 1 ≤ N) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hk : 1 / 21 < κ) (hz : z = ↑N ^ κ) (_hz2 : 2 ≤ z) (hzb : z ≤ b) (_hbc : b ≤ c) : ↑(goldbachWeightB7 A N z b c) ≤ 20 * ↑N / b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_initial_error_real_le_forty_two_mul_div_z (A : Finset ℕ) (N : ℕ) {κ z b c : ℝ} (hN : 1 ≤ N) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hk : 1 / 21 < κ) (hz : z = ↑N ^ κ) (hz2 : 2 ≤ z) (hzb : z ≤ b) (hbc : b ≤ c) : ↑(goldbachWeightD6 A N z b) + ↑(goldbachWeightB6pair A N z b) + ↑(goldbachWeightB7 A N z b c) ≤ 42 * ↑N / z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_initial_paid_real (A : Finset ℕ) (N : ℕ) {κ z b c : ℝ} (hN : 1 ≤ N) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hk : 1 / 21 < κ) (hz : z = ↑N ^ κ) (hz2 : 2 ≤ z) (hzb : z ≤ b) (hbc : b ≤ c) : ↑(goldbachS1 A N b) - ↑(goldbachS3Closed A N b c) ≥ ↑(goldbachS1 A N z) - ↑(goldbachS3Closed A N z c) + ↑(goldbachWeightG6 A N z b) + ↑(goldbachWeightG7 A N z b c) - ↑(goldbachWeightG14 A N z b) - ↑(goldbachWeightG15 A N z b c) - 42 * ↑N / z