← Mathematical handbook

noncomputable def Verification.n17PowerBase (a x y : ℝ) : ℝ

Equations

• Verification.n17PowerBase a x y = 1 + (x ^ a - 1) * (y ^ a - 1) / (2 ^ a - 1)

theorem Verification.n17PowerBase_bounds {a x y : ℝ} (ha : 1 ≤ a) (hx : 1 ≤ x) (hy : 1 ≤ y) (hx2 : 2 ≤ x ^ a) (hy2 : 2 ≤ y ^ a) : max 1 (x * y / 2 * 4 ^ (-a⁻¹)) ≤ n17PowerBase a x y ^ a⁻¹ ∧ n17PowerBase a x y ^ a⁻¹ ≤ 4 ^ a⁻¹ * max 1 (x * y / 2)

theorem Verification.nelsen17_tendsto_atBot {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), θ a ≠ 0) (ht : Filter.Tendsto θ l Filter.atBot) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen17 (θ a) ⋯).cdf ![u, v]) l (nhds (max 1 ((1 + ↑u) * (1 + ↑v) / 2) - 1))