← Mathematical handbook

noncomputable def Verification.n13A (u : ℝ) : ℝ

Equations

• Verification.n13A u = 1 - Real.log u

noncomputable def Verification.n13B (θ k u : ℝ) : ℝ

Equations

• Verification.n13B θ k u = Verification.n13A u ^ θ + k

noncomputable def Verification.n13Section (θ k u : ℝ) : ℝ

Equations

• Verification.n13Section θ k u = Real.exp (1 - Verification.n13B θ k u ^ θ⁻¹)

noncomputable def Verification.n13Factor (θ k u : ℝ) : ℝ

Equations

• Verification.n13Factor θ k u = Verification.n13A u ^ θ / Verification.n13A u * Verification.n13B θ k u ^ θ⁻¹ / Verification.n13B θ k u

noncomputable def Verification.n13SectionDeriv (θ k u : ℝ) : ℝ

Equations

• Verification.n13SectionDeriv θ k u = Verification.n13Section θ k u / u * Verification.n13Factor θ k u

theorem Verification.n13Section_deriv {θ k u : ℝ} (hθ : θ ≠ 0) (hu : 0 < u) (ha : 0 < n13A u) (hb : 0 < n13B θ k u) : HasDerivAt (n13Section θ k) (n13SectionDeriv θ k u) u

theorem Verification.n13Section_deriv2 {θ k u : ℝ} (hθ : θ ≠ 0) (hu : 0 < u) (ha : 0 < n13A u) (hb : 0 < n13B θ k u) : HasDerivAt (n13SectionDeriv θ k) (n13SectionDeriv θ k u / u * (n13Factor θ k u - 1 - (θ - 1) / n13A u + (θ - 1) * n13A u ^ θ / n13A u / n13B θ k u)) u

theorem Verification.n13Factor_le_one {θ k u : ℝ} (hθ : 1 ≤ θ) (hk : 0 ≤ k) (ha : 0 < n13A u) : n13Factor θ k u ≤ 1

theorem Verification.n13Section_deriv2_nonpos {θ k u : ℝ} (hθ : 1 ≤ θ) (hk : 0 ≤ k) (hu : 0 < u) (ha : 0 < n13A u) : n13SectionDeriv θ k u / u * (n13Factor θ k u - 1 - (θ - 1) / n13A u + (θ - 1) * n13A u ^ θ / n13A u / n13B θ k u) ≤ 0