← Copula mathematical handbook

structure ProbabilityTheory.Copula.RankRegion.RhoTau.JoinedIncreasingArcs (f : ℕ → ↑unitInterval → ℝ) : Prop

• strictMono (n : ℕ) : StrictMono (f n)
• join (n : ℕ) : f n 0 = f (n + 1) 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.JoinedIncreasingArcs.junction_strictAnti {f : ℕ → ↑unitInterval → ℝ} (h : JoinedIncreasingArcs f) : StrictAnti fun (n : ℕ) => f n 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.JoinedIncreasingArcs.ordered {f : ℕ → ↑unitInterval → ℝ} (h : JoinedIncreasingArcs f) {n m : ℕ} (hnm : n < m) (s t : ↑unitInterval) : f m t ≤ f n s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.JoinedIncreasingArcs.eq_of_ordered {f : ℕ → ↑unitInterval → ℝ} (h : JoinedIncreasingArcs f) {n m : ℕ} (hnm : n < m) {s t : ↑unitInterval} (he : f n s = f m t) : s = 0 ∧ t = 1 ∧ m = n + 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.joined_arcs_order {f g : ℕ → ↑unitInterval → ℝ} (hf : JoinedIncreasingArcs f) (hg : JoinedIncreasingArcs g) {n m : ℕ} {s t : ↑unitInterval} (h : f n s ≤ f m t) : g n s ≤ g m t

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.joined_arcTau : JoinedIncreasingArcs fun (n : ℕ) (s : ↑unitInterval) => arcTau n ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.joined_arcRho : JoinedIncreasingArcs fun (n : ℕ) (s : ↑unitInterval) => arcRho n ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.arcTau_gt_neg_one (n : ℕ) (s : ↑unitInterval) : -1 < arcTau n ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.arcRho_gt_neg_one (n : ℕ) (s : ↑unitInterval) : -1 < arcRho n ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.order_iff (a b : LowerParameter) : a.tau ≤ b.tau ↔ a.rho ≤ b.rho

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.tau_eq_iff (a b : LowerParameter) : a.tau = b.tau ↔ a.rho = b.rho