← Copula mathematical handbook

Quadratically clamped copulas for the xi–Blest boundary

The intercept is chosen by the uniform marginal constraint. Its existence uses the intermediate value theorem, and the ordering of its means proves monotonicity in the response threshold. No asserted copula or optimizer is passed as a hypothesis.

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMean (b a : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMean b a = ∫ (u : ↑unitInterval), ProbabilityTheory.Copula.RankRegion.Common.unitClamp (a + b * (1 - ↑u) ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.continuous_quadraticMean (b : ℝ) : Continuous (quadraticMean b)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMean_monotone (b : ℝ) : Monotone (quadraticMean b)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMean_zero (b : ℝ) (hb : 0 ≤ b) : quadraticMean b (-b) = 0

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticMean_top (b : ℝ) (hb : 0 ≤ b) : quadraticMean b 1 = 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.exists_quadratic_intercept (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : ∃ a ∈ Set.Icc (-b) 1, quadraticMean b a = ↑v

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticIntercept (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticIntercept b hb v = if v = 0 then -b else if v = 1 then 1 else ⋯.choose

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticIntercept_mean (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : quadraticMean b (quadraticIntercept b hb v) = ↑v

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticIntercept_monotone (b : ℝ) (hb : 0 ≤ b) : Monotone (quadraticIntercept b hb)

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticKernel (b : ℝ) (hb : 0 ≤ b) (v u : ↑unitInterval) : ℝ

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticKernel_integrable (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : MeasureTheory.Integrable (quadraticKernel b hb v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticKernel_monotone (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : Monotone fun (v : ↑unitInterval) => quadraticKernel b hb v u

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticKernel_zero (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : quadraticKernel b hb 0 u = 0

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticKernel_one (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : quadraticKernel b hb 1 u = 1

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticBand (b : ℝ) (hb : 0 ≤ b) : Copula 2

Actual quadratic-band copula at slope b; normalization is solved internally.

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticBand_cdf (b : ℝ) (hb : 0 ≤ b) (u v : ↑unitInterval) : (quadraticBand b hb).cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, unitClamp (quadraticIntercept b hb v + b * (1 - ↑t) ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticBand_conditionalCDF (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (quadraticBand b hb).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => unitClamp (quadraticIntercept b hb v + b * (1 - ↑u) ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticBand_isSI (b : ℝ) (hb : 0 ≤ b) : (quadraticBand b hb).IsSI