← 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 Verification.quadraticMean (b a : ℝ) : ℝ

Equations

• Verification.quadraticMean b a = ∫ (u : ↑unitInterval), Verification.unitClamp (a + b * (1 - ↑u) ^ 2)

theorem Verification.continuous_quadraticMean (b : ℝ) : Continuous (quadraticMean b)

theorem Verification.quadraticMean_monotone (b : ℝ) : Monotone (quadraticMean b)

theorem Verification.quadraticMean_zero (b : ℝ) (hb : 0 ≤ b) : quadraticMean b (-b) = 0

theorem Verification.quadraticMean_top (b : ℝ) (hb : 0 ≤ b) : quadraticMean b 1 = 1

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

noncomputable def Verification.quadraticIntercept (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : ℝ

Equations

• Verification.quadraticIntercept b hb v = if v = 0 then -b else if v = 1 then 1 else ⋯.choose

theorem Verification.quadraticIntercept_mean (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : quadraticMean b (quadraticIntercept b hb v) = ↑v

theorem Verification.quadraticIntercept_monotone (b : ℝ) (hb : 0 ≤ b) : Monotone (quadraticIntercept b hb)

noncomputable def Verification.quadraticKernel (b : ℝ) (hb : 0 ≤ b) (v u : ↑unitInterval) : ℝ

Equations

• Verification.quadraticKernel b hb v u = Verification.unitClamp (Verification.quadraticIntercept b hb v + b * (1 - ↑u) ^ 2)

theorem Verification.quadraticKernel_integrable (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : MeasureTheory.Integrable (quadraticKernel b hb v) MeasureTheory.volume

theorem Verification.quadraticKernel_monotone (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : Monotone fun (v : ↑unitInterval) => quadraticKernel b hb v u

theorem Verification.quadraticKernel_zero (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : quadraticKernel b hb 0 u = 0

theorem Verification.quadraticKernel_one (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : quadraticKernel b hb 1 u = 1

noncomputable def Verification.quadraticBand (b : ℝ) (hb : 0 ≤ b) : ProbabilityTheory.Copula 2

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

Equations

• Verification.quadraticBand b hb = Verification.copulaOfConditional (Verification.quadraticKernel b hb) ⋯ ⋯ ⋯ ⋯ ⋯

theorem Verification.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 Verification.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 Verification.quadraticBand_isSI (b : ℝ) (hb : 0 ≤ b) : (quadraticBand b hb).IsSI