Finite-window operations on Stieltjes measures

Agreement, translation, and capping of Stieltjes functions on an initial interval give the corresponding identities and inequalities for their associated measures.

theorem BGW.Probability.stieltjes_restrict_Ioc_congr {F G : StieltjesFunction ℝ} {T : ℝ} (hT : 0 ≤ T) (he : ∀ x ∈ Set.Icc 0 T, ↑F x = ↑G x) : F.measure.restrict (Set.Ioc 0 T) = G.measure.restrict (Set.Ioc 0 T)

Agreement of Stieltjes functions on a closed window gives agreement of their source measures.

theorem BGW.Probability.stieltjes_min_restrict_le {F G : StieltjesFunction ℝ} {T c : ℝ} (hT : 0 ≤ T) (he : ∀ x ∈ Set.Icc 0 T, ↑G x = min (↑F x) c) : G.measure.restrict (Set.Ioc 0 T) ≤ F.measure.restrict (Set.Ioc 0 T)

Capping a Stieltjes function decreases its restricted source measure.

theorem BGW.Probability.stieltjes_min_initial_cdf {F G : StieltjesFunction ℝ} {T c : ℝ} (hT : 0 ≤ T) (hc : c ≤ ↑F T) (he : ∀ x ∈ Set.Icc 0 T, ↑G x = min (↑F x) c) (a : ℝ) : (G.measure.restrict (Set.Ioc 0 T)) (Set.Iic a) = min ((F.measure.restrict (Set.Ioc 0 T)) (Set.Iic a)) ((F.measure.restrict (Set.Ioc 0 T)) Set.univ - ENNReal.ofReal (↑F T - c))

Capping a Stieltjes function caps its finite-window cumulative masses, including atoms.

theorem BGW.Probability.stieltjes_min_total {F G : StieltjesFunction ℝ} {T c : ℝ} (hT : 0 ≤ T) (hc : c ≤ ↑F T) (he : ∀ x ∈ Set.Icc 0 T, ↑G x = min (↑F x) c) : (G.measure.restrict (Set.Ioc 0 T)) Set.univ = (F.measure.restrict (Set.Ioc 0 T)) Set.univ - ENNReal.ofReal (↑F T - c)

Capping a Stieltjes function gives the prescribed surviving total mass on a finite window.

theorem BGW.Probability.stieltjes_translate_window {F G : StieltjesFunction ℝ} {t r C : ℝ} (hr : 0 ≤ r) (he : ∀ x ∈ Set.Icc 0 r, ↑G (t + x) = C + ↑F x) : MeasureTheory.Measure.map (fun (x : ℝ) => t + x) (F.measure.restrict (Set.Ioc 0 r)) = G.measure.restrict (Set.Ioc t (t + r))

Translation of a Stieltjes function on a finite window translates its restricted measure.