← Mathematical handbook

noncomputable def Verification.n16Second (θ t : ℝ) : ℝ

Equations

• Verification.n16Second θ t = 2 * θ / Verification.n16Rad θ t ^ 3

theorem Verification.n16Second_pos {θ t : ℝ} (hθ : 0 < θ) : 0 < n16Second θ t

theorem Verification.n16LogRad_deriv {θ t : ℝ} (hθ : 0 < θ) : HasDerivAt (fun (x : ℝ) => -Real.log (n16Rad θ x)) ((1 - t - θ) / n16Rad θ t ^ 2) t

theorem Verification.n16LogRad_deriv2 {θ t : ℝ} (hθ : 0 < θ) : HasDerivAt (fun (x : ℝ) => (1 - x - θ) / n16Rad θ x ^ 2) (((1 - t - θ) ^ 2 - 4 * θ) / n16Rad θ t ^ 4) t

theorem Verification.n16_density_threshold {θ : ℝ} (hθ : 3 + 2 * √2 ≤ θ) : 1 ≤ θ ∧ 4 * θ ≤ (θ - 1) ^ 2

theorem Verification.n16Second_logconvex {θ : ℝ} (hθ : 3 + 2 * √2 ≤ θ) : ConvexOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (n16Second θ t)