← Mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.a (A : AuxiliaryCertificate) : ↑unitInterval

Equations

• A.a = ⟨ProbabilityTheory.Copula.RankRegion.RhoGamma.centralLength A.s A.c, ⋯⟩

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.z (A : AuxiliaryCertificate) : ℝ

Equations

• A.z = ProbabilityTheory.Copula.RankRegion.RhoGamma.cornerLength A.s A.c

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.t (A : AuxiliaryCertificate) : ℝ

Equations

• A.t = ProbabilityTheory.Copula.RankRegion.RhoGamma.supportingSlope A.s A.c

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.a_pos (A : AuxiliaryCertificate) : 0 < ↑A.a

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.a_lt_one (A : AuxiliaryCertificate) : ↑A.a < 1

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.z_pos (A : AuxiliaryCertificate) : 0 < A.z

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.a_add_z (A : AuxiliaryCertificate) : ↑A.a + A.z = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.a_lt_t (A : AuxiliaryCertificate) : ↑A.a < A.t

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.slope_bound (A : AuxiliaryCertificate) : A.t + A.z * A.w ≤ 2 * ↑A.a

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.matching (A : AuxiliaryCertificate) : A.z ^ 2 * A.c = 2 * ↑A.a * (↑A.a - A.t)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.t_eq (A : AuxiliaryCertificate) : A.t = A.z * A.s

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.upper (A : AuxiliaryCertificate) : ℝ → ℝ

Equations

• A.upper = ProbabilityTheory.Copula.RankRegion.RhoGamma.upperPotential (↑A.a) A.t A.z A.h

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.continuous_upper (A : AuxiliaryCertificate) : Continuous A.upper

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.upper_join (A : AuxiliaryCertificate) : A.upper ↑A.a = ↑A.a * (A.t - ↑A.a) / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.upper_monotone (A : AuxiliaryCertificate) : MonotoneOn A.upper (Set.Icc (↑A.a) 1)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.upper_positive (A : AuxiliaryCertificate) (x y : ℝ) (hax : ↑A.a ≤ x) (hxy : x ≤ y) (hy1 : y ≤ 1) : x * (y - A.t) ≤ A.upper x + A.upper y

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.dual (A : AuxiliaryCertificate) : ℝ → ℝ

Equations

• A.dual = ProbabilityTheory.Copula.RankRegion.RhoGamma.gluedPotential (↑A.a) A.t A.upper

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.continuous_dual (A : AuxiliaryCertificate) : Continuous A.dual

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.dual_feasible (A : AuxiliaryCertificate) (x y : ↑unitInterval) : min ↑x ↑y * |max ↑x ↑y - A.t| ≤ A.dual ↑x + A.dual ↑y

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.magnitudes (A : AuxiliaryCertificate) : Copula 2

Equations

• A.magnitudes = (ProbabilityTheory.Copula.comonotonic 2).ordinalSum A.D A.a

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.upper_embed_value (A : AuxiliaryCertificate) (u : ↑unitInterval) : A.upper ↑(OrdinalSum.upperEmbed A.a u) = ((↑A.a + A.z * ↑u) ^ 2 - A.t * (↑A.a + A.z * ↑u)) / 2 - A.z ^ 2 / 2 * A.h ↑u

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.upper_contact_signed (A : AuxiliaryCertificate) (u v : ↑unitInterval) (hc : A.h ↑u + A.h ↑v = (↑u - ↑v) ^ 2 - A.s * |↑u - ↑v|) : A.upper ↑(OrdinalSum.upperEmbed A.a u) + A.upper ↑(OrdinalSum.upperEmbed A.a v) = ↑(OrdinalSum.upperEmbed A.a u) * ↑(OrdinalSum.upperEmbed A.a v) - A.t * min ↑(OrdinalSum.upperEmbed A.a u) ↑(OrdinalSum.upperEmbed A.a v)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.upper_contact (A : AuxiliaryCertificate) (u v : ↑unitInterval) (hc : A.h ↑u + A.h ↑v = (↑u - ↑v) ^ 2 - A.s * |↑u - ↑v|) : min ↑(OrdinalSum.upperEmbed A.a u) ↑(OrdinalSum.upperEmbed A.a v) * |max ↑(OrdinalSum.upperEmbed A.a u) ↑(OrdinalSum.upperEmbed A.a v) - A.t| = A.dual ↑(OrdinalSum.upperEmbed A.a u) + A.dual ↑(OrdinalSum.upperEmbed A.a v)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.lower_contact (A : AuxiliaryCertificate) (u : ↑unitInterval) : ↑(OrdinalSum.lowerEmbed A.a u) * |↑(OrdinalSum.lowerEmbed A.a u) - A.t| = A.dual ↑(OrdinalSum.lowerEmbed A.a u) + A.dual ↑(OrdinalSum.lowerEmbed A.a u)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.magnitude_contact (A : AuxiliaryCertificate) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂A.magnitudes.toMeasure, magnitudeCost A.t x = A.dual ↑(x 0) + A.dual ↑(x 1)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.copula (A : AuxiliaryCertificate) : Copula 2

Equations

• A.copula = ProbabilityTheory.Copula.RankRegion.RhoGamma.signOptimizer A.magnitudes A.t

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.supporting_bound (A : AuxiliaryCertificate) (C : Copula 2) : C.spearmanRho - 3 / 2 * A.t * C.giniGamma ≤ A.copula.spearmanRho - 3 / 2 * A.t * A.copula.giniGamma

Every concrete auxiliary branch yields an attained global rho–gamma support line.