← Mathematical handbook

Universal xi-footrule lower bounds from the two-bin relaxation

The relaxed profile is not asserted to be a copula. Its two rank-like integrals give a lower bound on the weighted objective for every copula.

noncomputable def Verification.conditionalBinLow (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : ℝ

Equations

• Verification.conditionalBinLow C v = C.cdf ![v, v] / ↑v

noncomputable def Verification.conditionalBinHigh (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : ℝ

Equations

• Verification.conditionalBinHigh C v = (↑v - C.cdf ![v, v]) / (1 - ↑v)

theorem Verification.conditionalBin_feasible (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (hv : 0 < ↑v ∧ ↑v < 1) : conditionalBinLow C v ∈ Set.Icc 0 1 ∧ conditionalBinHigh C v ∈ Set.Icc 0 1 ∧ ↑v * conditionalBinLow C v + (1 - ↑v) * conditionalBinHigh C v = ↑v

theorem Verification.conditionalBin_left_mass (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (hv : 0 < ↑v) : ∫ (u : ↑unitInterval) in Set.Iic v, C.conditionalCDF u v = ↑v * conditionalBinLow C v

theorem Verification.conditionalBin_jensen (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (hv : 0 < ↑v ∧ ↑v < 1) : ↑v * conditionalBinLow C v ^ 2 + (1 - ↑v) * conditionalBinHigh C v ^ 2 ≤ ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2

theorem Verification.conditionalBin_jensen_eq_iff (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (hv : 0 < ↑v ∧ ↑v < 1) : ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 = ↑v * conditionalBinLow C v ^ 2 + (1 - ↑v) * conditionalBinHigh C v ^ 2 ↔ (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] twoBin v (conditionalBinLow C v) (conditionalBinHigh C v)

noncomputable def Verification.relaxedFootrule (μ : ℝ) : ℝ

Equations

• Verification.relaxedFootrule μ = (6 * ∫ (v : ↑unitInterval), ↑v * Verification.jensenLow μ v) - 2

noncomputable def Verification.relaxedXi (μ : ℝ) : ℝ

Equations

• Verification.relaxedXi μ = (6 * ∫ (v : ↑unitInterval), ↑v * Verification.jensenLow μ v ^ 2 + (1 - ↑v) * Verification.jensenHigh μ v ^ 2) - 2

theorem Verification.integrable_jensen_diagonal (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => ↑v * jensenLow μ v) MeasureTheory.volume

theorem Verification.integrable_jensen_square (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => ↑v * jensenLow μ v ^ 2 + (1 - ↑v) * jensenHigh μ v ^ 2) MeasureTheory.volume

theorem Verification.conditional_objective_lower_bound (C : ProbabilityTheory.Copula 2) (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) (hv : 0 < ↑v ∧ ↑v < 1) : splitObjective μ (↑v) (jensenLow μ v) (jensenHigh μ v) ≤ μ * C.cdf ![v, v] + ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2

theorem Verification.xi_footrule_relaxed_lower_bound (C : ProbabilityTheory.Copula 2) (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : μ * relaxedFootrule μ + relaxedXi μ ≤ μ * C.spearmanFootrule + C.chatterjeeXi

Theorem 3.2, with the relaxed values defined by their exact integrals.

theorem Verification.xi_lower_bound_at_relaxed_footrule (C : ProbabilityTheory.Copula 2) (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (hC : C.spearmanFootrule = relaxedFootrule μ) : relaxedXi μ ≤ C.chatterjeeXi

At a prescribed relaxed footrule value, the bound reduces to a xi bound.