Identifying copula densities from their lower-orthant integrals #
theorem
ProbabilityTheory.Copula.HasMTP2Density.absolutelyContinuous
{d : ℕ}
{C : Copula d}
(h : C.HasMTP2Density)
:
theorem
ProbabilityTheory.Copula.toMeasure_eq_withDensity_of_cdf_integral
{d : ℕ}
(C : Copula d)
{f : (Fin d → ↑unitInterval) → ℝ}
(hf : MeasureTheory.Integrable f MeasureTheory.volume)
(hn : ∀ (x : Fin d → ↑unitInterval), 0 ≤ f x)
(hF : ∀ (u : Fin d → ↑unitInterval), ∫ (x : Fin d → ↑unitInterval) in Set.Iic u, f x = C.cdf u)
:
C.toMeasure = MeasureTheory.volume.withDensity fun (x : Fin d → ↑unitInterval) => ENNReal.ofReal (f x)
An integrable nonnegative candidate is the copula's density when its lower-orthant integrals agree with the CDF.
theorem
ProbabilityTheory.Copula.integral_cube_Iic_mul
(f g : ↑unitInterval → ℝ)
(u v : ↑unitInterval)
: