noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeInterval (N : ℕ) (a b : ℝ) : Finset ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeInterval N a b = {p ∈ Finset.range (MathlibNt.SieveTheory.PrimeReciprocalLogScale.rpowFloor N b + 1) | Nat.Prime p ∧ ↑N ^ a < ↑p ∧ ↑p ≤ ↑N ^ b}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG11PrimeInterval {N p : ℕ} {a b : ℝ} : p ∈ goldbachG11PrimeInterval N a b ↔ Nat.Prime p ∧ ↑N ^ a < ↑p ∧ ↑p ≤ ↑N ^ b

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBox (N : ℕ) (lo hi : Fin 4 → ℝ) : Finset GoldbachG11Label

Coordinates 0,1,2,3 are r,q,s,t; the carrier keeps the production sigma order.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBox N lo hi = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeInterval N (lo 3) (hi 3)).sigma fun (_t : ℕ) => (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeInterval N (lo 2) (hi 2)).sigma fun (_s : ℕ) => (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeInterval N (lo 0) (hi 0)).sigma fun (_r : ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeInterval N (lo 1) (hi 1)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBoxMass (N : ℕ) (lo hi : Fin 4 → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBoxMass N lo hi = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBox N lo hi, 1 / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LogBoxMass (lo hi : Fin 4 → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LogBoxMass lo hi = MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (lo 0) (hi 0) (lo 1) (hi 1) * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (lo 2) (hi 2) (lo 3) (hi 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBoxMass_eq_rectangles (N : ℕ) (lo hi : Fin 4 → ℝ) : goldbachG11PrimeBoxMass N lo hi = PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N (lo 0) (hi 0) (lo 1) (hi 1) * PrimeReciprocalLogRectangle.primeReciprocalLogRectangle N (lo 2) (hi 2) (lo 3) (hi 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachG11PrimeBoxMass (lo hi : Fin 4 → ℝ) (hlo : ∀ (i : Fin 4), 0 < lo i) (hhi : ∀ (i : Fin 4), lo i < hi i) : Filter.Tendsto (fun (N : ℕ) => goldbachG11PrimeBoxMass N lo hi) Filter.atTop (nhds (goldbachG11LogBoxMass lo hi))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachG11PrimeBoxMass_sum {ι : Type u_1} (S : Finset ι) (c : ι → ℝ) (lo hi : ι → Fin 4 → ℝ) (hlo : ∀ j ∈ S, ∀ (i : Fin 4), 0 < lo j i) (hhi : ∀ j ∈ S, ∀ (i : Fin 4), lo j i < hi j i) : Filter.Tendsto (fun (N : ℕ) => ∑ j ∈ S, c j * goldbachG11PrimeBoxMass N (lo j) (hi j)) Filter.atTop (nhds (∑ j ∈ S, c j * goldbachG11LogBoxMass (lo j) (hi j)))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels_subset_primeBox (N : ℕ) : goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ⊆ goldbachG11PrimeBox N (fun (x : Fin 4) => 4 / 53) fun (x : Fin 4) => 4 / 33

The strict lower endpoint is justified by the prime-cutoff theorem, not discarded.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrderedPrimeLabels (N : ℕ) : Finset GoldbachG11Label

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrderedPrimeLabels N = {v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBox N (fun (x : Fin 4) => 4 / 53) fun (x : Fin 4) => 4 / 33 | v.snd.snd.fst ≤ v.snd.snd.snd ∧ v.snd.snd.snd ≤ v.snd.fst ∧ v.snd.fst ≤ v.fst}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels_eq_coprime_filter (N : ℕ) : goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) = {v ∈ goldbachG11OrderedPrimeLabels N | (goldbachG11LabelProd v).Coprime N}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_eq_logCoordinateSum (h : ℝ → ℝ) (N : ℕ) : goldbachG11PrimeKernel h N = ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), h (Real.log ↑v.snd.snd.fst / Real.log ↑N) / (Real.log ↑v.snd.snd.snd / Real.log ↑N) * (1 / ↑(goldbachG11LabelProd v))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_le_orderedSum (h : ℝ → ℝ) (hh : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) {N : ℕ} (hN : 4 ≤ N) : goldbachG11PrimeKernel h N ≤ ∑ v ∈ goldbachG11OrderedPrimeLabels N, h (Real.log ↑v.snd.snd.fst / Real.log ↑N) * Real.log ↑N / (↑(goldbachG11LabelProd v) * Real.log ↑v.snd.snd.snd)

Removing coprimality is only an upper bound; ordering and all diagonals remain.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBoxContribution (h : ℝ → ℝ) (N : ℕ) (lo hi : Fin 4 → ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBoxContribution h N lo hi = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) with v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBox N lo hi, h (Real.log ↑v.snd.snd.fst / Real.log ↑N) * Real.log ↑N / (↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v) * Real.log ↑v.snd.snd.snd)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeBoxContribution_le (h : ℝ → ℝ) {N : ℕ} (hN : 4 ≤ N) (lo hi : Fin 4 → ℝ) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ r ∈ Set.Ioc (lo 0) (hi 0), ∀ q ∈ Set.Ioc (lo 1) (hi 1), h r / q ≤ C) : goldbachG11PrimeBoxContribution h N lo hi ≤ C * goldbachG11PrimeBoxMass N lo hi

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_le_boxCover {ι : Type u_1} (S : Finset ι) (h : ℝ → ℝ) (hh : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) {N : ℕ} (hN : 4 ≤ N) (lo hi : ι → Fin 4 → ℝ) (C : ι → ℝ) (hC : ∀ j ∈ S, 0 ≤ C j) (hbound : ∀ j ∈ S, ∀ r ∈ Set.Ioc (lo j 0) (hi j 0), ∀ q ∈ Set.Ioc (lo j 1) (hi j 1), h r / q ≤ C j) (hcover : ∀ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ∃ j ∈ S, v ∈ goldbachG11PrimeBox N (lo j) (hi j)) : goldbachG11PrimeKernel h N ≤ ∑ j ∈ S, C j * goldbachG11PrimeBoxMass N (lo j) (hi j)

Finite covers may overlap. This is not an assumption about a prime-to-integral limit.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_le_fixedCover_eventually {ι : Type u_1} (S : Finset ι) (h : ℝ → ℝ) (hh : ∀ x ∈ Set.Icc (4 / 53) (4 / 33), 0 ≤ h x) (lo hi : ι → Fin 4 → ℝ) (C : ι → ℝ) (hlo : ∀ j ∈ S, ∀ (i : Fin 4), 0 < lo j i) (hhi : ∀ j ∈ S, ∀ (i : Fin 4), lo j i < hi j i) (hC : ∀ j ∈ S, 0 ≤ C j) (hbound : ∀ j ∈ S, ∀ r ∈ Set.Ioc (lo j 0) (hi j 0), ∀ q ∈ Set.Ioc (lo j 1) (hi j 1), h r / q ≤ C j) (hcover : ∀ (N : ℕ), 4 ≤ N → ∀ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ∃ j ∈ S, v ∈ goldbachG11PrimeBox N (lo j) (hi j)) (ν : ℝ) (hν : 0 < ν) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG11PrimeKernel h N ≤ ∑ j ∈ S, C j * goldbachG11LogBoxMass (lo j) (hi j) + ν

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_triangle (S : Finset ℕ) (w : ℕ → ℝ) : 2 * ∑ s ∈ S, ∑ t ∈ S with s ≤ t, w s * w t = (∑ s ∈ S, w s) ^ 2 + ∑ s ∈ S, w s ^ 2

Exact finite triangular identity. The diagonal is present with its full weight.