Shared estimates for half-open logarithmic grids. The density, cell selection, and boundary cover remain parameters of the consumers, not replacement measures.

theorem MathlibNt.Analysis.LogGridEstimates.reciprocal_variation {c d l e : ℝ} (hl : 0 < l) (hc : l ≤ c) (hcd : c ≤ d) (he : 0 ≤ e) (hdelta : d - c ≤ e * (l * l)) : 0 ≤ 1 / c - 1 / d ∧ 1 / c - 1 / d ≤ e

Reciprocal oscillation paid for by a positive lower gap.

theorem MathlibNt.Analysis.LogGridEstimates.cell_reciprocal_variation {a b da db l e : ℝ} {x : ℝ × ℝ} (hx : x ∈ Set.Ioc a (a + da) ×ˢ Set.Ioc b (b + db)) (hl : 0 < l) (hgap : l ≤ 1 - (a + da) - (b + db)) (he : 0 ≤ e) (hwidth : da + db ≤ e * (l * l)) : 0 ≤ 1 / (1 - (a + da) - (b + db)) - 1 / (1 - x.1 - x.2) ∧ 1 / (1 - (a + da) - (b + db)) - 1 / (1 - x.1 - x.2) ≤ e

The two coordinate widths control the reciprocal gap throughout an Ioc cell.

theorem MathlibNt.Analysis.LogGridEstimates.cells_pairwiseDisjoint (n : ℕ) (a b : ℕ → ℝ) (ha : Monotone a) (hb : Monotone b) : Set.univ.Pairwise (Function.onFun Disjoint fun (q : Fin n × Fin n) => Set.Ioc (a ↑q.1) (a (↑q.1 + 1)) ×ˢ Set.Ioc (b ↑q.2) (b (↑q.2 + 1)))

Product cells inherit exact disjointness, including grid lines.

theorem MathlibNt.Analysis.LogGridEstimates.volume_strip (a b w : ℝ) (f : ℝ → ℝ) (hs : MeasurableSet {x : ℝ × ℝ | x.1 ∈ Set.Icc a b ∧ f x.1 < x.2 ∧ x.2 < f x.1 + w}) (hw : 0 ≤ w) : MeasureTheory.volume {x : ℝ × ℝ | x.1 ∈ Set.Icc a b ∧ f x.1 < x.2 ∧ x.2 < f x.1 + w} = ENNReal.ofReal (w * (b - a))

Exact volume of an open vertical strip of constant width over a closed base. No slope or sign restriction on the moving lower boundary is needed.

theorem MathlibNt.Analysis.LogGridEstimates.weighted_sum_eq_of_mem {α : Type u_1} {ι : Type u_2} (s : Finset ι) (C : ι → Set α) (k : ι → ℝ) (d : α → ℝ) (hd : Set.univ.Pairwise (Function.onFun Disjoint C)) {q : ι} (hq : q ∈ s) {x : α} (hx : x ∈ C q) : ∑ r ∈ s, k r * (C r).indicator d x = k q * d x

Evaluation of a weighted cell sum uses the actual density at the point.

theorem MathlibNt.Analysis.LogGridEstimates.weighted_sum_zero {α : Type u_1} {ι : Type u_2} (s : Finset ι) (C : ι → Set α) (k : ι → ℝ) (d : α → ℝ) {x : α} (hx : x ∉ ⋃ q ∈ s, C q) : ∑ q ∈ s, k q * (C q).indicator d x = 0

The weighted sum has no contribution outside the selected union.

theorem MathlibNt.Analysis.LogGridEstimates.weighted_error {k k' d D e : ℝ} (hd0 : 0 ≤ d) (hd : d ≤ D) (he : 0 ≤ e) (hk : k' - k ≤ e) : k' * d ≤ k * d + e * D

A bounded density transports kernel oscillation without dropping the weight.

theorem MathlibNt.Analysis.LogGridEstimates.integral_sub_le_three_strips (G S A E₀ E₁ E₂ : Set (ℝ × ℝ)) (g f : ℝ × ℝ → ℝ) (e M v₀ v₁ v₂ : ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hf : MeasureTheory.IntegrableOn f S MeasureTheory.volume) (hS : MeasurableSet S) (hA : MeasurableSet A) (hAv : MeasureTheory.volume A = 1) (hE₀ : MeasurableSet E₀) (hE₁ : MeasurableSet E₁) (hE₂ : MeasurableSet E₂) (hV₀ : MeasureTheory.volume E₀ = ENNReal.ofReal v₀) (hV₁ : MeasureTheory.volume E₁ = ENNReal.ofReal v₁) (hV₂ : MeasureTheory.volume E₂ = ENNReal.ofReal v₂) (hv₀ : 0 ≤ v₀) (hv₁ : 0 ≤ v₁) (hv₂ : 0 ≤ v₂) (he : 0 ≤ e) (hM : 0 ≤ M) (hf0 : ∀ x ∈ S, 0 ≤ f x) (hzero : ∀ x ∉ G, g x = 0) (hinside : G ∩ S ⊆ A) (hlocal : ∀ x ∈ G ∩ S, g x ≤ f x + e) (hcover : G \ S ⊆ E₀ ∪ E₁ ∪ E₂) (hcap : ∀ x ∈ G \ S, g x ≤ M) : (∫ (x : ℝ × ℝ), g x) - ∫ (x : ℝ × ℝ) in S, f x ≤ e + (v₀ + v₁ + v₂) * M

Three measurable strips may overlap. This specializes the accepted excess-cover integral theorem, keeping their individual volumes and the actual weighted functions.