← Mathematical handbook

noncomputable def Verification.n22Comparison (r t : ℝ) : ℝ

Equations

• Verification.n22Comparison r t = Real.arcsin (1 - (1 - Real.sin t) ^ r)

noncomputable def Verification.n22ComparisonPrime (r t : ℝ) : ℝ

Equations

• Verification.n22ComparisonPrime r t = r * Real.cos t * (1 - Real.sin t) ^ (r - 1) / √(1 - (1 - (1 - Real.sin t) ^ r) ^ 2)

noncomputable def Verification.n22ComparisonSquare (r x : ℝ) : ℝ

Equations

• Verification.n22ComparisonSquare r x = (2 - x) * x ^ (r - 1) / (2 - x ^ r)

theorem Verification.n22ComparisonSquare_deriv {r x : ℝ} (hr : 1 ≤ r) (hx : x ∈ Set.Ioo 0 1) : HasDerivAt (n22ComparisonSquare r) (2 * x ^ (r - 2) * (2 * (r - 1) - r * x + x ^ r) / (2 - x ^ r) ^ 2) x

theorem Verification.n22ComparisonSquare_monotone {r : ℝ} (hr : 1 ≤ r) : MonotoneOn (n22ComparisonSquare r) (Set.Ioo 0 1)

theorem Verification.n22Comparison_deriv {r t : ℝ} (hr : 1 ≤ r) (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : HasDerivAt (n22Comparison r) (n22ComparisonPrime r t) t

theorem Verification.n22ComparisonPrime_sq {r t : ℝ} (hr : 1 ≤ r) (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : n22ComparisonPrime r t ^ 2 = r ^ 2 * n22ComparisonSquare r (1 - Real.sin t)

theorem Verification.n22ComparisonPrime_antitone {r : ℝ} (hr : 1 ≤ r) : AntitoneOn (n22ComparisonPrime r) (Set.Ioo 0 (Real.pi / 2))

theorem Verification.n22Comparison_concave {r : ℝ} (hr : 1 ≤ r) : ConcaveOn ℝ (Set.Icc 0 (Real.pi / 2)) (n22Comparison r)

theorem Verification.n22Comparison_zero (r : ℝ) : n22Comparison r 0 = 0

theorem Verification.n22Comparison_subadd {r s t : ℝ} (hr : 1 ≤ r) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t ≤ Real.pi / 2) : n22Comparison r (s + t) ≤ n22Comparison r s + n22Comparison r t

theorem Verification.n22Comparison_ge {r t : ℝ} (hr : 1 ≤ r) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : t ≤ n22Comparison r t