noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshUpperIntegrand (h : ℝ → ℝ) (n : ℕ) (x : (ℝ × ℝ) × ℝ × ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshUpperIntegrand h n x = ∑ j ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCells n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoeff h n j * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCell n j).indicator MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshDensity x

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshUpperSum (h : ℝ → ℝ) (n : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshUpperSum h n = ∑ j ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCells n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoeff h n j * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LogBoxMass (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshLo n j) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshHi n j)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachG11MeshStep : Filter.Tendsto goldbachG11MeshStep Filter.atTop (nhds 0)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachG11Mesh_sameCell (i : (n : ℕ) → Fin (n + 1)) (y : ℕ → ℝ) {x : ℝ} (hx : ∀ (n : ℕ), x ∈ Set.Icc (goldbachG11MeshPoint n ↑(i n)) (goldbachG11MeshPoint n (↑(i n) + 1))) (hy : ∀ (n : ℕ), y n ∈ Set.Icc (goldbachG11MeshPoint n ↑(i n)) (goldbachG11MeshPoint n (↑(i n) + 1))) : Filter.Tendsto y Filter.atTop (nhds x)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachG11MeshSup (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (i : (n : ℕ) → Fin (n + 1)) {x : ℝ} (hx : ∀ (n : ℕ), x ∈ Set.Icc (goldbachG11MeshPoint n ↑(i n)) (goldbachG11MeshPoint n (↑(i n) + 1))) : Filter.Tendsto (fun (n : ℕ) => goldbachG11MeshSup h n (i n)) Filter.atTop (nhds (h x))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachG11MeshCoeff (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (j : (n : ℕ) → (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) {x : (ℝ × ℝ) × ℝ × ℝ} (hx : ∀ (n : ℕ), x ∈ goldbachG11MeshCell n (j n)) : Filter.Tendsto (fun (n : ℕ) => goldbachG11MeshCoeff h n (j n)) Filter.atTop (nhds (h x.1.1 / x.1.2))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_goldbachG11MeshUpperIntegrand (h : ℝ → ℝ) (n : ℕ) : MeasureTheory.Integrable (goldbachG11MeshUpperIntegrand h n) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshUpperSum_eq_integral (h : ℝ → ℝ) (n : ℕ) : goldbachG11MeshUpperSum h n = ∫ (x : (ℝ × ℝ) × ℝ × ℝ), goldbachG11MeshUpperIntegrand h n x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshUpperIntegrand_eq_of_mem (h : ℝ → ℝ) {n : ℕ} {j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)} (hj : j ∈ goldbachG11MeshCells n) {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG11MeshCell n j) : goldbachG11MeshUpperIntegrand h n x = goldbachG11MeshCoeff h n j * goldbachG11MeshDensity x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshUpperIntegrand_eq_zero (h : ℝ → ℝ) {n : ℕ} {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∉ goldbachG11MeshRegion n) : goldbachG11MeshUpperIntegrand h n x = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshRegion_eventually_not_mem {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∉ goldbachG11MeshSource) : ∀ᶠ (n : ℕ) in Filter.atTop, x ∉ goldbachG11MeshRegion n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachG11MeshUpperIntegrand (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (x : (ℝ × ℝ) × ℝ × ℝ) : Filter.Tendsto (fun (n : ℕ) => goldbachG11MeshUpperIntegrand h n x) Filter.atTop (nhds (goldbachG11MeshSource.indicator (goldbachG11MeshIntegrand h) x))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoeff_le (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) {M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), h x ≤ M) (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) : goldbachG11MeshCoeff h n j ≤ M / (4 / 53)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshUpperIntegrand_dominated (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (hpos : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) {M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), h x ≤ M) (n : ℕ) (x : (ℝ × ℝ) × ℝ × ℝ) : ‖goldbachG11MeshUpperIntegrand h n x‖ ≤ M / (4 / 53) * goldbachG11MeshAmbient.indicator goldbachG11MeshDensity x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachG11MeshUpperSum (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (hpos : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) : Filter.Tendsto (goldbachG11MeshUpperSum h) Filter.atTop (nhds (goldbachG11PrimeIntegral h))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshUpperSum_exists_le_integral (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (hpos : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) (ν : ℝ) (hν : 0 < ν) : ∃ (n : ℕ), goldbachG11MeshUpperSum h n ≤ goldbachG11PrimeIntegral h + ν