Measurable parametric Stieltjes functions

We provide tools to build a measurable function α → StieltjesFunction with limits 0 at -∞ and 1 at +∞ for all a : α from a measurable function f : α → ℚ → ℝ. These measurable parametric Stieltjes functions are cumulative distribution functions (CDF) of transition kernels. The reason for going through ℚ instead of defining directly a Stieltjes function is that since ℚ is countable, building a measurable function is easier and we can obtain properties of the form ∀ᵐ (a : α) ∂μ, ∀ (q : ℚ), ... (for some measure μ on α) by proving the weaker ∀ (q : ℚ), ∀ᵐ (a : α) ∂μ, ....

This construction will be possible if f a : ℚ → ℝ satisfies a package of properties for all a: monotonicity, limits at +-∞ and a continuity property. We define IsRatStieltjesPoint f a to state that this is the case at a and define the property IsMeasurableRatCDF f that f is measurable and IsRatStieltjesPoint f a for all a. The function α → StieltjesFunction obtained by extending f by continuity from the right is then called IsMeasurableRatCDF.stieltjesFunction.

In applications, we will often only have IsRatStieltjesPoint f a almost surely with respect to some measure. In order to turn that almost everywhere property into an everywhere property we define toRatCDF (f : α → ℚ → ℝ) := fun a q ↦ if IsRatStieltjesPoint f a then f a q else defaultRatCDF q, which satisfies the property IsMeasurableRatCDF (toRatCDF f).

Finally, we define stieltjesOfMeasurableRat, composition of toRatCDF and IsMeasurableRatCDF.stieltjesFunction.

Main definitions

• stieltjesOfMeasurableRat: turn a measurable function f : α → ℚ → ℝ into a measurable function α → StieltjesFunction.

theorem StieltjesFunction.measurable_measure {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → StieltjesFunction} (hf : ∀ (q : ℝ), Measurable fun (a : α) => ↑(f a) q) (hf_bot : ∀ (a : α), Filter.Tendsto (↑(f a)) Filter.atBot (nhds 0)) (hf_top : ∀ (a : α), Filter.Tendsto (↑(f a)) Filter.atTop (nhds 1)) : Measurable fun (a : α) => (f a).measure

A measurable function α → StieltjesFunction with limits 0 at -∞ and 1 at +∞ gives a measurable function α → Measure ℝ by taking StieltjesFunction.measure at each point.

structure ProbabilityTheory.IsRatStieltjesPoint {α : Type u_1} (f : α → ℚ → ℝ) (a : α) : Prop

a : α is a Stieltjes point for f : α → ℚ → ℝ if f a is monotone with limit 0 at -∞ and 1 at +∞ and satisfies a continuity property.

• mono : Monotone (f a)
• tendsto_atTop_one : Filter.Tendsto (f a) Filter.atTop (nhds 1)
• tendsto_atBot_zero : Filter.Tendsto (f a) Filter.atBot (nhds 0)
• iInf_rat_gt_eq (t : ℚ) : ⨅ (r : ↑(Set.Ioi t)), f a ↑r = f a t

theorem ProbabilityTheory.isRatStieltjesPoint_unit_prod_iff {α : Type u_1} (f : α → ℚ → ℝ) (a : α) : IsRatStieltjesPoint (fun (p : Unit × α) => f p.2) ((), a) ↔ IsRatStieltjesPoint f a

theorem ProbabilityTheory.measurableSet_isRatStieltjesPoint {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) : MeasurableSet {a : α | IsRatStieltjesPoint f a}

theorem ProbabilityTheory.IsRatStieltjesPoint.ite {α : Type u_1} {f g : α → ℚ → ℝ} {a : α} (p : α → Prop) [DecidablePred p] (hf : p a → IsRatStieltjesPoint f a) (hg : ¬p a → IsRatStieltjesPoint g a) : IsRatStieltjesPoint (fun (a : α) => if p a then f a else g a) a

structure ProbabilityTheory.IsMeasurableRatCDF {α : Type u_1} [MeasurableSpace α] (f : α → ℚ → ℝ) : Prop

A function f : α → ℚ → ℝ is a (kernel) rational cumulative distribution function if it is measurable in the first argument and if f a satisfies a list of properties for all a : α: monotonicity between 0 at -∞ and 1 at +∞ and a form of continuity.

A function with these properties can be extended to a measurable function α → StieltjesFunction. See ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction.

• isRatStieltjesPoint (a : α) : IsRatStieltjesPoint f a
• measurable : Measurable f

theorem ProbabilityTheory.IsMeasurableRatCDF.nonneg {α : Type u_1} [MeasurableSpace α] {f : α → ℚ → ℝ} (hf : IsMeasurableRatCDF f) (a : α) (q : ℚ) : 0 ≤ f a q

theorem ProbabilityTheory.IsMeasurableRatCDF.le_one {α : Type u_1} [MeasurableSpace α] {f : α → ℚ → ℝ} (hf : IsMeasurableRatCDF f) (a : α) (q : ℚ) : f a q ≤ 1

theorem ProbabilityTheory.IsMeasurableRatCDF.tendsto_atTop_one {α : Type u_1} [MeasurableSpace α] {f : α → ℚ → ℝ} (hf : IsMeasurableRatCDF f) (a : α) : Filter.Tendsto (f a) Filter.atTop (nhds 1)

theorem ProbabilityTheory.IsMeasurableRatCDF.tendsto_atBot_zero {α : Type u_1} [MeasurableSpace α] {f : α → ℚ → ℝ} (hf : IsMeasurableRatCDF f) (a : α) : Filter.Tendsto (f a) Filter.atBot (nhds 0)

theorem ProbabilityTheory.IsMeasurableRatCDF.iInf_rat_gt_eq {α : Type u_1} [MeasurableSpace α] {f : α → ℚ → ℝ} (hf : IsMeasurableRatCDF f) (a : α) (q : ℚ) : ⨅ (r : ↑(Set.Ioi q)), f a ↑r = f a q

def ProbabilityTheory.defaultRatCDF (q : ℚ) : ℝ

A function with the property IsMeasurableRatCDF. Used in a piecewise construction to convert a function which only satisfies the properties defining IsMeasurableRatCDF on some set into a true IsMeasurableRatCDF.

Equations

• ProbabilityTheory.defaultRatCDF q = if q < 0 then 0 else 1

theorem ProbabilityTheory.monotone_defaultRatCDF : Monotone defaultRatCDF

theorem ProbabilityTheory.defaultRatCDF_nonneg (q : ℚ) : 0 ≤ defaultRatCDF q

theorem ProbabilityTheory.defaultRatCDF_le_one (q : ℚ) : defaultRatCDF q ≤ 1

theorem ProbabilityTheory.tendsto_defaultRatCDF_atTop : Filter.Tendsto defaultRatCDF Filter.atTop (nhds 1)

theorem ProbabilityTheory.tendsto_defaultRatCDF_atBot : Filter.Tendsto defaultRatCDF Filter.atBot (nhds 0)

theorem ProbabilityTheory.iInf_rat_gt_defaultRatCDF (t : ℚ) : ⨅ (r : ↑(Set.Ioi t)), defaultRatCDF ↑r = defaultRatCDF t

theorem ProbabilityTheory.isRatStieltjesPoint_defaultRatCDF {α : Type u_1} (a : α) : IsRatStieltjesPoint (fun (x : α) => defaultRatCDF) a

theorem ProbabilityTheory.IsMeasurableRatCDF_defaultRatCDF (α : Type u_2) [MeasurableSpace α] : IsMeasurableRatCDF fun (x : α) (q : ℚ) => defaultRatCDF q

noncomputable def ProbabilityTheory.toRatCDF {α : Type u_1} (f : α → ℚ → ℝ) : α → ℚ → ℝ

Turn a function f : α → ℚ → ℝ into another with the property IsRatStieltjesPoint f a everywhere. At a that does not satisfy that property, f a is replaced by an arbitrary suitable function. Mainly useful when f satisfies the property IsRatStieltjesPoint f a almost everywhere with respect to some measure.

Equations

• ProbabilityTheory.toRatCDF f a = if ProbabilityTheory.IsRatStieltjesPoint f a then f a else ProbabilityTheory.defaultRatCDF

theorem ProbabilityTheory.toRatCDF_of_isRatStieltjesPoint {α : Type u_1} {f : α → ℚ → ℝ} {a : α} (h : IsRatStieltjesPoint f a) (q : ℚ) : toRatCDF f a q = f a q

theorem ProbabilityTheory.toRatCDF_unit_prod {α : Type u_1} {f : α → ℚ → ℝ} (a : α) : toRatCDF (fun (p : Unit × α) => f p.2) ((), a) = toRatCDF f a

theorem ProbabilityTheory.measurable_toRatCDF {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) : Measurable (toRatCDF f)

theorem ProbabilityTheory.isMeasurableRatCDF_toRatCDF {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) : IsMeasurableRatCDF (toRatCDF f)

@[irreducible]

noncomputable def ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux {α : Type u_2} (f : α → ℚ → ℝ) : α → ℝ → ℝ

Auxiliary definition for IsMeasurableRatCDF.stieltjesFunction: turn f : α → ℚ → ℝ into a function α → ℝ → ℝ by assigning to f a x the infimum of f a q over q : ℚ with x < q.

Equations

• ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a x = ⨅ (q : { q' : ℚ // x < ↑q' }), f a ↑q

theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def {α : Type u_2} (f : α → ℚ → ℝ) (a : α) (x : ℝ) : stieltjesFunctionAux f a x = ⨅ (q : { q' : ℚ // x < ↑q' }), f a ↑q

theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def' {α : Type u_1} (f : α → ℚ → ℝ) (a : α) : stieltjesFunctionAux f a = fun (t : ℝ) => ⨅ (r : { r' : ℚ // t < ↑r' }), f a ↑r

theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod {α : Type u_1} {f : α → ℚ → ℝ} (a : α) : stieltjesFunctionAux (fun (p : Unit × α) => f p.2) ((), a) = stieltjesFunctionAux f a

theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_eq {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) (r : ℚ) : stieltjesFunctionAux f a ↑r = f a r

theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_nonneg {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) (r : ℝ) : 0 ≤ stieltjesFunctionAux f a r

theorem ProbabilityTheory.IsMeasurableRatCDF.monotone_stieltjesFunctionAux {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) : Monotone (stieltjesFunctionAux f a)

theorem ProbabilityTheory.IsMeasurableRatCDF.continuousWithinAt_stieltjesFunctionAux_Ici {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) (x : ℝ) : ContinuousWithinAt (stieltjesFunctionAux f a) (Set.Ici x) x

noncomputable def ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) : StieltjesFunction

Extend a function f : α → ℚ → ℝ with property IsMeasurableRatCDF from ℚ to ℝ, to a function α → StieltjesFunction.

Equations

• hf.stieltjesFunction a = { toFun := ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a, mono' := ⋯, right_continuous' := ⋯ }

theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) (r : ℚ) : ↑(hf.stieltjesFunction a) ↑r = f a r

theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_nonneg {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) (r : ℝ) : 0 ≤ ↑(hf.stieltjesFunction a) r

theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_le_one {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) (x : ℝ) : ↑(hf.stieltjesFunction a) x ≤ 1

theorem ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) : Filter.Tendsto (↑(hf.stieltjesFunction a)) Filter.atBot (nhds 0)

theorem ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) : Filter.Tendsto (↑(hf.stieltjesFunction a)) Filter.atTop (nhds 1)

theorem ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (x : ℝ) : Measurable fun (a : α) => ↑(hf.stieltjesFunction a) x

theorem ProbabilityTheory.IsMeasurableRatCDF.stronglyMeasurable_stieltjesFunction {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (x : ℝ) : MeasureTheory.StronglyMeasurable fun (a : α) => ↑(hf.stieltjesFunction a) x

theorem ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_Iic {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) (x : ℝ) : (hf.stieltjesFunction a).measure (Set.Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x)

theorem ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) : (hf.stieltjesFunction a).measure Set.univ = 1

instance ProbabilityTheory.IsMeasurableRatCDF.instIsProbabilityMeasure_stieltjesFunction {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) (a : α) : MeasureTheory.IsProbabilityMeasure (hf.stieltjesFunction a).measure

theorem ProbabilityTheory.IsMeasurableRatCDF.measurable_measure_stieltjesFunction {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : IsMeasurableRatCDF f) : Measurable fun (a : α) => (hf.stieltjesFunction a).measure

noncomputable def ProbabilityTheory.stieltjesOfMeasurableRat {α : Type u_1} [MeasurableSpace α] (f : α → ℚ → ℝ) (hf : Measurable f) : α → StieltjesFunction

Turn a measurable function f : α → ℚ → ℝ into a measurable function α → StieltjesFunction. Composition of toRatCDF and IsMeasurableRatCDF.stieltjesFunction.

Equations

• ProbabilityTheory.stieltjesOfMeasurableRat f hf = ⋯.stieltjesFunction

theorem ProbabilityTheory.stieltjesOfMeasurableRat_eq {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (a : α) (r : ℚ) : ↑(stieltjesOfMeasurableRat f hf a) ↑r = toRatCDF f a r

theorem ProbabilityTheory.stieltjesOfMeasurableRat_unit_prod {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (a : α) : stieltjesOfMeasurableRat (fun (p : Unit × α) => f p.2) ⋯ ((), a) = stieltjesOfMeasurableRat f hf a

theorem ProbabilityTheory.stieltjesOfMeasurableRat_nonneg {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (a : α) (r : ℝ) : 0 ≤ ↑(stieltjesOfMeasurableRat f hf a) r

theorem ProbabilityTheory.stieltjesOfMeasurableRat_le_one {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (a : α) (x : ℝ) : ↑(stieltjesOfMeasurableRat f hf a) x ≤ 1

theorem ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atBot {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (a : α) : Filter.Tendsto (↑(stieltjesOfMeasurableRat f hf a)) Filter.atBot (nhds 0)

theorem ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atTop {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (a : α) : Filter.Tendsto (↑(stieltjesOfMeasurableRat f hf a)) Filter.atTop (nhds 1)

theorem ProbabilityTheory.measurable_stieltjesOfMeasurableRat {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (x : ℝ) : Measurable fun (a : α) => ↑(stieltjesOfMeasurableRat f hf a) x

theorem ProbabilityTheory.stronglyMeasurable_stieltjesOfMeasurableRat {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (x : ℝ) : MeasureTheory.StronglyMeasurable fun (a : α) => ↑(stieltjesOfMeasurableRat f hf a) x

theorem ProbabilityTheory.measure_stieltjesOfMeasurableRat_Iic {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (a : α) (x : ℝ) : (stieltjesOfMeasurableRat f hf a).measure (Set.Iic x) = ENNReal.ofReal (↑(stieltjesOfMeasurableRat f hf a) x)

theorem ProbabilityTheory.measure_stieltjesOfMeasurableRat_univ {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (a : α) : (stieltjesOfMeasurableRat f hf a).measure Set.univ = 1

instance ProbabilityTheory.instIsProbabilityMeasure_stieltjesOfMeasurableRat {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) (a : α) : MeasureTheory.IsProbabilityMeasure (stieltjesOfMeasurableRat f hf a).measure

theorem ProbabilityTheory.measurable_measure_stieltjesOfMeasurableRat {α : Type u_1} {f : α → ℚ → ℝ} [MeasurableSpace α] (hf : Measurable f) : Measurable fun (a : α) => (stieltjesOfMeasurableRat f hf a).measure