← Mathematical handbook

The standard normal quantile on the open unit interval

theorem Verification.measurableEmbedding_standardNormalCDF : MeasurableEmbedding ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))

noncomputable def Verification.normalQuantile (u : ↑unitInterval) : ℝ

Equations

• Verification.normalQuantile u = Verification.measurableEmbedding_standardNormalCDF.invFun ↑u

theorem Verification.measurable_normalQuantile : Measurable normalQuantile

theorem Verification.normalCDF_mem_Ioo (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x ∈ Set.Ioo 0 1

theorem Verification.normalQuantile_cdfUnit (x : ℝ) : normalQuantile (ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) x) = x

theorem Verification.cdf_normalQuantile {u : ↑unitInterval} (hu : ↑u ∈ Set.Ioo 0 1) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (normalQuantile u) = ↑u

theorem Verification.normalQuantile_strictMonoOn : StrictMonoOn normalQuantile {u : ↑unitInterval | ↑u ∈ Set.Ioo 0 1}