← Mathematical handbook

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

Equations

• Verification.n18Core θ t = 1 + θ / Real.log t

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

Equations

• Verification.n18CorePrime θ t = -θ / (t * Real.log t ^ 2)

theorem Verification.n18_log_bound {θ t : ℝ} (ht : 0 < t) (hb : t ≤ Real.exp (-θ)) : Real.log t ≤ -θ

theorem Verification.n18Core_deriv {θ t : ℝ} (hθ : 0 < θ) (ht : 0 < t) (hb : t ≤ Real.exp (-θ)) : HasDerivAt (n18Core θ) (n18CorePrime θ t) t

theorem Verification.n18Core_deriv2 {θ t : ℝ} (hθ : 0 < θ) (ht : 0 < t) (hb : t ≤ Real.exp (-θ)) : HasDerivAt (n18CorePrime θ) (θ * (Real.log t + 2) / (t ^ 2 * Real.log t ^ 3)) t

theorem Verification.n18Core_continuousAt_zero (θ : ℝ) : ContinuousAt (n18Core θ) 0

theorem Verification.n18Core_continuousOn {θ : ℝ} (hθ : 0 < θ) : ContinuousOn (n18Core θ) (Set.Icc 0 (Real.exp (-θ)))

theorem Verification.n18Core_antitone {θ : ℝ} (hθ : 0 < θ) : AntitoneOn (n18Core θ) (Set.Icc 0 (Real.exp (-θ)))

theorem Verification.n18Core_convex {θ : ℝ} (hθ : 2 ≤ θ) : ConvexOn ℝ (Set.Icc 0 (Real.exp (-θ))) (n18Core θ)

theorem Verification.n18Core_cutoff {θ : ℝ} (hθ : θ ≠ 0) : n18Core θ (Real.exp (-θ)) = 0

theorem Verification.n18Core_nonneg {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Icc 0 (Real.exp (-θ))) : 0 ≤ n18Core θ t