noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshStep (n : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshStep n = (3 / 11 - 4 / 33) / (↑n + 1)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshPoint (n i : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshPoint n i = 4 / 33 + ↑i * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshStep_pos (n : ℕ) : 0 < goldbachG12HighMeshStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshPoint_succ (n i : ℕ) : goldbachG12HighMeshPoint n (i + 1) = goldbachG12HighMeshPoint n i + goldbachG12HighMeshStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshPoint_strictMono (n : ℕ) : StrictMono (goldbachG12HighMeshPoint n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshPoint_end (n : ℕ) : goldbachG12HighMeshPoint n (n + 1) = 3 / 11

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshPoint_bounds (n : ℕ) {i : ℕ} (hi : i ≤ n + 1) : goldbachG12HighMeshPoint n i ∈ Set.Icc (4 / 33) (3 / 11)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshPoint_pos (n i : ℕ) : 0 < goldbachG12HighMeshPoint n i

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshCell_subset (n : ℕ) (i : Fin (n + 1)) : Set.Icc (goldbachG12HighMeshPoint n ↑i) (goldbachG12HighMeshPoint n (↑i + 1)) ⊆ Set.Icc (4 / 33) (3 / 11)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMesh_exists_cell (n : ℕ) {x : ℝ} (hx : x ∈ Set.Ioc (4 / 33) (3 / 11)) : ∃ (i : Fin (n + 1)), x ∈ Set.Ioc (goldbachG12HighMeshPoint n ↑i) (goldbachG12HighMeshPoint n (↑i + 1))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMesh_index_mono {n : ℕ} {i j : Fin (n + 1)} {x y : ℝ} (hx : x ∈ Set.Ioc (goldbachG12HighMeshPoint n ↑i) (goldbachG12HighMeshPoint n (↑i + 1))) (hy : y ∈ Set.Ioc (goldbachG12HighMeshPoint n ↑j) (goldbachG12HighMeshPoint n (↑j + 1))) (hxy : x ≤ y) : i ≤ j

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCells (n : ℕ) : Finset ((Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1))

Only the first three coordinates are ordered.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCells n = {j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1) | j.1.1 ≤ j.1.2 ∧ j.1.2 ≤ j.2.1}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshLo (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) (i : Fin 4) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshLo n j i = if i = 3 then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshPoint n ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoords j i) else MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint n ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoords j i)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshHi (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) (i : Fin 4) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshHi n j i = if i = 3 then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12HighMeshPoint n (↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoords j i) + 1) else MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint n (↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoords j i) + 1)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshLo_pos (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) (i : Fin 4) : 0 < goldbachG12MeshLo n j i

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshLo_lt_hi (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) (i : Fin 4) : goldbachG12MeshLo n j i < goldbachG12MeshHi n j i

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels_subset_primeBox (N : ℕ) : goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) ⊆ goldbachG11PrimeBox N ![4 / 53, 4 / 53, 4 / 53, 4 / 33] ![4 / 33, 4 / 33, 4 / 33, 3 / 11]

The closed original cross is covered without enlarging its geometric domain.

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshBox : Set ((ℝ × ℝ) × ℝ × ℝ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshBox = (Set.Ioc (4 / 53) (4 / 33) ×ˢ Set.Ioc (4 / 53) (4 / 33)) ×ˢ Set.Ioc (4 / 53) (4 / 33) ×ˢ Set.Ioc (4 / 33) (3 / 11)

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshAmbient : Set ((ℝ × ℝ) × ℝ × ℝ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshAmbient = (Set.Icc (4 / 53) (4 / 33) ×ˢ Set.Icc (4 / 53) (4 / 33)) ×ˢ Set.Icc (4 / 53) (4 / 33) ×ˢ Set.Icc (4 / 33) (3 / 11)

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshSource : Set ((ℝ × ℝ) × ℝ × ℝ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshSource = {x : (ℝ × ℝ) × ℝ × ℝ | x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshBox ∧ x.1.1 ≤ x.1.2 ∧ x.1.2 ≤ x.2.1}

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCell (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) : Set ((ℝ × ℝ) × ℝ × ℝ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCell n j = (Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshLo n j 0) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshHi n j 0) ×ˢ Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshLo n j 1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshHi n j 1)) ×ˢ Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshLo n j 2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshHi n j 2) ×ˢ Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshLo n j 3) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshHi n j 3)

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshRegion (n : ℕ) : Set ((ℝ × ℝ) × ℝ × ℝ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshRegion n = ⋃ j ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCells n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCell n j

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachG12MeshCell (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) : MeasurableSet (goldbachG12MeshCell n j)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachG12MeshAmbient : MeasurableSet goldbachG12MeshAmbient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.isCompact_goldbachG12MeshAmbient : IsCompact goldbachG12MeshAmbient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachG12MeshSource : MeasurableSet goldbachG12MeshSource

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshBox_subset_ambient : goldbachG12MeshBox ⊆ goldbachG12MeshAmbient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCell_subset_box (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) : goldbachG12MeshCell n j ⊆ goldbachG12MeshBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCell_unique {n : ℕ} {j k : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)} {x : (ℝ × ℝ) × ℝ × ℝ} (hj : x ∈ goldbachG12MeshCell n j) (hk : x ∈ goldbachG12MeshCell n k) : j = k

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshBox_cover (n : ℕ) {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG12MeshBox) : ∃ (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)), x ∈ goldbachG12MeshCell n j

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshSource_cover (n : ℕ) {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG12MeshSource) : ∃ j ∈ goldbachG12MeshCells n, x ∈ goldbachG12MeshCell n j

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCell_order_error {n : ℕ} {j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)} (hj : j ∈ goldbachG12MeshCells n) {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG12MeshCell n j) : x.1.1 < x.1.2 + goldbachG11MeshStep n ∧ x.1.2 < x.2.1 + goldbachG11MeshStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Mesh_prime_cover (n N : ℕ) (hN : 4 ≤ N) (v : GoldbachG11Label) (hv : v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) : ∃ j ∈ goldbachG12MeshCells n, v ∈ goldbachG11PrimeBox N (goldbachG12MeshLo n j) (goldbachG12MeshHi n j)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshDensity (x : (ℝ × ℝ) × ℝ × ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshDensity x = MathlibNt.SieveTheory.LiuWeight.liuLogDensity x.1 * MathlibNt.SieveTheory.LiuWeight.liuLogDensity x.2

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshIntegrand (h : ℝ → ℝ) (x : (ℝ × ℝ) × ℝ × ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshIntegrand h x = h x.1.1 / x.1.2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshDensity x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachG12MeshDensity : ContinuousOn goldbachG12MeshDensity goldbachG12MeshAmbient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshDensity_nonneg {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG12MeshAmbient) : 0 ≤ goldbachG12MeshDensity x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrableOn_goldbachG12MeshDensity {s : Set ((ℝ × ℝ) × ℝ × ℝ)} (hs : MeasurableSet s) (hsub : s ⊆ goldbachG12MeshAmbient) : MeasureTheory.IntegrableOn goldbachG12MeshDensity s MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_goldbachG12MeshSource (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) : MeasureTheory.Integrable (goldbachG12MeshSource.indicator (goldbachG12MeshIntegrand h)) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LogBoxMass_eq_meshIntegral (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) : goldbachG11LogBoxMass (goldbachG12MeshLo n j) (goldbachG12MeshHi n j) = ∫ (x : (ℝ × ℝ) × ℝ × ℝ) in goldbachG12MeshCell n j, goldbachG12MeshDensity x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshSource_mem_iff (r q s t : ℝ) : ((r, q), s, t) ∈ goldbachG12MeshSource ↔ r ∈ Set.Ioc (4 / 53) (4 / 33) ∧ q ∈ Set.Icc r (4 / 33) ∧ s ∈ Set.Icc q (4 / 33) ∧ t ∈ Set.Ioc (4 / 33) (3 / 11)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PrimeIntegral_eq_meshSource (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) : goldbachG12PrimeIntegral h = ∫ (x : (ℝ × ℝ) × ℝ × ℝ), goldbachG12MeshSource.indicator (goldbachG12MeshIntegrand h) x

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshUpperIntegrand h n x = ∑ j ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCells n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoeff h n j * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCell n j).indicator MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshDensity x

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshUpperSum h n = ∑ j ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshCells n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoeff h n j * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LogBoxMass (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshLo n j) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshHi n j)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachG12MeshCoeff (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 ∈ goldbachG12MeshCell 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_goldbachG12MeshUpperIntegrand (h : ℝ → ℝ) (n : ℕ) : MeasureTheory.Integrable (goldbachG12MeshUpperIntegrand h n) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshUpperSum_eq_integral (h : ℝ → ℝ) (n : ℕ) : goldbachG12MeshUpperSum h n = ∫ (x : (ℝ × ℝ) × ℝ × ℝ), goldbachG12MeshUpperIntegrand h n x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshUpperIntegrand_eq_of_mem (h : ℝ → ℝ) {n : ℕ} {j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)} (hj : j ∈ goldbachG12MeshCells n) {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG12MeshCell n j) : goldbachG12MeshUpperIntegrand h n x = goldbachG11MeshCoeff h n j * goldbachG12MeshDensity x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshUpperIntegrand_eq_zero (h : ℝ → ℝ) {n : ℕ} {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∉ goldbachG12MeshRegion n) : goldbachG12MeshUpperIntegrand h n x = 0

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

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshUpperIntegrand_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 : (ℝ × ℝ) × ℝ × ℝ) : ‖goldbachG12MeshUpperIntegrand h n x‖ ≤ M / (4 / 53) * goldbachG12MeshAmbient.indicator goldbachG12MeshDensity x

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MeshUpperSum_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 : ℕ), goldbachG12MeshUpperSum h n ≤ goldbachG12PrimeIntegral h + ν