← Mathematical handbook

noncomputable def Verification.gaussianScaleMixtureJointDensity (r : ℝ) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (p : ℝ × ℝ) : ENNReal

Equations

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

theorem Verification.measurable_gaussianScaleMixtureJointDensity (r : ℝ) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) : Measurable (gaussianScaleMixtureJointDensity r μ s)

theorem Verification.gaussianScaleMixtureLaw_joint_withDensity {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (bivariateCorrelation r) μ s) = MeasureTheory.volume.withDensity (gaussianScaleMixtureJointDensity r μ s)

theorem Verification.gaussianScaleMixtureJointDensity_pos {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (p : ℝ × ℝ) : 0 < gaussianScaleMixtureJointDensity r μ s p

theorem Verification.gaussianScaleMixtureLaw_joint_equivalent_volume {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (bivariateCorrelation r) μ s)).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.volume.AbsolutelyContinuous (MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (bivariateCorrelation r) μ s))