← Mathematical handbook

theorem Verification.n13_powerRoot_bounds (p a b : ℝ) (hp : 0 < p) (ha : 1 ≤ a) (hb : 1 ≤ b) : max a b ≤ (a ^ p + b ^ p - 1) ^ p⁻¹ ∧ (a ^ p + b ^ p - 1) ^ p⁻¹ ≤ 2 ^ p⁻¹ * max a b

theorem Verification.nelsen13_tendsto_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), 0 ≤ θ z) (hlim : Filter.Tendsto θ l Filter.atTop) (u v : ↑unitInterval) : Filter.Tendsto (fun (z : α) => (nelsen13 (θ z) ⋯).cdf ![u, v]) l (nhds (min ↑u ↑v))