noncomputable def LiLiuGoldbachLogDarboux.grid (a b : ℝ) (n i : ℕ) : ℝ

Equations

• LiLiuGoldbachLogDarboux.grid a b n i = a + ↑i * (b - a) / ↑n

def LiLiuGoldbachLogDarboux.cell (a b c d : ℝ) (n : ℕ) (q : Fin n × Fin n) : Set (ℝ × ℝ)

Equations

• LiLiuGoldbachLogDarboux.cell a b c d n q = Set.Ioc (LiLiuGoldbachLogDarboux.grid a b n ↑q.1) (LiLiuGoldbachLogDarboux.grid a b n (↑q.1 + 1)) ×ˢ Set.Ioc (LiLiuGoldbachLogDarboux.grid c d n ↑q.2) (LiLiuGoldbachLogDarboux.grid c d n (↑q.2 + 1))

noncomputable def LiLiuGoldbachLogDarboux.corner (a b c d : ℝ) (n : ℕ) (q : Fin n × Fin n) : ℝ × ℝ

Equations

• LiLiuGoldbachLogDarboux.corner a b c d n q = (LiLiuGoldbachLogDarboux.grid a b n (↑q.1 + 1), LiLiuGoldbachLogDarboux.grid c d n (↑q.2 + 1))

noncomputable def LiLiuGoldbachLogDarboux.oscillation (a b c d : ℝ) (L : NNReal) (n : ℕ) : ℝ

Equations

• LiLiuGoldbachLogDarboux.oscillation a b c d L n = ↑L * (b - a + (d - c)) / ↑n

noncomputable def LiLiuGoldbachLogDarboux.coefficient (a b c d : ℝ) (K : ℝ × ℝ → ℝ) (L : NNReal) (n : ℕ) (q : Fin n × Fin n) : ℝ

Equations

• LiLiuGoldbachLogDarboux.coefficient a b c d K L n q = max 0 (K (LiLiuGoldbachLogDarboux.corner a b c d n q) - LiLiuGoldbachLogDarboux.oscillation a b c d L n)

theorem LiLiuGoldbachLogDarboux.grid_zero (a b : ℝ) (n : ℕ) : grid a b n 0 = a

theorem LiLiuGoldbachLogDarboux.grid_last (a b : ℝ) {n : ℕ} (hn : 0 < n) : grid a b n n = b

theorem LiLiuGoldbachLogDarboux.grid_mono {a b : ℝ} (hab : a ≤ b) (n : ℕ) : Monotone (grid a b n)

theorem LiLiuGoldbachLogDarboux.grid_step (a b : ℝ) (n i : ℕ) : grid a b n (i + 1) - grid a b n i = (b - a) / ↑n

theorem LiLiuGoldbachLogDarboux.grid_strict {a b : ℝ} (hab : a < b) {n : ℕ} (hn : 0 < n) (i : ℕ) : grid a b n i < grid a b n (i + 1)

theorem LiLiuGoldbachLogDarboux.grid_bounds {a b : ℝ} (hab : a ≤ b) {n i : ℕ} (hn : 0 < n) (hi : i ≤ n) : a ≤ grid a b n i ∧ grid a b n i ≤ b

theorem LiLiuGoldbachLogDarboux.cell_subset {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) : cell a b c d n q ⊆ Set.Ioc a b ×ˢ Set.Ioc c d

theorem LiLiuGoldbachLogDarboux.cell_disjoint {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) (n : ℕ) : Set.univ.Pairwise (Function.onFun Disjoint (cell a b c d n))

theorem LiLiuGoldbachLogDarboux.exists_grid_cell {a b x : ℝ} (hab : a < b) {n : ℕ} (hn : 0 < n) (hx : x ∈ Set.Ioc a b) : ∃ (i : Fin n), x ∈ Set.Ioc (grid a b n ↑i) (grid a b n (↑i + 1))

theorem LiLiuGoldbachLogDarboux.cells_union {a b c d : ℝ} (hab : a < b) (hcd : c < d) {n : ℕ} (hn : 0 < n) : ⋃ q ∈ Finset.univ, cell a b c d n q = Set.Ioc a b ×ˢ Set.Ioc c d

theorem LiLiuGoldbachLogDarboux.integral_eq_sum_cells {a b c d : ℝ} (hab : a < b) (hcd : c < d) {n : ℕ} (hn : 0 < n) {f : ℝ × ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f (Set.Ioc a b ×ˢ Set.Ioc c d) MeasureTheory.volume) : ∫ (x : ℝ × ℝ) in Set.Ioc a b ×ˢ Set.Ioc c d, f x = ∑ q : Fin n × Fin n, ∫ (x : ℝ × ℝ) in cell a b c d n q, f x

A generic finite fixed-grid integral decomposition; no prime arithmetic.

theorem LiLiuGoldbachLogDarboux.corner_dist {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) {n : ℕ} (q : Fin n × Fin n) {x : ℝ × ℝ} (hx : x ∈ cell a b c d n q) : dist x (corner a b c d n q) ≤ (b - a + (d - c)) / ↑n

theorem LiLiuGoldbachLogDarboux.coefficient_bounds {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) {K : ℝ × ℝ → ℝ} {L : NNReal} (hK : LipschitzWith L K) (hpos : ∀ x ∈ Set.Ioc a b ×ˢ Set.Ioc c d, 0 ≤ K x) {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) {x : ℝ × ℝ} (hx : x ∈ cell a b c d n q) : 0 ≤ coefficient a b c d K L n q ∧ coefficient a b c d K L n q ≤ K x ∧ K x - 2 * oscillation a b c d L n ≤ coefficient a b c d K L n q

theorem LiLiuGoldbachLogDarboux.weighted_integrable {a b c d : ℝ} (ha : 0 < a) (hc : 0 < c) {K : ℝ × ℝ → ℝ} (hK : Continuous K) : MeasureTheory.IntegrableOn (fun (x : ℝ × ℝ) => K x / (x.1 * x.2)) (Set.Ioc a b ×ˢ Set.Ioc c d) MeasureTheory.volume

Integrability is derived from continuity on the positive closed rectangle.

theorem LiLiuGoldbachLogDarboux.integral_eq_iterated {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) {f : ℝ × ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f (Set.Ioc a b ×ˢ Set.Ioc c d) MeasureTheory.volume) : ∫ (x : ℝ × ℝ) in Set.Ioc a b ×ˢ Set.Ioc c d, f x = ∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, f (u, v)

noncomputable def LiLiuGoldbachLogDarboux.cellMass (a b c d : ℝ) (n : ℕ) (q : Fin n × Fin n) : ℝ

Equations

• LiLiuGoldbachLogDarboux.cellMass a b c d n q = MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (LiLiuGoldbachLogDarboux.grid a b n ↑q.1) (LiLiuGoldbachLogDarboux.grid a b n (↑q.1 + 1)) (LiLiuGoldbachLogDarboux.grid c d n ↑q.2) (LiLiuGoldbachLogDarboux.grid c d n (↑q.2 + 1))

theorem LiLiuGoldbachLogDarboux.cellMass_eq {a b c d : ℝ} (ha : 0 < a) (hab : a < b) (hc : 0 < c) (hcd : c < d) {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) : cellMass a b c d n q = ∫ (x : ℝ × ℝ) in cell a b c d n q, 1 / (x.1 * x.2)

theorem LiLiuGoldbachLogDarboux.darboux_explicit {a b c d : ℝ} (ha : 0 < a) (hab : a < b) (hc : 0 < c) (hcd : c < d) {K : ℝ × ℝ → ℝ} {L : NNReal} (hK : LipschitzWith L K) (hpos : ∀ x ∈ Set.Ioc a b ×ˢ Set.Ioc c d, 0 ≤ K x) {n : ℕ} (hn : 0 < n) : (∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, K (u, v) / (u * v)) - 2 * oscillation a b c d L n * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass a b c d ≤ ∑ q : Fin n × Fin n, coefficient a b c d K L n q * cellMass a b c d n q

Explicit error bound for the concrete nonnegative lower coefficients. The factor two arises from using the upper-right sample minus the oscillation.

theorem LiLiuGoldbachLogDarboux.exists_darboux {a b c d : ℝ} (ha : 0 < a) (hab : a < b) (hc : 0 < c) (hcd : c < d) {K : ℝ × ℝ → ℝ} {L : NNReal} (hK : LipschitzWith L K) (hpos : ∀ x ∈ Set.Ioc a b ×ˢ Set.Ioc c d, 0 ≤ K x) {η : ℝ} (hη : 0 < η) : ∃ (n : ℕ), 0 < n ∧ ∃ (coeff : Fin n × Fin n → ℝ), (∀ (q : Fin n × Fin n), 0 ≤ coeff q) ∧ (∀ (q : Fin n × Fin n), ∀ x ∈ cell a b c d n q, coeff q ≤ K x) ∧ (∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, K (u, v) / (u * v)) - η ≤ ∑ q : Fin n × Fin n, coeff q * cellMass a b c d n q

Finite logarithmic-density Darboux lower approximation on any positive rectangle. The coefficient is a kernel value, not a density-weighted kernel value.