noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedMotherSlice (N : ℕ) (ρ : ℝ) (h : ℝ → ℝ) (a : ℕ → ℕ → Prop) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedMotherSlice N ρ h a = ∑ u ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedBodies N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ∑ p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedPrimeWindow N ρ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u) with (a (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd u)) p, h (Real.log ↑p / Real.log ↑N)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedRoughMass (N : ℕ) (ρ : ℝ) (h : ℝ → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedRoughMass N ρ h = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), h (Real.log ↑v.snd.snd.fst / Real.log ↑N) * ↑(LiLiuPrereqBuchstab.roughCount (ρ ^ 2 * ↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)) ↑v.snd.snd.snd)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ExpandedMother_split (N : ℕ) (ρ : ℝ) (h : ℝ → ℝ) (hh : ∀ (r : ℝ), 0 ≤ h r) : goldbachG11ExpandedMotherMass N ρ h ≤ ((goldbachG11ExpandedMotherSlice N ρ h fun (m p : ℕ) => p ≤ m.minFac ∧ ¬p ∣ N) + goldbachG11ExpandedMotherSlice N ρ h fun (x p : ℕ) => p ∣ N) + goldbachG11ExpandedMotherSlice N ρ h fun (m p : ℕ) => m.minFac < p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Expanded_ordered_pair_mem {N p : ℕ} {ρ : ℝ} {u : GoldbachG11SwitchedBody} (hu : u ∈ goldbachG11GoodSwitchedBodies N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hp : p ∈ goldbachG11ExpandedPrimeWindow N ρ (goldbachG11SwitchedBodyProd u)) (hpq : p ≤ (goldbachG11SwitchedBodyProd u).minFac) (hpN : ¬p ∣ N) : ⟨u.fst, ⟨u.snd.fst, ⟨p, u.snd.snd.fst⟩⟩⟩ ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ∧ u.snd.snd.snd ∈ LiLiuPrereqBuchstab.roughNumbers (ρ ^ 2 * ↑N / ↑(goldbachG11LabelProd ⟨u.fst, ⟨u.snd.fst, ⟨p, u.snd.snd.fst⟩⟩⟩)) ↑u.snd.snd.fst

The original five coordinates survive the enlarged upper endpoint.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Expanded_ordered_le_rough (N : ℕ) (ρ : ℝ) (h : ℝ → ℝ) (hh : ∀ (r : ℝ), 0 ≤ h r) : (goldbachG11ExpandedMotherSlice N ρ h fun (m p : ℕ) => p ≤ m.minFac ∧ ¬p ∣ N) ≤ goldbachG11ExpandedRoughMass N ρ h