← Mathematical handbook

Continuous conditional-law costs for xi and the correlation ratio

theorem Verification.integral_unit_cdf_sq (μ : MeasureTheory.ProbabilityMeasure ↑unitInterval) : ∫ (t : ↑unitInterval), (↑μ).real (Set.Iic t) ^ 2 = 1 - ∫ (p : ↑unitInterval × ↑unitInterval), max ↑p.1 ↑p.2 ∂↑(μ.prod μ)

Squared CDF integral as a continuous cost of two independent samples.

noncomputable def Verification.lawXiCost (μ : MeasureTheory.ProbabilityMeasure ↑unitInterval) : ℝ

Equations

• Verification.lawXiCost μ = 6 * (1 - ∫ (p : ↑unitInterval × ↑unitInterval), max ↑p.1 ↑p.2 ∂↑(μ.prod μ)) - 2

noncomputable def Verification.lawEtaCost (μ : MeasureTheory.ProbabilityMeasure ↑unitInterval) : ℝ

Equations

• Verification.lawEtaCost μ = 12 * (∫ (x : ↑unitInterval), ↑x ∂↑μ - 1 / 2) ^ 2

theorem Verification.continuous_lawXiCost : Continuous lawXiCost

theorem Verification.continuous_lawEtaCost : Continuous lawEtaCost

theorem Verification.chatterjeeXi_eq_integral_conditionalLaw (C : ProbabilityTheory.Copula 2) : C.chatterjeeXi = ∫ (μ : MeasureTheory.ProbabilityMeasure ↑unitInterval), lawXiCost μ ∂↑(conditionalLaw C)

Xi is a continuous linear statistic of the law of conditional laws.

theorem Verification.correlationRatio_eq_integral_conditionalLaw (C : ProbabilityTheory.Copula 2) : correlationRatio C = ∫ (μ : MeasureTheory.ProbabilityMeasure ↑unitInterval), lawEtaCost μ ∂↑(conditionalLaw C)

The correlation ratio is another continuous linear statistic of the same law.