Conditional kernels and xi for independence and functional dependence #
theorem
ProbabilityTheory.Copula.conditionalKernel_of_function
(C : Copula 2)
{f : ↑unitInterval → ↑unitInterval}
(hf : Measurable f)
(h : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = f (x 0))
:
⇑C.conditionalKernel =ᵐ[MeasureTheory.volume] ⇑(Kernel.deterministic f hf)
Functional dependence identifies the conditional kernel almost everywhere.
@[simp]
theorem
ProbabilityTheory.Copula.chatterjeeXi_eq_one_of_function
(C : Copula 2)
{f : ↑unitInterval → ↑unitInterval}
(hf : Measurable f)
(h : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = f (x 0))
:
Xi is one whenever the second coordinate is a measurable function of the first.
@[simp]