← Mathematical handbook

The half-shift dual certificate for s >= 1

This covers the theta <= 1 branch of Lemma 3.5, with s = 1/theta, and the sufficient direction of Lemma 3.6. It includes the junction s=1.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotential (s : ℝ) (u : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotential s u = 3 / 8 - s / 2 + (s - 1) * ProbabilityTheory.Copula.RankRegion.RhoGamma.medianWedge✝ u

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.continuous_halfShiftPotential (s : ℝ) : Continuous (halfShiftPotential s)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotentialReal (s u : ℝ) : ℝ

The same potential on the real line, used for its derivative bound.

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotentialReal s u = 3 / 8 - s / 2 + (s - 1) * min u (1 - u)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotentialReal_lipschitz {s : ℝ} (hs : 1 ≤ s) : LipschitzWith ⟨s - 1, ⋯⟩ (halfShiftPotentialReal s)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotential_lipschitz {s : ℝ} (hs : 1 ≤ s) : LipschitzWith ⟨s - 1, ⋯⟩ (halfShiftPotential s)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotential_deriv_bound {s : ℝ} (hs : 1 ≤ s) (u : ℝ) : |deriv (halfShiftPotentialReal s) u| ≤ s - 1

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotential_zero (s : ℝ) : halfShiftPotential s 0 = 3 / 8 - s / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotential_integral (s : ℝ) : 2 * ∫ (u : ↑unitInterval), halfShiftPotential s u = 1 / 4 - s / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotential_feasible {s : ℝ} (hs : 1 ≤ s) (u v : ↑unitInterval) : halfShiftPotential s u + halfShiftPotential s v ≤ (↑u - ↑v) ^ 2 - s * |↑u - ↑v|

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShift_cost (s : ℝ) : ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 - s * |↑(x 0) - ↑(x 1)| ∂RhoFootrule.halfTurn.toMeasure = 1 / 4 - s / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShift_optimal {s : ℝ} (hs : 1 ≤ s) (C : Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 - s * |↑(x 0) - ↑(x 1)| ∂RhoFootrule.halfTurn.toMeasure ≤ ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 - s * |↑(x 0) - ↑(x 1)| ∂C.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShiftPotential_contact (s : ℝ) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂RhoFootrule.halfTurn.toMeasure, halfShiftPotential s (x 0) + halfShiftPotential s (x 1) = (↑(x 0) - ↑(x 1)) ^ 2 - s * |↑(x 0) - ↑(x 1)|