← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.a_le_complete {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : SignData ι) (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) : S.a u ≤ completeSigns.a u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.two_weight_witness {a : ℝ} (ha : 0 ≤ a) (ha' : a ≤ 1 / 4) : ∃ (v : Fin 2 → ℝ), (∀ (i : Fin 2), 0 ≤ v i) ∧ ∑ i : Fin 2, v i = 1 ∧ completeSigns.a v = a ∧ completeSigns.b v = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.small_inversion_complete {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) (ha : S.a u ≤ 1 / 4) : ∃ (v : Fin 2 → ℝ), (∀ (i : Fin 2), 0 ≤ v i) ∧ ∑ i : Fin 2, v i = 1 ∧ completeSigns.a v = S.a u ∧ completeSigns.b v ≤ S.b u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.a_le_quarter_of_card_le_two {n : ℕ} (hn : n ≤ 2) (S : SignData (Fin n)) (u : Fin n → ℝ) (hu : ∀ (i : Fin n), 0 ≤ u i) (hs : ∑ i : Fin n, u i = 1) : S.a u ≤ 1 / 4

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.exists_third_index {n : ℕ} (hn : 3 ≤ n) (p q : Fin n) : ∃ (k : Fin n), k ≠ p ∧ k ≠ q