← Mathematical handbook

Gaussian conditional CDF on copula coordinates

noncomputable def Verification.gaussianQuantileConditional (r : ℝ) (v u : ↑unitInterval) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.measurable_gaussianQuantileConditional (r : ℝ) (v : ↑unitInterval) : Measurable (gaussianQuantileConditional r v)

theorem Verification.gaussianBivariate_conditionalCDF_quantile {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) {v : ↑unitInterval} (hv : ↑v ∈ Set.Ioo 0 1) : (fun (u : ↑unitInterval) => (gaussianBivariate r ⋯).conditionalCDF u v) =ᵐ[MeasureTheory.volume] gaussianQuantileConditional r v

theorem Verification.gaussianQuantileConditional_antitoneOn {r : ℝ} (hr : 0 ≤ r) (v : ↑unitInterval) : AntitoneOn (gaussianQuantileConditional r v) {u : ↑unitInterval | ↑u ∈ Set.Ioo 0 1}

theorem Verification.gaussianQuantileConditional_monotoneOn {r : ℝ} (hr : r ≤ 0) (v : ↑unitInterval) : MonotoneOn (gaussianQuantileConditional r v) {u : ↑unitInterval | ↑u ∈ Set.Ioo 0 1}