← Mathematical handbook

noncomputable def Verification.n22Prime (p t : ℝ) : ℝ

Equations

• Verification.n22Prime p t = if t < Real.pi / 2 then -p * Real.cos t * (1 - Real.sin t) ^ (p - 1) else 0

theorem Verification.n22Base_deriv_cutoff : HasDerivAt n22Base 0 (Real.pi / 2)

theorem Verification.n22Psi_deriv (p : ℝ) (hp : 1 ≤ p) (t : ℝ) : HasDerivAt (fun (x : ℝ) => n22Base x ^ p) (n22Prime p t) t

theorem Verification.n22_trig_pos {t : ℝ} (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : 0 < Real.cos t ∧ 0 < 1 - Real.sin t

theorem Verification.n22_log_cos_deriv {t : ℝ} (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : HasDerivAt (fun (x : ℝ) => Real.log (Real.cos x)) (-Real.sin t / Real.cos t) t

theorem Verification.n22_log_cos_deriv2 {t : ℝ} (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : HasDerivAt (fun (x : ℝ) => -Real.sin x / Real.cos x) (-1 / Real.cos t ^ 2) t

theorem Verification.n22_log_base_deriv {t : ℝ} (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : HasDerivAt (fun (x : ℝ) => Real.log (1 - Real.sin x)) (-Real.cos t / (1 - Real.sin t)) t

theorem Verification.n22_log_base_deriv2 {t : ℝ} (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : HasDerivAt (fun (x : ℝ) => -Real.cos x / (1 - Real.sin x)) (-1 / (1 - Real.sin t)) t

theorem Verification.n22_log_cos_concave : ConcaveOn ℝ (Set.Ioo 0 (Real.pi / 2)) fun (x : ℝ) => Real.log (Real.cos x)

theorem Verification.n22_log_base_concave : ConcaveOn ℝ (Set.Ioo 0 (Real.pi / 2)) fun (x : ℝ) => Real.log (1 - Real.sin x)

theorem Verification.n22Prime_neg {p t : ℝ} (hp : 1 ≤ p) (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : n22Prime p t < 0

theorem Verification.n22Prime_log {p t : ℝ} (hp : 1 ≤ p) (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : Real.log (-n22Prime p t) = Real.log (Real.cos t) + (p - 1) * Real.log (1 - Real.sin t) + Real.log p

theorem Verification.n22Prime_log_concave {p : ℝ} (hp : 1 ≤ p) : ConcaveOn ℝ (Set.Ioo 0 (Real.pi / 2)) fun (t : ℝ) => Real.log (-n22Prime p t)