← Mathematical handbook

noncomputable def Verification.continuousCDFQuantile (μ : MeasureTheory.Measure ℝ) (hc : Continuous ↑(ProbabilityTheory.cdf μ)) (hs : StrictMono ↑(ProbabilityTheory.cdf μ)) (u : ↑unitInterval) : ℝ

Equations

• Verification.continuousCDFQuantile μ hc hs u = ⋯.invFun ↑u

theorem Verification.strictCDF_mem_Ioo (μ : MeasureTheory.Measure ℝ) (hs : StrictMono ↑(ProbabilityTheory.cdf μ)) (x : ℝ) : ↑(ProbabilityTheory.cdf μ) x ∈ Set.Ioo 0 1

theorem Verification.continuousCDFQuantile_cdfUnit (μ : MeasureTheory.Measure ℝ) (hc : Continuous ↑(ProbabilityTheory.cdf μ)) (hs : StrictMono ↑(ProbabilityTheory.cdf μ)) (x : ℝ) : continuousCDFQuantile μ hc hs (ProbabilityTheory.cdfUnit μ x) = x

theorem Verification.cdf_continuousCDFQuantile (μ : MeasureTheory.Measure ℝ) (hc : Continuous ↑(ProbabilityTheory.cdf μ)) (hs : StrictMono ↑(ProbabilityTheory.cdf μ)) {u : ↑unitInterval} (hu : ↑u ∈ Set.Ioo 0 1) : ↑(ProbabilityTheory.cdf μ) (continuousCDFQuantile μ hc hs u) = ↑u

theorem Verification.continuousCDFQuantile_tendsto_zero (μ : MeasureTheory.Measure ℝ) (hc : Continuous ↑(ProbabilityTheory.cdf μ)) (hs : StrictMono ↑(ProbabilityTheory.cdf μ)) : Filter.Tendsto (continuousCDFQuantile μ hc hs) (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot