theorem
Verification.conditionalCDF_polynomial
(C : ProbabilityTheory.Copula 2)
(v : ↑unitInterval)
(p : Polynomial ℝ)
(hp : ∀ (u : ↑unitInterval), Polynomial.eval (↑u) p = C.cdf ![u, v])
:
(fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) =>
Polynomial.eval (↑u) (Polynomial.derivative p)
An actual polynomial CDF section identifies the conditional CDF almost everywhere.