← Mathematical handbook

Copulas from a Lipschitz displacement on two median strips

structure ProbabilityTheory.Copula.RankRegion.XiRho.Support.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 ProbabilityTheory.Copula.RankRegion.XiRho.Support.instCoeFunStripDisplacementForallElemRealUnitInterval : CoeFun StripDisplacement fun (x : StripDisplacement) => ↑unitInterval → ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.Support.instCoeFunStripDisplacementForallElemRealUnitInterval = { coe := ProbabilityTheory.Copula.RankRegion.XiRho.Support.StripDisplacement.toFun }

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.Support.medianWedge (u : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.Support.medianWedge u = min (↑u) (1 - ↑u)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.medianWedge_lipschitz (u v : ↑unitInterval) : |medianWedge u - medianWedge v| ≤ |↑u - ↑v|

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.StripDisplacement.continuous (g : StripDisplacement) : Continuous g.toFun

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.StripDisplacement.abs_le (g : StripDisplacement) (v : ↑unitInterval) : |g.toFun v| ≤ ↑v

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.Support.twoStrip (g : StripDisplacement) : Copula 2

Equations

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

@[simp]

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.cdf_twoStrip (g : StripDisplacement) (u v : ↑unitInterval) : (twoStrip g).cdf ![u, v] = ↑u * ↑v + medianWedge u * g.toFun v

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.Support.stripKernel (g : StripDisplacement) (v u : ↑unitInterval) : ℝ

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.stripKernel_integrable (g : StripDisplacement) (v : ↑unitInterval) : MeasureTheory.Integrable (stripKernel g v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.integral_median_step (p q : ℝ) (u : ↑unitInterval) : (∫ (t : ↑unitInterval) in Set.Iic u, if t ≤ 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 ProbabilityTheory.Copula.RankRegion.XiRho.Support.integral_stripKernel_Iic (g : StripDisplacement) (v u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, stripKernel g v t = (twoStrip g).cdf ![u, v]

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.conditionalCDF_twoStrip (g : StripDisplacement) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (twoStrip g).conditionalCDF u v) =ᵐ[MeasureTheory.volume] stripKernel g v

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.integral_stripKernel_sq (g : StripDisplacement) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), stripKernel g v u ^ 2 = ↑v ^ 2 + g.toFun v ^ 2

theorem ProbabilityTheory.Copula.RankRegion.XiRho.Support.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 ProbabilityTheory.Copula.RankRegion.XiRho.Support.beta_twoStrip (g : StripDisplacement) : (twoStrip g).blomqvistBeta = 2 * g.toFun unitHalf