← Mathematical handbook

Copulas from a Lipschitz displacement on two median strips

structure Verification.StripDisplacement : Type

• toFun : ↑unitInterval → ℝ
• zero : self.toFun 0 = 0
• one : self.toFun 1 = 0
• lipschitz (v w : ↑unitInterval) : |self.toFun v - self.toFun w| ≤ |↑v - ↑w|

@[instance_reducible]

instance Verification.instCoeFunStripDisplacementForallElemRealUnitInterval : CoeFun StripDisplacement fun (x : StripDisplacement) => ↑unitInterval → ℝ

Equations

• Verification.instCoeFunStripDisplacementForallElemRealUnitInterval = { coe := Verification.StripDisplacement.toFun }

noncomputable def Verification.medianWedge (u : ↑unitInterval) : ℝ

Equations

• Verification.medianWedge u = min (↑u) (1 - ↑u)

theorem Verification.medianWedge_lipschitz (u v : ↑unitInterval) : |medianWedge u - medianWedge v| ≤ |↑u - ↑v|

theorem Verification.StripDisplacement.continuous (g : StripDisplacement) : Continuous g.toFun

theorem Verification.StripDisplacement.abs_le (g : StripDisplacement) (v : ↑unitInterval) : |g.toFun v| ≤ ↑v

noncomputable def Verification.twoStrip (g : StripDisplacement) : ProbabilityTheory.Copula 2

Equations

• Verification.twoStrip g = ProbabilityTheory.Copula.ofClassical (fun (x : Fin 2 → ↑unitInterval) => ↑(x 0) * ↑(x 1) + Verification.medianWedge (x 0) * g.toFun (x 1)) ⋯

@[simp]

theorem Verification.cdf_twoStrip (g : StripDisplacement) (u v : ↑unitInterval) : (twoStrip g).cdf ![u, v] = ↑u * ↑v + medianWedge u * g.toFun v

noncomputable def Verification.stripKernel (g : StripDisplacement) (v u : ↑unitInterval) : ℝ

Equations

• Verification.stripKernel g v u = if u ≤ ProbabilityTheory.Copula.unitHalf then ↑v + g.toFun v else ↑v - g.toFun v

theorem Verification.stripKernel_integrable (g : StripDisplacement) (v : ↑unitInterval) : MeasureTheory.Integrable (stripKernel g v) MeasureTheory.volume

theorem Verification.integral_median_step (p q : ℝ) (u : ↑unitInterval) : (∫ (t : ↑unitInterval) in Set.Iic u, if t ≤ ProbabilityTheory.Copula.unitHalf then p else q) = min (↑u) (1 / 2) * p + max 0 (↑u - 1 / 2) * q

Exact integration of any two constants separated at the median.

theorem Verification.integral_stripKernel_Iic (g : StripDisplacement) (v u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, stripKernel g v t = (twoStrip g).cdf ![u, v]

theorem Verification.conditionalCDF_twoStrip (g : StripDisplacement) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (twoStrip g).conditionalCDF u v) =ᵐ[MeasureTheory.volume] stripKernel g v

theorem Verification.integral_stripKernel_sq (g : StripDisplacement) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), stripKernel g v u ^ 2 = ↑v ^ 2 + g.toFun v ^ 2

theorem Verification.xi_twoStrip (g : StripDisplacement) : (twoStrip g).chatterjeeXi = 6 * ∫ (v : ↑unitInterval), g.toFun v ^ 2

Population xi of the two-strip copula; valid for any Lipschitz displacement.

theorem Verification.beta_twoStrip (g : StripDisplacement) : (twoStrip g).blomqvistBeta = 2 * g.toFun ProbabilityTheory.Copula.unitHalf