← Mathematical handbook

theorem Verification.cdf_map_neg_of_atomless (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] (x : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (z : ℝ) => -z) μ)) (-x) = 1 - ↑(ProbabilityTheory.cdf μ) x

theorem Verification.ofContinuousMarginals_countermonotonic_of_ae_neg (μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)) (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal μ i))) [MeasureTheory.NullSingletonClass (ProbabilityTheory.Copula.marginal μ 0)] (he : ∀ᵐ (x : Fin 2 → ℝ) ∂↑μ, x 1 = -x 0) : ProbabilityTheory.Copula.ofContinuousMarginals μ hc = ProbabilityTheory.Copula.countermonotonic

theorem Verification.gaussian_negative_one_ae_neg : ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation (-1)), x.ofLp 1 = -x.ofLp 0

theorem Verification.gaussianScaleMixture_negative_one (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation (-1)) ⋯ ⋯ μ s hs hp = ProbabilityTheory.Copula.countermonotonic

theorem Verification.studentBivariate_negative_one (ν : ℝ) (hν : 0 < ν) : studentBivariate (-1) ⋯ ν hν = ProbabilityTheory.Copula.countermonotonic