← Mathematical handbook

theorem Verification.unitOdds_deriv {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (fun (x : ℝ) => x / (1 - x)) ((1 - t) ^ 2)⁻¹ t

theorem Verification.integral_unit_odds (f : ℝ → ℝ) : ∫ (s : ℝ) in Set.Ioi 0, f s = ∫ (t : ℝ) in 0..1, ((1 - t) ^ 2)⁻¹ * f (t / (1 - t))