← Mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.dual (S : LeftData) (x : ℝ) : ℝ

Equations

• S.dual x = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.potential (↑S.N) S.v S.w ⋯ (x + S.w)

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.continuous_dual (S : LeftData) : Continuous S.dual

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.dual_phase (S : LeftData) (k : ℕ) (i : Fin 4) (s : ↑unitInterval) : S.dual (S.phase k i ↑s) = UpperSpline.pieceValue (↑S.N) S.v S.w i ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.path_contact (S : LeftData) (i : S.Index) (s : ↑unitInterval) : S.dual ↑(S.path i s 0) + S.dual ↑(S.path i s 1) = S.distance i ↑s ^ 2 - UpperSpline.period (↑S.N) S.v S.w * S.distance i ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.symmetric_contact (S : LeftData) (i : S.Index × Bool) (s : ↑unitInterval) : S.dual ↑(S.symmetricPath i s 0) + S.dual ↑(S.symmetricPath i s 1) = |↑(S.symmetricPath i s 0) - ↑(S.symmetricPath i s 1)| ^ 2 - UpperSpline.period (↑S.N) S.v S.w * |↑(S.symmetricPath i s 0) - ↑(S.symmetricPath i s 1)|

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_dual (S : LeftData) (C : Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), S.dual ↑(x 0) + S.dual ↑(x 1) ∂C.toMeasure = 2 * ∫ (u : ↑unitInterval), S.dual ↑u

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.cost_lower_bound (S : LeftData) (C : Copula 2) : 2 * ∫ (u : ↑unitInterval), S.dual ↑u ≤ ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂C.toMeasure - UpperSpline.period (↑S.N) S.v S.w * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂C.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.cost_attained (S : LeftData) : ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂S.copula.toMeasure - UpperSpline.period (↑S.N) S.v S.w * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂S.copula.toMeasure = 2 * ∫ (u : ↑unitInterval), S.dual ↑u

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.supporting_bound (S : LeftData) (C : Copula 2) : C.spearmanRho - 2 * UpperSpline.period (↑S.N) S.v S.w * C.spearmanFootrule ≤ S.copula.spearmanRho - 2 * UpperSpline.period (↑S.N) S.v S.w * S.copula.spearmanFootrule

The supporting line is valid for every copula and is attained by this family.

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.maximizes_rho (S : LeftData) (C : Copula 2) (h : C.spearmanFootrule = S.copula.spearmanFootrule) : C.spearmanRho ≤ S.copula.spearmanRho