← Copula mathematical handbook

The supporting functional and transport weak duality

The magnitude law is constructed from the original copula. The supporting bound and contact-set certificate do not assume the proposed optimizer.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.magnitudeCost (t : ℝ) (x : Fin 2 → ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.magnitudeCost t x = min ↑(x 0) ↑(x 1) * |max ↑(x 0) ↑(x 1) - t|

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.continuous_magnitudeCost (t : ℝ) : Continuous (magnitudeCost t)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.integral_magnitudeCopula (C : Copula 2) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(magnitudeCopula C).toMeasure = ∫ (x : Fin 2 → ↑unitInterval), f fun (i : Fin 2) => rankMagnitude (x i) ∂C.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.supporting_functional (C : Copula 2) (t : ℝ) : C.spearmanRho - 3 / 2 * t * C.giniGamma = 3 * ∫ (x : Fin 2 → ↑unitInterval), rankSign x * min ↑(rankMagnitude (x 0)) ↑(rankMagnitude (x 1)) * (max ↑(rankMagnitude (x 0)) ↑(rankMagnitude (x 1)) - t) ∂C.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.supporting_functional_le (C : Copula 2) (t : ℝ) : C.spearmanRho - 3 / 2 * t * C.giniGamma ≤ 3 * ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂(magnitudeCopula C).toMeasure

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.transport_weak_duality (C : Copula 2) (t : ℝ) {f : ↑unitInterval → ℝ} (hf : Continuous f) (hfeasible : ∀ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ≤ f (x 0) + f (x 1)) : ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂C.toMeasure ≤ 2 * ∫ (u : ↑unitInterval), f u

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.transport_contact_value (C : Copula 2) (t : ℝ) {f : ↑unitInterval → ℝ} (hf : Continuous f) (hcontact : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, magnitudeCost t x = f (x 0) + f (x 1)) : ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂C.toMeasure = 2 * ∫ (u : ↑unitInterval), f u

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.transport_contact_optimal (C : Copula 2) (t : ℝ) {f : ↑unitInterval → ℝ} (hf : Continuous f) (hfeasible : ∀ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ≤ f (x 0) + f (x 1)) (hcontact : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, magnitudeCost t x = f (x 0) + f (x 1)) : (∀ (D : Copula 2), ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂D.toMeasure ≤ ∫ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ∂C.toMeasure) ∧ ∀ (g : ↑unitInterval → ℝ), Continuous g → (∀ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ≤ g (x 0) + g (x 1)) → 2 * ∫ (u : ↑unitInterval), f u ≤ 2 * ∫ (u : ↑unitInterval), g u