← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.weighted2 {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (f : ι → ι → ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.weighted2 u f = ∑ i : ι, ∑ j : ι, u i * u j * f i j

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3 {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (f : ι → ι → ι → ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3 u f = ∑ i : ι, ∑ j : ι, ∑ k : ι, u i * u j * u k * f i j k

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3_swap_left {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (f : ι → ι → ι → ℝ) : weighted3 u f = weighted3 u fun (i j k : ι) => f j i k

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3_swap_right {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (f : ι → ι → ι → ℝ) : weighted3 u f = weighted3 u fun (i j k : ι) => f i k j

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3_swap_outer {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (f : ι → ι → ι → ℝ) : weighted3 u f = weighted3 u fun (i j k : ι) => f k j i

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3_add {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (f g : ι → ι → ι → ℝ) : (weighted3 u fun (i j k : ι) => f i j k + g i j k) = weighted3 u f + weighted3 u g

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3_sub {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (f g : ι → ι → ι → ℝ) : (weighted3 u fun (i j k : ι) => f i j k - g i j k) = weighted3 u f - weighted3 u g

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3_neg {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (f : ι → ι → ι → ℝ) : (weighted3 u fun (i j k : ι) => -f i j k) = -weighted3 u f

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3_pair {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (hs : ∑ i : ι, u i = 1) (f : ι → ι → ℝ) : (weighted3 u fun (i j x : ι) => f i j) = weighted2 u f

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted3_shared {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (a b : ι → ι → ℝ) : (weighted3 u fun (i j k : ι) => a i j * b i k) = ∑ i : ι, (u i * ∑ j : ι, a i j * u j) * ∑ k : ι, b i k * u k

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.weighted_cycle_product {ι : Type u_1} [Fintype ι] (u : ι → ℝ) (hs : ∑ i : ι, u i = 1) (a b : ι → ι → ℝ) (ha : ∀ (i j : ι), a j i = -a i j) (hb : ∀ (i j : ι), b j i = -b i j) : (weighted3 u fun (i j k : ι) => (a i j - a i k + a j k) * (b i j - b i k + b j k)) = (3 * weighted2 u fun (i j : ι) => a i j * b i j) - 6 * ∑ i : ι, (u i * ∑ j : ι, a i j * u j) * ∑ k : ι, b i k * u k

The six mixed terms in the cycle product all reduce to the same rank moment.