← Mathematical handbook

theorem Verification.amh_log_quotient_integrable_one : IntervalIntegrable (fun (w : ℝ) => Real.log (1 - w) / w) MeasureTheory.volume 0 1

theorem Verification.amhRhoBoundary_tendsto_one : Filter.Tendsto (amhRhoBoundary 1) (nhdsWithin 1 (Set.Iio 1)) (nhds (-2))

theorem Verification.amhRhoIntegrand_integral_one : ∫ (w : ℝ) in 0..1, amhRhoIntegrand 1 w = (-2 * ∫ (w : ℝ) in 0..1, Real.log (1 - w) / w) - 3

theorem Verification.amh_spearmanRho_one : (ProbabilityTheory.Copula.amh 1 ⋯ ⋯).spearmanRho = (24 * ∫ (t : ℝ) in 1..0, Real.log t / (1 - t)) - 39

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