theorem
Papers.AnsariRockel2024.bb5_exponent_eq_power_log
(θ δ x y : ℝ)
(hδ : 0 < δ)
(hx : 0 < x)
(hy : 0 < y)
:
Verification.bb5TailKernel θ δ x y = Verification.extremeValuePowerLog (Verification.galambos δ hδ) θ x y ⋯ ⋯
theorem
Papers.AnsariRockel2024.bb5_exponent_submodular
(θ δ : ℝ)
(hθ : 1 ≤ θ)
(hδ : 0 < δ)
{x₁ x₂ y₁ y₂ : ℝ}
(hx : 0 < x₁)
(hy : 0 < y₁)
(hxx : x₁ ≤ x₂)
(hyy : y₁ ≤ y₂)
:
Verification.bb5TailKernel θ δ x₁ y₁ + Verification.bb5TailKernel θ δ x₂ y₂ ≤ Verification.bb5TailKernel θ δ x₁ y₂ + Verification.bb5TailKernel θ δ x₂ y₁