Weighted integral comparison on initial segments

Let μ be a measure on the real line and let φ ≤ 1 on (a, ∞). If the weighted integral of φ over (a, ∞) is at most the weight of (a, ρ], the same comparison holds after intersecting both domains with any initial segment of (a, ∞).

TauCeti.setLIntegral_indicator_mul_le_setLIntegral_indicator_inter_Iic supplies this comparison without measurability assumptions on the weight, density, or initial segment. Applied along each ray, it compares a radial density with the indicator of a ball on sets star-shaped about the origin.

References

The comparison argument comes from the proof of Bombieri–Gubler, Heights in Diophantine Geometry (2006), Lemma C.3.7. It is adapted from the Apache-2.0 formalization of Vaaler's theorem in rwst/Subspace-Theorems (files ArithmeticHeights/GaussMeasure.lean and ArithmeticHeights/SliceBound.lean), by Ralf Stephan.

theorem TauCeti.setLIntegral_indicator_mul_le_setLIntegral_indicator_inter_Iic {μ : MeasureTheory.Measure ℝ} {a ρ : ℝ} {w φ : ℝ → ENNReal} {R : Set ℝ} (hφ : ∀ r ∈ Set.Ioi a, φ r ≤ 1) (hmass : ∫⁻ (r : ℝ) in Set.Ioi a, w r * φ r ∂μ ≤ ∫⁻ (r : ℝ) in Set.Ioi a, (Set.Iic ρ).indicator w r ∂μ) (hR : ∀ ⦃r s : ℝ⦄, a < s → s ≤ r → r ∈ R → s ∈ R) : ∫⁻ (r : ℝ) in Set.Ioi a, R.indicator (fun (r : ℝ) => w r * φ r) r ∂μ ≤ ∫⁻ (r : ℝ) in Set.Ioi a, (R ∩ Set.Iic ρ).indicator w r ∂μ

Let R be an initial segment of (a, ∞) and let φ ≤ 1 there. If the integral of φ against a weight w is at most the weight of (a, ρ], then its integral over R is at most the weight of R ∩ (a, ρ]. The measure is arbitrary, and no measurability assumptions on w, φ, or R are needed.