← Copula mathematical handbook

Feasibility of the glued magnitude potential

The proof separates the lower square, the upper square, and the mixed rectangles. This is the global inequality in Lemma 4.1 of Ansari–Rockel–Steinmassl, including points outside the attaining support.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.gluedPotential (a t : ℝ) (F : ℝ → ℝ) (x : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.gluedPotential a t F x = if x ≤ a then x * (t - x) / 2 else F x

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.gluedPotential_of_le {a t x : ℝ} (F : ℝ → ℝ) (hx : x ≤ a) : gluedPotential a t F x = x * (t - x) / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.gluedPotential_of_ge {a t x : ℝ} (F : ℝ → ℝ) (hjoin : F a = a * (t - a) / 2) (hx : a ≤ x) : gluedPotential a t F x = F x

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.upper_square_feasible {a t : ℝ} {F : ℝ → ℝ} (ha0 : 0 ≤ a) (hat : a ≤ t) (hta : t ≤ 2 * a) (hjoin : F a = a * (t - a) / 2) (hmono : MonotoneOn F (Set.Icc a 1)) (hpositive : ∀ (x y : ℝ), a ≤ x → x ≤ y → y ≤ 1 → x * (y - t) ≤ F x + F y) {x y : ℝ} (hax : a ≤ x) (hxy : x ≤ y) (hy1 : y ≤ 1) : x * |y - t| ≤ F x + F y

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.gluedPotential_feasible {a t : ℝ} {F : ℝ → ℝ} (ha0 : 0 ≤ a) (hat : a ≤ t) (hta : t ≤ 2 * a) (hjoin : F a = a * (t - a) / 2) (hmono : MonotoneOn F (Set.Icc a 1)) (hpositive : ∀ (x y : ℝ), a ≤ x → x ≤ y → y ≤ 1 → x * (y - t) ≤ F x + F y) (x y : ↑unitInterval) : min ↑x ↑y * |max ↑x ↑y - t| ≤ gluedPotential a t F ↑x + gluedPotential a t F ↑y

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.continuous_gluedPotential {a t : ℝ} {F : ℝ → ℝ} (hF : Continuous F) (hjoin : F a = a * (t - a) / 2) : Continuous (gluedPotential a t F)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.upperPotential (a t z : ℝ) (h : ℝ → ℝ) (x : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.upperPotential a t z h x = (x ^ 2 - t * x) / 2 - z ^ 2 / 2 * h ((x - a) / z)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.continuous_upperPotential (a t z : ℝ) {h : ℝ → ℝ} (hh : Continuous h) : Continuous (upperPotential a t z h)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.upperPotential_join {a t z : ℝ} {h : ℝ → ℝ} (hmatch : z ^ 2 * h 0 = 2 * a * (a - t)) : upperPotential a t z h a = a * (t - a) / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.upperPotential_monotone {a t z w : ℝ} {h : ℝ → ℝ} (hz : 0 < z) (hw : 0 ≤ w) (hL : LipschitzWith ⟨w, hw⟩ h) (ha : t + z * w ≤ 2 * a) : MonotoneOn (upperPotential a t z h) (Set.Ici a)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.upperPotential_positive_cost {a t z s : ℝ} {h : ℝ → ℝ} (hz : 0 < z) (haz : a + z = 1) (ht : t = z * s) (hdual : ∀ (u v : ↑unitInterval), h ↑u + h ↑v ≤ (↑u - ↑v) ^ 2 - s * |↑u - ↑v|) (x y : ℝ) (hax : a ≤ x) (hxy : x ≤ y) (hy1 : y ≤ 1) : x * (y - t) ≤ upperPotential a t z h x + upperPotential a t z h y