← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.potential_eq_base_closed {n v w x : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hp : 0 < period n v w) (hx : x ∈ Set.Icc 0 (period n v w)) : potential n v w hp x = basePotential n v w x

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.potential_piecePoint {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hp : 0 < period n v w) (i : Fin 4) (s : ↑unitInterval) : potential n v w hp (piecePoint n v w i ↑s) = pieceValue n v w i ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.potential_translated_piecePoint {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hp : 0 < period n v w) (k : ℕ) (i : Fin 4) (s : ↑unitInterval) : potential n v w hp (↑k * period n v w + piecePoint n v w i ↑s) = pieceValue n v w i ↑s