← Copula mathematical handbook

Exact density identification for two-strip copulas

noncomputable def ProbabilityTheory.Copula.RankRegion.Common.lowerStep (a u : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.Common.lowerStep a u = if u ≤ a then 1 else 0

theorem ProbabilityTheory.Copula.RankRegion.Common.measurable_lowerStep (a : ↑unitInterval) : Measurable (lowerStep a)

theorem ProbabilityTheory.Copula.RankRegion.Common.integrable_lowerStep (a : ↑unitInterval) : MeasureTheory.Integrable (lowerStep a) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.Common.integral_lowerStep (a u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, lowerStep a t = min ↑u ↑a

noncomputable def ProbabilityTheory.Copula.RankRegion.Common.medianSign (u : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.Common.medianSign u = if u ≤ ProbabilityTheory.Copula.unitHalf then 1 else -1

theorem ProbabilityTheory.Copula.RankRegion.Common.measurable_medianSign : Measurable medianSign

theorem ProbabilityTheory.Copula.RankRegion.Common.integral_medianSign (u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, medianSign t = medianWedge u

theorem ProbabilityTheory.Copula.RankRegion.Common.twoStrip_density (g : StripDisplacement) (d : ↑unitInterval → ℝ) (hd : Measurable d) (hd1 : ∀ (v : ↑unitInterval), |d v| ≤ 1) (hprimitive : ∀ (v : ↑unitInterval), ∫ (t : ↑unitInterval) in Set.Iic v, d t = g.toFun v) : (twoStrip g).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (1 + medianSign (x 0) * d (x 1))