← Mathematical handbook

noncomputable def Verification.extremeValuePowerCDF (C : ProbabilityTheory.Copula 2) (θ : ℝ) (u v : ↑unitInterval) : ℝ

Equations

• Verification.extremeValuePowerCDF C θ u v = if u = 0 ∨ v = 0 then 0 else Real.exp (-Verification.extremeValuePowerLog C θ (-Real.log ↑u) (-Real.log ↑v) ⋯ ⋯)

theorem Verification.extremeValuePowerCDF_zero_left (C : ProbabilityTheory.Copula 2) (θ : ℝ) (v : ↑unitInterval) : extremeValuePowerCDF C θ 0 v = 0

theorem Verification.extremeValuePowerCDF_zero_right (C : ProbabilityTheory.Copula 2) (θ : ℝ) (u : ↑unitInterval) : extremeValuePowerCDF C θ u 0 = 0

theorem Verification.extremeValuePowerCDF_nonneg (C : ProbabilityTheory.Copula 2) (θ : ℝ) (u v : ↑unitInterval) : 0 ≤ extremeValuePowerCDF C θ u v

theorem Verification.extremeValuePowerCDF_positive_coords (C : ProbabilityTheory.Copula 2) (θ : ℝ) (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : extremeValuePowerCDF C θ u v = Real.exp (-extremeValuePowerLog C θ (-Real.log ↑u) (-Real.log ↑v) ⋯ ⋯)

theorem Verification.extremeValuePowerLog_zero_left (C : ProbabilityTheory.Copula 2) (θ : ℝ) (hθ : 0 < θ) (y : ℝ) (hy : 0 ≤ y) : extremeValuePowerLog C θ 0 y ⋯ hy = y

theorem Verification.extremeValuePowerLog_zero_right (C : ProbabilityTheory.Copula 2) (θ : ℝ) (hθ : 0 < θ) (x : ℝ) (hx : 0 ≤ x) : extremeValuePowerLog C θ x 0 hx ⋯ = x

theorem Verification.extremeValuePowerCDF_one_left (C : ProbabilityTheory.Copula 2) (θ : ℝ) (hθ : 0 < θ) (v : ↑unitInterval) : extremeValuePowerCDF C θ 1 v = ↑v

theorem Verification.extremeValuePowerCDF_one_right (C : ProbabilityTheory.Copula 2) (θ : ℝ) (hθ : 0 < θ) (u : ↑unitInterval) : extremeValuePowerCDF C θ u 1 = ↑u

theorem Verification.extremeValuePowerCDF_mono (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (θ : ℝ) (hθ : 1 ≤ θ) (u v u' v' : ↑unitInterval) (hu : u ≤ u') (hv : v ≤ v') : extremeValuePowerCDF C θ u v ≤ extremeValuePowerCDF C θ u' v'

theorem Verification.extremeValuePowerCDF_rectangle (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (θ : ℝ) (hθ : 1 ≤ θ) (a b c d : ↑unitInterval) (hab : a ≤ b) (hcd : c ≤ d) : 0 ≤ extremeValuePowerCDF C θ b d - extremeValuePowerCDF C θ a d - extremeValuePowerCDF C θ b c + extremeValuePowerCDF C θ a c

theorem Verification.extremeValuePowerCDF_isClassical (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (θ : ℝ) (hθ : 1 ≤ θ) : ProbabilityTheory.Copula.IsClassical fun (u : Fin 2 → ↑unitInterval) => extremeValuePowerCDF C θ (u 0) (u 1)

noncomputable def Verification.extremeValuePower (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (θ : ℝ) (hθ : 1 ≤ θ) : ProbabilityTheory.Copula 2

Equations

• Verification.extremeValuePower C hC θ hθ = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => Verification.extremeValuePowerCDF C θ (u 0) (u 1)) ⋯

theorem Verification.extremeValuePower_cdf (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (extremeValuePower C hC θ hθ).cdf ![u, v] = extremeValuePowerCDF C θ u v