← Mathematical handbook

structure Verification.StableTail : Type

• value : ℝ → ℝ → ℝ
• nonneg {x y : ℝ} : 0 ≤ x → 0 ≤ y → 0 ≤ self.value x y
• zero_left {y : ℝ} : 0 ≤ y → self.value 0 y = y
• zero_right {x : ℝ} : 0 ≤ x → self.value x 0 = x
• mono {x₁ x₂ y₁ y₂ : ℝ} : 0 ≤ x₁ → 0 ≤ y₁ → x₁ ≤ x₂ → y₁ ≤ y₂ → self.value x₁ y₁ ≤ self.value x₂ y₂
• submodular {x₁ x₂ y₁ y₂ : ℝ} : 0 ≤ x₁ → 0 ≤ y₁ → x₁ ≤ x₂ → y₁ ≤ y₂ → self.value x₁ y₁ + self.value x₂ y₂ ≤ self.value x₁ y₂ + self.value x₂ y₁
• homogeneous {x y c : ℝ} : 0 ≤ x → 0 ≤ y → 0 ≤ c → self.value (c * x) (c * y) = c * self.value x y

noncomputable def Verification.spectralStableTail {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (hXi : MeasureTheory.Integrable X μ) (hYi : MeasureTheory.Integrable Y μ) (hX : ∀ (ω : Ω), 0 ≤ X ω) (hY : ∀ (ω : Ω), 0 ≤ Y ω) (hXm : ∫ (ω : Ω), X ω ∂μ = 1) (hYm : ∫ (ω : Ω), Y ω ∂μ = 1) : StableTail

Equations

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

theorem Verification.StableTail.exp_rectangle (L : StableTail) {x₁ x₂ y₁ y₂ : ℝ} (hx : 0 ≤ x₁) (hy : 0 ≤ y₁) (hxx : x₁ ≤ x₂) (hyy : y₁ ≤ y₂) : 0 ≤ Real.exp (-L.value x₁ y₁) - Real.exp (-L.value x₁ y₂) - Real.exp (-L.value x₂ y₁) + Real.exp (-L.value x₂ y₂)

noncomputable def Verification.stableTailCDF (L : StableTail) (u v : ↑unitInterval) : ℝ

Equations

• Verification.stableTailCDF L u v = if u = 0 ∨ v = 0 then 0 else Real.exp (-L.value (-Real.log ↑u) (-Real.log ↑v))

theorem Verification.stableTailCDF_zero_left (L : StableTail) (v : ↑unitInterval) : stableTailCDF L 0 v = 0

theorem Verification.stableTailCDF_zero_right (L : StableTail) (u : ↑unitInterval) : stableTailCDF L u 0 = 0

theorem Verification.stableTailCDF_nonneg (L : StableTail) (u v : ↑unitInterval) : 0 ≤ stableTailCDF L u v

theorem Verification.stableTailCDF_positive_coords (L : StableTail) (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : stableTailCDF L u v = Real.exp (-L.value (-Real.log ↑u) (-Real.log ↑v))

theorem Verification.stableTailCDF_one_left (L : StableTail) (v : ↑unitInterval) : stableTailCDF L 1 v = ↑v

theorem Verification.stableTailCDF_one_right (L : StableTail) (u : ↑unitInterval) : stableTailCDF L u 1 = ↑u

theorem Verification.stableTailCDF_mono (L : StableTail) (u v u' v' : ↑unitInterval) (hu : u ≤ u') (hv : v ≤ v') : stableTailCDF L u v ≤ stableTailCDF L u' v'

theorem Verification.stableTailCDF_rectangle (L : StableTail) (a b c d : ↑unitInterval) (hab : a ≤ b) (hcd : c ≤ d) : 0 ≤ stableTailCDF L b d - stableTailCDF L a d - stableTailCDF L b c + stableTailCDF L a c

theorem Verification.stableTailCDF_isClassical (L : StableTail) : ProbabilityTheory.Copula.IsClassical fun (u : Fin 2 → ↑unitInterval) => stableTailCDF L (u 0) (u 1)

noncomputable def Verification.stableTailCopula (L : StableTail) : ProbabilityTheory.Copula 2

Equations

• Verification.stableTailCopula L = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => Verification.stableTailCDF L (u 0) (u 1)) ⋯

theorem Verification.stableTailCopula_cdf (L : StableTail) (u v : ↑unitInterval) : (stableTailCopula L).cdf ![u, v] = stableTailCDF L u v