Documentation

Copula.Rank.Region.RhoFootrule.UpperLeftMoments

← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.distance (S : LeftData) :

S.Index → ℝ → ℝ

Equations

S.distance (Sum.inl val) x✝ = S.w + (↑S.N + 1) * S.v
S.distance (Sum.inr (Sum.inl val)) x✝ = S.w + ↑S.N * S.v + S.v * x✝
S.distance (Sum.inr (Sum.inr val)) x✝ = S.w + (↑S.N + 1) * S.v - S.v * x✝

Instances For

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.distance_nonneg (S : LeftData) (i : S.Index) (s : ↑unitInterval) :

0 ≤ S.distance i ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.path_delta (S : LeftData) (i : S.Index) (s : ↑unitInterval) :

↑(S.path i s 1) - ↑(S.path i s 0) = S.distance i ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.path_abs_distance (S : LeftData) (i : S.Index) (s : ↑unitInterval) :

|↑(S.path i s 0) - ↑(S.path i s 1)| = S.distance i ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.symmetric_abs_distance (S : LeftData) (i : S.Index × Bool) (s : ↑unitInterval) :

|↑(S.symmetricPath i s 0) - ↑(S.symmetricPath i s 1)| = S.distance i.1 ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_distance_cost (S : LeftData) (f : ℝ → ℝ) (hf : Continuous f) :

∫ (x : Fin 2 → ↑unitInterval), f |↑(x 0) - ↑(x 1)| ∂S.copula.toMeasure = 2 * ∑ i : S.Index, S.weight i * ∫ (s : ↑unitInterval), f (S.distance i ↑s)

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_distance_reversed (S : LeftData) (f : ℝ → ℝ) :

∫ (s : ↑unitInterval), f (S.w + (↑S.N + 1) * S.v - S.v * ↑s) = ∫ (s : ↑unitInterval), f (S.w + ↑S.N * S.v + S.v * ↑s)

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_distance_formula (S : LeftData) (f : ℝ → ℝ) (hf : Continuous f) :

∫ (x : Fin 2 → ↑unitInterval), f |↑(x 0) - ↑(x 1)| ∂S.copula.toMeasure = 2 * ↑S.N * S.w * f (S.w + (↑S.N + 1) * S.v) + 2 * ↑S.N * (↑S.N + 1) * S.v * ∫ (s : ↑unitInterval), f (S.w + ↑S.N * S.v + S.v * ↑s)

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_abs_distance (S : LeftData) :

∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂S.copula.toMeasure = S.w + (↑S.N + 1) * S.v - ↑S.N * (↑S.N + 1) * S.v ^ 2

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_sq_distance (S : LeftData) :

∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂S.copula.toMeasure = (S.w + (↑S.N + 1) * S.v) ^ 2 - 2 * ↑S.N * (↑S.N + 1) * (S.w + (↑S.N + 1) * S.v) * S.v ^ 2 + 2 / 3 * ↑S.N * (↑S.N + 1) * S.v ^ 3

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.footrule (S : LeftData) :

S.copula.spearmanFootrule = 1 - 3 * (S.w + (↑S.N + 1) * S.v - ↑S.N * (↑S.N + 1) * S.v ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.rho (S : LeftData) :

S.copula.spearmanRho = 1 - 6 * ((S.w + (↑S.N + 1) * S.v) ^ 2 - 2 * ↑S.N * (↑S.N + 1) * (S.w + (↑S.N + 1) * S.v) * S.v ^ 2 + 2 / 3 * ↑S.N * (↑S.N + 1) * S.v ^ 3)