← Mathematical handbook

theorem Verification.amh_log_quotient_integrable {θ : ℝ} (hθ : θ < 1) : IntervalIntegrable (fun (w : ℝ) => Real.log (1 - θ * w) / w) MeasureTheory.volume 0 1

noncomputable def Verification.amhRhoBoundary (θ w : ℝ) : ℝ

Equations

• Verification.amhRhoBoundary θ w = -Real.log (1 - θ * w) / (θ ^ 2 * w) + (θ - 1 + θ * w) * Real.log (1 - θ * w) / θ ^ 2 - 2 * w / θ

theorem Verification.amhRhoBoundary_deriv (θ w : ℝ) (hθ : θ ≠ 0) (hw : w ≠ 0) (hd : 1 - θ * w ≠ 0) : HasDerivAt (amhRhoBoundary θ) ((1 - w) / (θ * w) + (1 - w) * (1 - θ * w) / (θ * w) ^ 2 * Real.log (1 - θ * w) + (1 + θ) / θ ^ 2 * (Real.log (1 - θ * w) / w)) w

theorem Verification.amhRhoBoundary_tendsto_zero (θ : ℝ) (hθ : θ ≠ 0) : Filter.Tendsto (amhRhoBoundary θ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (1 / θ))

noncomputable def Verification.amhRhoIntegrand (θ w : ℝ) : ℝ

Equations

• Verification.amhRhoIntegrand θ w = (1 - w) / (θ * w) + (1 - w) * (1 - θ * w) / (θ * w) ^ 2 * Real.log (1 - θ * w)

theorem Verification.amhRhoIntegrand_integrable_of_le_one {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (h0 : θ ≠ 0) : IntervalIntegrable (amhRhoIntegrand θ) MeasureTheory.volume 0 1

theorem Verification.amhRhoIntegrand_integrable {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) : IntervalIntegrable (amhRhoIntegrand θ) MeasureTheory.volume 0 1

theorem Verification.amhRhoIntegrand_integral {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) : ∫ (w : ℝ) in 0..1, amhRhoIntegrand θ w = (-(1 + θ) / θ ^ 2 * ∫ (w : ℝ) in 0..1, Real.log (1 - θ * w) / w) - 2 * (1 - θ) * Real.log (1 - θ) / θ ^ 2 - 3 / θ

theorem Verification.amh_spearmanRho_log_integral {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) : (ProbabilityTheory.Copula.amh θ hmin ⋯).spearmanRho = (-12 * (1 + θ) / θ ^ 2 * ∫ (w : ℝ) in 0..1, Real.log (1 - θ * w) / w) - 24 * (1 - θ) * Real.log (1 - θ) / θ ^ 2 - 3 * (θ + 12) / θ

theorem Verification.amh_log_integral_substitution (θ : ℝ) (h0 : θ ≠ 0) : ∫ (w : ℝ) in 0..1, Real.log (1 - θ * w) / w = -∫ (t : ℝ) in 1..1 - θ, Real.log t / (1 - t)

theorem Verification.amh_spearmanRho {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) : (ProbabilityTheory.Copula.amh θ hmin ⋯).spearmanRho = (12 * (1 + θ) * ∫ (t : ℝ) in 1..1 - θ, Real.log t / (1 - t)) / θ ^ 2 - 24 * (1 - θ) * Real.log (1 - θ) / θ ^ 2 - 3 * (θ + 12) / θ