Identifying conditional CDFs by their lower-interval integrals #
theorem
ProbabilityTheory.Copula.conditionalCDF_ae_eq_of_integral
(C : Copula 2)
(v : ↑unitInterval)
{f : ↑unitInterval → ℝ}
(hf : MeasureTheory.Integrable f MeasureTheory.volume)
(hn : ∀ (t : ↑unitInterval), 0 ≤ f t)
(hF : ∀ (u : ↑unitInterval), ∫ (t : ↑unitInterval) in Set.Iic u, f t = C.cdf ![u, v])
:
(fun (t : ↑unitInterval) => C.conditionalCDF t v) =ᵐ[MeasureTheory.volume] f
An integrable nonnegative candidate is a version of the conditional CDF at a fixed threshold if its indefinite integrals recover the copula CDF. The exceptional null set is allowed to depend on the threshold.