Documentation

Papers.AnsariRockel2024.EllipticalDensity

← Mathematical handbook

theorem Papers.AnsariRockel2024.student_marginal_withDensity (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) :

ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) i = MeasureTheory.volume.withDensity (Verification.normalScaleMixtureDensity (ProbabilityTheory.gammaProbability (ν / 2) (ν / 2) ⋯ ⋯) fun (t : ℝ) => (√t)⁻¹)

theorem Papers.AnsariRockel2024.student_marginal_equivalent_volume (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) :

(ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) i).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.volume.AbsolutelyContinuous (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) i)

theorem Papers.AnsariRockel2024.laplace_marginal_withDensity (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (i : Fin 2) :

ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.gaussianScaleMixtureLaw (Verification.bivariateCorrelation r) (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt) i = MeasureTheory.volume.withDensity (Verification.normalScaleMixtureDensity (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt)

theorem Papers.AnsariRockel2024.student_marginal_standard_density (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) :

ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) i = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (Real.Gamma ((ν + 1) / 2) / (√(ν * Real.pi) * Real.Gamma (ν / 2)) * (1 + x ^ 2 / ν) ^ (-((ν + 1) / 2)))

theorem Papers.AnsariRockel2024.student_joint_withDensity (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) :

MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) = MeasureTheory.volume.withDensity (Verification.gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability (ν / 2) (ν / 2) ⋯ ⋯) fun (t : ℝ) => (√t)⁻¹)

theorem Papers.AnsariRockel2024.student_joint_equivalent_volume (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) :

(MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν)).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.volume.AbsolutelyContinuous (MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν))

theorem Papers.AnsariRockel2024.laplace_joint_withDensity (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) :

MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (Verification.bivariateCorrelation r) (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt) = MeasureTheory.volume.withDensity (Verification.gaussianScaleMixtureJointDensity r (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt)

theorem Papers.AnsariRockel2024.student_joint_standard_density (r : ℝ) (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) :

MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ENNReal.ofReal ((2 * Real.pi * √(1 - r ^ 2))⁻¹ * (1 + (p.1 ^ 2 - 2 * r * p.1 * p.2 + p.2 ^ 2) / (ν * (1 - r ^ 2))) ^ (-((ν + 2) / 2)))

theorem Papers.AnsariRockel2024.student_absolutelyContinuous_iff (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) :

(Verification.studentBivariate r hr ν hν).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ r ∈ Set.Ioo (-1) 1

theorem Papers.AnsariRockel2024.laplace_absolutelyContinuous_iff (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) :

(Verification.laplaceBivariate r hr).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ r ∈ Set.Ioo (-1) 1

theorem Papers.AnsariRockel2024.student_joint_printed_density_counterexample :

Verification.studentPrintedJointPDF 0 2 (0, 0) = 1 ∧ Verification.studentJointPDF 0 2 (0, 0) = (2 * Real.pi)⁻¹

theorem Papers.AnsariRockel2024.student_joint_printed_formula_false :

¬∀ r ∈ Set.Ioo (-1) 1, ∀ (ν : ℝ), 0 < ν → ∀ (p : ℝ × ℝ), Verification.studentJointPDF r ν p = Verification.studentPrintedJointPDF r ν p