← Mathematical handbook

A Lebesgue density for the actual Gaussian copula

noncomputable def Verification.gaussianCopulaDensity (r : ℝ) (u : Fin 2 → ↑unitInterval) : ℝ

Equations

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

theorem Verification.gaussianCopulaDensity_nonneg (r : ℝ) (u : Fin 2 → ↑unitInterval) : 0 ≤ gaussianCopulaDensity r u

theorem Verification.measurable_gaussianCopulaDensity (r : ℝ) : Measurable (gaussianCopulaDensity r)

theorem Verification.gaussianCopulaDensity_normal (r x y : ℝ) : gaussianCopulaDensity r ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) x, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) y] = ProbabilityTheory.gaussianPDFReal (r * x) (1 - r ^ 2).toNNReal y / ProbabilityTheory.gaussianPDFReal 0 1 y

theorem Verification.gaussian_map_withDensity_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) {F : α → β} (hF : Measurable F) {g : β → ENNReal} (hg : Measurable g) : MeasureTheory.Measure.map F (μ.withDensity fun (x : α) => g (F x)) = (MeasureTheory.Measure.map F μ).withDensity g

theorem Verification.gaussianBivariate_density {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : (gaussianBivariate r ⋯).toMeasure = MeasureTheory.volume.withDensity fun (u : Fin 2 → ↑unitInterval) => ENNReal.ofReal (gaussianCopulaDensity r u)