← Copula mathematical handbook

def ProbabilityTheory.Copula.RankRegion.RhoTau.IsInversion {n : ℕ} (π : Equiv.Perm (Fin n)) (i j : Fin n) : Prop

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.IsInversion π i j = (i < j ∧ π j < π i ∨ j < i ∧ π i < π j)

@[instance_reducible]

instance ProbabilityTheory.Copula.RankRegion.RhoTau.instDecidableIsInversion {n : ℕ} (π : Equiv.Perm (Fin n)) (i j : Fin n) : Decidable (IsInversion π i j)

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.instDecidableIsInversion π i j = ProbabilityTheory.Copula.RankRegion.RhoTau.instDecidableIsInversion._aux_1 π i j

def ProbabilityTheory.Copula.RankRegion.RhoTau.permutationSigns {n : ℕ} (π : Equiv.Perm (Fin n)) : SignData (Fin n)

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.permutation_inversion {n : ℕ} (π : Equiv.Perm (Fin n)) (i j : Fin n) : (permutationSigns π).inversion i j = if IsInversion π i j then 1 else 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.inversion_of_increasing {n : ℕ} (π : Equiv.Perm (Fin n)) {i j : Fin n} (hij : i < j) (hπ : π i < π j) : (permutationSigns π).inversion i j = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.inversion_of_decreasing {n : ℕ} (π : Equiv.Perm (Fin n)) {i j : Fin n} (hij : i < j) (hπ : π j < π i) : (permutationSigns π).inversion i j = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.edge_of_inversion_zero {n : ℕ} (S : SignData (Fin n)) {i j : Fin n} (h : S.inversion i j = 0) : S.edge i j = -1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.edge_of_inversion_one {n : ℕ} (S : SignData (Fin n)) {i j : Fin n} (h : S.inversion i j = 1) : S.edge i j = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.triple_of_increasing {n : ℕ} (π : Equiv.Perm (Fin n)) {i j k : Fin n} (hij : i < j) (hjk : j < k) (hpij : π i < π j) (hpjk : π j < π k) : (permutationSigns π).triple i j k = 0

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.permutation_increasing_reduction {n : ℕ} (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) (hu : ∀ (i : Fin n), 0 < u i) {p q r : Fin n} (hpq : p < q) (hqr : q < r) (hπpq : π p < π q) (hπqr : π q < π r) : ∃ (v : Fin n → ℝ), (∀ (i : Fin n), 0 ≤ v i) ∧ ∑ i : Fin n, v i = ∑ i : Fin n, u i ∧ (∃ (i : Fin n), v i = 0) ∧ (permutationSigns π).a v = (permutationSigns π).a u ∧ (permutationSigns π).b v ≤ (permutationSigns π).b u

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.permutation_four_reduction {n : ℕ} (π : Equiv.Perm (Fin n)) (u : Fin n → ℝ) (hu : ∀ (i : Fin n), 0 < u i) {p q r s : Fin n} (hpq : p < q) (hqr : q < r) (hrs : r < s) (hπrs : π r < π s) (hπsp : π s < π p) (hπpq : π p < π q) : ∃ (v : Fin n → ℝ), (∀ (i : Fin n), 0 ≤ v i) ∧ ∑ i : Fin n, v i = ∑ i : Fin n, u i ∧ (∃ (i : Fin n), v i = 0) ∧ (permutationSigns π).a v = (permutationSigns π).a u ∧ (permutationSigns π).b v ≤ (permutationSigns π).b u