← Mathematical handbook

structure ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate : Type

The analytic data used in gluing, with concrete instances for every auxiliary branch.

• s : ℝ
• s_pos : 0 < self.s
• w : ℝ
• w_nonneg : 0 ≤ self.w
• c : ℝ
• c_neg : self.c < 0
• discriminant : self.w ^ 2 ≤ self.s ^ 2 + 2 * self.c
• h : ℝ → ℝ
• lipschitz : LipschitzWith ⟨self.w, ⋯⟩ self.h
• at_zero : self.h 0 = self.c
• D : Copula 2
• feasible (u v : ↑unitInterval) : self.h ↑u + self.h ↑v ≤ (↑u - ↑v) ^ 2 - self.s * |↑u - ↑v|
• contact : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂self.D.toMeasure, self.h ↑(x 0) + self.h ↑(x 1) = (↑(x 0) - ↑(x 1)) ^ 2 - self.s * |↑(x 0) - ↑(x 1)|

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.auxiliary_contact_of_integral (D : Copula 2) (s : ℝ) {h : ℝ → ℝ} (hh : Continuous h) (hf : ∀ (u v : ↑unitInterval), h ↑u + h ↑v ≤ (↑u - ↑v) ^ 2 - s * |↑u - ↑v|) (hi : ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂D.toMeasure - s * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂D.toMeasure = 2 * ∫ (u : ↑unitInterval), h ↑u) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂D.toMeasure, h ↑(x 0) + h ↑(x 1) = (↑(x 0) - ↑(x 1)) ^ 2 - s * |↑(x 0) - ↑(x 1)|

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.ofRight (S : RhoFootrule.RightData) : AuxiliaryCertificate

Equations

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.ofLeft (S : RhoFootrule.LeftData) : AuxiliaryCertificate

Equations

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift (s : ℝ) (hs : 1 ≤ s) : AuxiliaryCertificate

Equations

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