← Copula mathematical handbook

def ProbabilityTheory.Copula.RankRegion.RhoTau.CompleteReplacement {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.CompleteReplacement.transport {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {S : SignData ι} {T : SignData κ} {u : ι → ℝ} {v : κ → ℝ} (h : CompleteReplacement T v) (ha : T.a v = S.a u) (hb : T.b v ≤ S.b u) : CompleteReplacement S u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.completeReplacement_small {ι : Type u_1} [Fintype ι] (S : SignData ι) (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) (ha : S.a u ≤ 1 / 4) : CompleteReplacement S u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.normalized_remainder {n : ℕ} (u : Fin (n + 1) → ℝ) (hu : ∀ (i : Fin (n + 1)), 0 ≤ u i) (hs : ∑ i : Fin (n + 1), u i = 1) (i : Fin (n + 1)) (hi : u i < 1) : (∀ (j : Fin n), 0 ≤ u (i.succAbove j) / (1 - u i)) ∧ ∑ j : Fin n, u (i.succAbove j) / (1 - u i) = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.completeReplacement_endpoint {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) (u : Fin (n + 1) → ℝ) (hu : ∀ (i : Fin (n + 1)), 0 ≤ u i) (hs : ∑ i : Fin (n + 1), u i = 1) (i : Fin (n + 1)) (hi : u i < 1) (he : ∀ (j : Fin (n + 1)), j ≠ i → (permutationSigns π).edge i j = 1) (hrep : CompleteReplacement (permutationSigns (deletePermutation π i)) fun (j : Fin n) => u (i.succAbove j) / (1 - u i)) : CompleteReplacement (permutationSigns π) u

Reinsert a stripped endpoint into a complete replacement of the normalized remainder.