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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshStep n = (4 / 33 - 4 / 53) / (↑n + 1)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint n i = 4 / 53 + ↑i * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshStep n

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoords {α : Type u_1} (x : (α × α) × α × α) : Fin 4 → α

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoords x = ![x.1.1, x.1.2, x.2.1, x.2.2]

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCells 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 ∧ j.2.1 ≤ j.2.2}

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshLo n j i = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint n ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoords j i)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshHi n j i = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint n (↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoords j i) + 1)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshStep_pos (n : ℕ) : 0 < goldbachG11MeshStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint_succ (n i : ℕ) : goldbachG11MeshPoint n (i + 1) = goldbachG11MeshPoint n i + goldbachG11MeshStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint_strictMono (n : ℕ) : StrictMono (goldbachG11MeshPoint n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint_end (n : ℕ) : goldbachG11MeshPoint n (n + 1) = 4 / 33

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint_bounds (n : ℕ) {i : ℕ} (hi : i ≤ n + 1) : goldbachG11MeshPoint n i ∈ Set.Icc (4 / 53) (4 / 33)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint_pos (n i : ℕ) : 0 < goldbachG11MeshPoint n i

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCell_subset (n : ℕ) (i : Fin (n + 1)) : Set.Icc (goldbachG11MeshPoint n ↑i) (goldbachG11MeshPoint n (↑i + 1)) ⊆ Set.Icc (4 / 53) (4 / 33)

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

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshSup (h : ℝ → ℝ) (n : ℕ) (i : Fin (n + 1)) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshSup h n i = sSup (h '' Set.Icc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint n ↑i) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint n (↑i + 1)))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoeff (h : ℝ → ℝ) (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoeff h n j = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshSup h n j.1.1 / MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshPoint n ↑j.1.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshSup_attained (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (n : ℕ) (i : Fin (n + 1)) : ∃ x ∈ Set.Icc (goldbachG11MeshPoint n ↑i) (goldbachG11MeshPoint n (↑i + 1)), h x = goldbachG11MeshSup h n i

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshSup_le (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (n : ℕ) (i : Fin (n + 1)) {M : ℝ} (hM : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), h x ≤ M) : goldbachG11MeshSup h n i ≤ M

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCoeff_majorant (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) (hpos : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) {r q : ℝ} (hr : r ∈ Set.Ioc (goldbachG11MeshLo n j 0) (goldbachG11MeshHi n j 0)) (hq : q ∈ Set.Ioc (goldbachG11MeshLo n j 1) (goldbachG11MeshHi n j 1)) : h r / q ≤ goldbachG11MeshCoeff h n j