← Mathematical handbook

noncomputable def Verification.rafteryKernel (a : ℝ) (u t : ↑unitInterval) : ℝ

CDF of a power distribution supported on [0,t]. Its value at t=0 is irrelevant to integration.

Equations

• Verification.rafteryKernel a u t = if t ≤ u then 1 else (↑u / ↑t) ^ a

theorem Verification.rafteryKernel_nonneg (a : ℝ) (u t : ↑unitInterval) : 0 ≤ rafteryKernel a u t

theorem Verification.rafteryKernel_le_one {a : ℝ} (ha : 0 ≤ a) (u t : ↑unitInterval) : rafteryKernel a u t ≤ 1

theorem Verification.rafteryKernel_monotone {a : ℝ} (ha : 0 ≤ a) (t : ↑unitInterval) : Monotone fun (u : ↑unitInterval) => rafteryKernel a u t

theorem Verification.rafteryKernel_measurable (a : ℝ) (u : ↑unitInterval) : Measurable (rafteryKernel a u)

theorem Verification.rafteryKernel_integrable {a : ℝ} (ha : 0 ≤ a) (u : ↑unitInterval) : MeasureTheory.Integrable (rafteryKernel a u) MeasureTheory.volume

theorem Verification.rafteryKernel_product_integrable {a : ℝ} (ha : 0 ≤ a) (u v : ↑unitInterval) : MeasureTheory.Integrable (fun (t : ↑unitInterval) => rafteryKernel a u t * rafteryKernel a v t) MeasureTheory.volume

theorem Verification.rafteryKernel_zero_ae {a : ℝ} (ha : 0 < a) : rafteryKernel a 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0

theorem Verification.integral_rafteryKernel {a : ℝ} (ha : 1 < a) (u : ↑unitInterval) : ∫ (t : ↑unitInterval), rafteryKernel a u t = (a * ↑u - ↑u ^ a) / (a - 1)

noncomputable def Verification.rafteryMixtureCDF (a : ℝ) (u v : ↑unitInterval) : ℝ

Equations

• Verification.rafteryMixtureCDF a u v = ↑u ^ a * ↑v ^ a / a + (a - 1) / a * ∫ (t : ↑unitInterval), Verification.rafteryKernel a u t * Verification.rafteryKernel a v t

theorem Verification.rafteryMixtureCDF_symm (a : ℝ) (u v : ↑unitInterval) : rafteryMixtureCDF a u v = rafteryMixtureCDF a v u

theorem Verification.rafteryMixtureCDF_zero {a : ℝ} (ha : 1 < a) (v : ↑unitInterval) : rafteryMixtureCDF a 0 v = 0

theorem Verification.rafteryMixtureCDF_one {a : ℝ} (ha : 1 < a) (u : ↑unitInterval) : rafteryMixtureCDF a u 1 = ↑u

theorem Verification.rafteryMixtureCDF_rectangle {a : ℝ} (ha : 1 < a) (u₁ u₂ v₁ v₂ : ↑unitInterval) (hu : u₁ ≤ u₂) (hv : v₁ ≤ v₂) : 0 ≤ rafteryMixtureCDF a u₂ v₂ - rafteryMixtureCDF a u₁ v₂ - rafteryMixtureCDF a u₂ v₁ + rafteryMixtureCDF a u₁ v₁

theorem Verification.rafteryMixture_isClassical {a : ℝ} (ha : 1 < a) : ProbabilityTheory.Copula.IsClassical fun (x : Fin 2 → ↑unitInterval) => rafteryMixtureCDF a (x 0) (x 1)

noncomputable def Verification.rafteryPower (a : ℝ) (ha : 1 < a) : ProbabilityTheory.Copula 2

Equations

• Verification.rafteryPower a ha = ProbabilityTheory.Copula.ofClassical (fun (x : Fin 2 → ↑unitInterval) => Verification.rafteryMixtureCDF a (x 0) (x 1)) ⋯

theorem Verification.rafteryPower_cdf {a : ℝ} (ha : 1 < a) (u v : ↑unitInterval) : (rafteryPower a ha).cdf ![u, v] = rafteryMixtureCDF a u v

theorem Verification.rafteryMixtureCDF_of_le {a : ℝ} (ha : 1 < a) (u v : ↑unitInterval) (huv : u ≤ v) : rafteryMixtureCDF a u v = ↑u + ↑u ^ a * (↑v ^ a - ↑v ^ (1 - a)) / (2 * a - 1)