← Mathematical handbook

noncomputable def Verification.bb5InteriorCDF (θ δ u v : ℝ) : ℝ

Equations

• Verification.bb5InteriorCDF θ δ u v = Real.exp (-Verification.bb5TailKernel θ δ (-Real.log u) (-Real.log v))

theorem Papers.AnsariRockel2024.bb5_exponent_exp_rectangle (θ δ : ℝ) (hθ : 1 ≤ θ) (hδ : 0 < δ) {x₁ x₂ y₁ y₂ : ℝ} (hx : 0 < x₁) (hy : 0 < y₁) (hxx : x₁ ≤ x₂) (hyy : y₁ ≤ y₂) : 0 ≤ Real.exp (-Verification.bb5TailKernel θ δ x₁ y₁) - Real.exp (-Verification.bb5TailKernel θ δ x₁ y₂) - Real.exp (-Verification.bb5TailKernel θ δ x₂ y₁) + Real.exp (-Verification.bb5TailKernel θ δ x₂ y₂)

theorem Papers.AnsariRockel2024.bb5_interior_rectangle_nonneg (θ δ : ℝ) (hθ : 1 ≤ θ) (hδ : 0 < δ) {a b c d : ℝ} (ha : 0 < a) (hab : a ≤ b) (hb : b < 1) (hc : 0 < c) (hcd : c ≤ d) (hd : d < 1) : 0 ≤ Verification.bb5InteriorCDF θ δ b d - Verification.bb5InteriorCDF θ δ a d - Verification.bb5InteriorCDF θ δ b c + Verification.bb5InteriorCDF θ δ a c