← Mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.left_offset_neg {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hp : 0 < RhoFootrule.UpperSpline.period n v w) : RhoFootrule.UpperSpline.offset n v w + v * w < 0

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.right_offset_neg {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hp : 0 < RhoFootrule.UpperSpline.period n v w) : RhoFootrule.UpperSpline.offset n v w < 0

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.right_discriminant_bound {n v w : ℝ} (hn : 0 ≤ n) (hv : 0 ≤ v) (hw : 0 ≤ w) : v ^ 2 ≤ RhoFootrule.UpperSpline.period n v w ^ 2 + 2 * RhoFootrule.UpperSpline.offset n v w

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.left_discriminant_bound {n v w : ℝ} (hn : 0 ≤ n) (hv : 0 ≤ v) (hw : 0 ≤ w) : v ^ 2 ≤ RhoFootrule.UpperSpline.period n v w ^ 2 + 2 * (RhoFootrule.UpperSpline.offset n v w + v * w)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.right_dual_zero (S : RhoFootrule.RightData) : S.dual 0 = RhoFootrule.UpperSpline.offset (↑S.N) S.v S.w

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.left_dual_zero (S : RhoFootrule.LeftData) : S.dual 0 = RhoFootrule.UpperSpline.offset (↑S.N) S.v S.w + S.v * S.w

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.right_dual_lipschitz (S : RhoFootrule.RightData) : LipschitzWith ⟨S.v, ⋯⟩ S.dual

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.left_dual_lipschitz (S : RhoFootrule.LeftData) : LipschitzWith ⟨S.v, ⋯⟩ S.dual

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShift_endpoint_properties {s : ℝ} (hs : 1 ≤ s) : 3 / 8 - s / 2 < 0 ∧ (s - 1) ^ 2 ≤ s ^ 2 + 2 * (3 / 8 - s / 2)