Theorems · Definition · probability
ProbabilityTheory.stieltjesOfMeasurableRat
{α : Type u_1} → [inst : MeasurableSpace α] → (f : α → ℚ → ℝ) → Measurable f → α → StieltjesFunction ℝTurn a measurable function f : α → ℚ → ℝ into a measurable function α → StieltjesFunction ℝ.
Composition of toRatCDF and IsMeasurableRatCDF.stieltjesFunction.
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- Measurablestatement and proof · cited by 1,499
- StieltjesFunctionstatement · cited by 85
- ProbabilityTheory.isMeasurableRatCDF_toRatCDFproof · cited by 11
- ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionproof · cited by 11
Cited by24
Results whose statement or proof uses this declaration.
- ProbabilityTheory.condCDFproof · cited by 20
- ProbabilityTheory.stieltjesOfMeasurableRat_nonnegstatement · cited by 4
- ProbabilityTheory.measurable_stieltjesOfMeasurableRatstatement · cited by 4
- ProbabilityTheory.stieltjesOfMeasurableRat_ae_eqstatement · cited by 3
- ProbabilityTheory.integrable_stieltjesOfMeasurableRatstatement and proof · cited by 2
- ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atBotstatement · cited by 2
- ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atTopstatement · cited by 2
- ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRatstatement and proof · cited by 2
- ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prodstatement and proof · cited by 2
- ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRatstatement · cited by 2
- ProbabilityTheory.setIntegral_stieltjesOfMeasurableRatstatement and proof · cited by 2
- ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_ratstatement · cited by 1