← Mathematical handbook

theorem Verification.denseRange_cdfUnit_of_continuous (μ : MeasureTheory.Measure ℝ) (hc : Continuous ↑(ProbabilityTheory.cdf μ)) : DenseRange (ProbabilityTheory.cdfUnit μ)

theorem Verification.sklar_lowerOrthant_of_common_marginals {d : ℕ} (μ ν : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (C D : ProbabilityTheory.Copula d) (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal μ i))) (hm : ∀ (i : Fin d), ProbabilityTheory.Copula.marginal μ i = ProbabilityTheory.Copula.marginal ν i) (hC : ProbabilityTheory.Copula.IsSklarCopula μ C) (hD : ProbabilityTheory.Copula.IsSklarCopula ν D) (ho : ∀ (x : Fin d → ℝ), (↑μ).real (Set.Iic x) ≤ (↑ν).real (Set.Iic x)) : C.LowerOrthantLE D