Quadratic bounds on cos

LeanAPAP.lean

@@ -23,7 +23,10 @@ import LeanAPAP.Mathlib.Algebra.Star.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Order
 import LeanAPAP.Mathlib.Algebra.Star.Pi
 import LeanAPAP.Mathlib.Algebra.Star.SelfAdjoint
+import LeanAPAP.Mathlib.Analysis.Calculus.Deriv.Basic
+import LeanAPAP.Mathlib.Analysis.Calculus.MeanValue
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
+import LeanAPAP.Mathlib.Analysis.Convex.Jensen
 import LeanAPAP.Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Mathlib.Analysis.MeanInequalitiesPow
 import LeanAPAP.Mathlib.Analysis.Normed.Field.Basic
@@ -32,6 +35,8 @@ import LeanAPAP.Mathlib.Analysis.NormedSpace.PiLp
 import LeanAPAP.Mathlib.Analysis.NormedSpace.Ray
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Arg
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+import LeanAPAP.Mathlib.Data.Complex.Abs
 import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.Complex.Order
 import LeanAPAP.Mathlib.Data.Finset.Card

LeanAPAP/Mathlib/Analysis/Calculus/Deriv/Basic.lean

@@ -0,0 +1,8 @@
+import Mathlib.Analysis.Calculus.Deriv.Basic
+
+variable {𝕜 F : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  {f f' : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}
+
+lemma deriv_eqOn (hs : IsOpen s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) :
+    s.EqOn (deriv f) f' := fun x hx ↦ by
+  rw [← derivWithin_of_isOpen hs hx, (hf' _ hx).derivWithin $ hs.uniqueDiffWithinAt hx]

LeanAPAP/Mathlib/Analysis/Calculus/MeanValue.lean

@@ -0,0 +1,53 @@
+import Mathlib.Analysis.Calculus.MeanValue
+import LeanAPAP.Mathlib.Analysis.Calculus.Deriv.Basic
+
+-- TODO: Rename `Convex.monotoneOn_of_deriv_nonneg` to `monotoneOn_of_deriv_nonneg`
+-- TODO: Antitone versions, strict versions
+
+/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
+of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
+`f` is a monotone function on `D`. -/
+lemma monotoneOn_of_hasDerivWithinAt_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ}
+    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x)
+    (hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x) : MonotoneOn f D :=
+  hD.monotoneOn_of_deriv_nonneg hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) fun x hx ↦ by
+    rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx
+
+/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
+`f` is a monotone function. -/
+lemma monotone_of_hasDerivAt_nonneg {f f' : ℝ → ℝ} (hf : ∀ x, HasDerivAt f (f' x) x)
+    (hf' : 0 ≤ f') : Monotone f :=
+  monotone_of_deriv_nonneg (fun x ↦ (hf _).differentiableAt) fun x ↦ by
+    rw [(hf _).deriv]; exact hf' _
+
+/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
+interior, and `f''` is nonnegative on the interior, then `f` is convex on `D`. -/
+lemma convexOn_of_hasDerivWithinAt2_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f f' f'' : ℝ → ℝ}
+    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x)
+    (hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x)
+    (hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x) : ConvexOn ℝ D f := by
+  have : (interior D).EqOn (deriv f) f' := deriv_eqOn isOpen_interior hf'
+  refine convexOn_of_deriv2_nonneg hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_
+  · rw [differentiableOn_congr this]
+    exact fun x hx ↦ (hf'' _ hx).differentiableWithinAt
+  · rintro x hx
+    convert hf''₀ _ hx using 1
+    dsimp
+    rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]
+    exact (hf'' _ hy).congr this $ by rw [this hy]
+
+/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
+interior, and `f''` is nonpositive on the interior, then `f` is concave on `D`. -/
+lemma concaveOn_of_hasDerivWithinAt2_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f f' f'' : ℝ → ℝ}
+    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x)
+    (hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x)
+    (hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0) : ConcaveOn ℝ D f := by
+  have : (interior D).EqOn (deriv f) f' := deriv_eqOn isOpen_interior hf'
+  refine concaveOn_of_deriv2_nonpos hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_
+  · rw [differentiableOn_congr this]
+    exact fun x hx ↦ (hf'' _ hx).differentiableWithinAt
+  · rintro x hx
+    convert hf''₀ _ hx using 1
+    dsimp
+    rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]
+    exact (hf'' _ hy).congr this $ by rw [this hy]

LeanAPAP/Mathlib/Analysis/Convex/Jensen.lean

@@ -0,0 +1,35 @@
+import Mathlib.Analysis.Convex.Jensen
+
+open Set
+open scoped Convex
+
+section MaximumPrinciple
+variable {ι 𝕜 E β} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β] [Module 𝕜 E]
+  [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}
+  {x y z : E}
+
+/-- **Maximum principle** for convex functions on a segment. If a function `f` is convex on the
+segment `[x, y]`, then the eventual maximum of `f` on `[x, y]` is at `x` or `y`. -/
+lemma ConvexOn.le_max_of_mem_segment (hf : ConvexOn 𝕜 [x -[𝕜] y] f) (hz : z ∈ [x -[𝕜] y]) :
+    f z ≤ max (f x) (f y) := by
+  rw [← convexHull_pair] at hf hz; simpa using hf.exists_ge_of_mem_convexHull hz
+
+/-- **Minimum principle** for concave functions on a segment. If a function `f` is concave on the
+segment `[x, y]`, then the eventual minimum of `f` on `[x, y]` is at `x` or `y`. -/
+lemma ConcaveOn.min_le_of_mem_segment (hf : ConcaveOn 𝕜 [x -[𝕜] y] f) (hz : z ∈ [x -[𝕜] y]) :
+    min (f x) (f y) ≤ f z := by
+  rw [← convexHull_pair] at hf hz; simpa using hf.exists_le_of_mem_convexHull hz
+
+/-- **Maximum principle** for convex functions on an interval. If a function `f` is convex on the
+interval `[x, y]`, then the eventual maximum of `f` on `[x, y]` is at `x` or `y`. -/
+lemma ConvexOn.le_max_of_mem_Icc {f : 𝕜 → β} {x y z : 𝕜} (hf : ConvexOn 𝕜 (Icc x y) f)
+    (hz : z ∈ Icc x y) : f z ≤ max (f x) (f y) := by
+  rw [← segment_eq_Icc (hz.1.trans hz.2)] at hf hz; exact hf.le_max_of_mem_segment hz
+
+/-- **Minimum principle** for concave functions on an interval. If a function `f` is concave on the
+interval `[x, y]`, then the eventual minimum of `f` on `[x, y]` is at `x` or `y`. -/
+lemma ConcaveOn.min_le_of_mem_Icc {f : 𝕜 → β} {x y z : 𝕜} (hf : ConcaveOn 𝕜 (Icc x y) f)
+    (hz : z ∈ Icc x y) : min (f x) (f y) ≤ f z := by
+  rw [← segment_eq_Icc (hz.1.trans hz.2)] at hf hz; exact hf.min_le_of_mem_segment hz
+
+end MaximumPrinciple

LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

@@ -1,14 +1,26 @@
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
+import LeanAPAP.Mathlib.Data.Complex.Abs
+import LeanAPAP.Mathlib.Data.Complex.Basic
 
 open scoped Real
 
 namespace Complex
-variable {a : ℂ}
-
-@[norm_cast] lemma ofReal_zsmul (n : ℤ) (r : ℝ) : ↑(n • r) = n • (r : ℂ) := by simp
+variable {a x : ℂ}
 
 @[simp] lemma abs_arg_inv (x : ℂ) : |x⁻¹.arg| = |x.arg| := by rw [arg_inv]; split_ifs <;> simp [*]
 
+lemma abs_eq_one_iff' : abs x = 1 ↔ ∃ θ ∈ Set.Ioc (-π) π, exp (θ * I) = x := by
+  rw [abs_eq_one_iff]
+  constructor
+  · rintro ⟨θ, rfl⟩
+    refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
+    · convert toIocMod_mem_Ioc _ _ _
+      ring
+    · rw [eq_sub_of_add_eq $ toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
+      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
+  · rintro ⟨θ, _, rfl⟩
+    exact ⟨θ, rfl⟩
+
 /-- The arclength between two complex numbers is the absolute value of their argument. -/
 noncomputable def arcLength (x y : ℂ) : ℝ := |(x / y).arg|
 

LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

@@ -0,0 +1,78 @@
+import Mathlib.Analysis.Calculus.Deriv.Pow
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+import LeanAPAP.Mathlib.Analysis.Calculus.MeanValue
+import LeanAPAP.Mathlib.Analysis.Convex.Jensen
+
+open Set
+
+namespace Real
+variable {x : ℝ}
+
+lemma hasDerivWithinAt_sin (x : ℝ) (s : Set ℝ) :  HasDerivWithinAt sin (cos x) s x := by
+  simpa using (hasDerivWithinAt_id x s).sin
+
+lemma hasDerivWithinAt_cos (x : ℝ) (s : Set ℝ) :  HasDerivWithinAt cos (-sin x) s x := by
+  simpa using (hasDerivWithinAt_id x s).cos
+
+lemma sin_le (hx : 0 ≤ x) : sin x ≤ x := by
+  suffices : MonotoneOn (fun x ↦ x - sin x) (Ici 0)
+  · simpa using this left_mem_Ici hx hx
+  exact monotoneOn_of_hasDerivWithinAt_nonneg (convex_Ici _) (Continuous.continuousOn $ by
+    continuity) (fun x _ ↦ (hasDerivWithinAt_id ..).sub $ hasDerivWithinAt_sin ..) $ by
+    simp [cos_le_one]
+
+lemma cos_quadratic_lower_bound : 1 - x ^ 2 / 2 ≤ cos x := by
+  wlog hx₀ : 0 ≤ x
+  · simpa using this $ neg_nonneg.2 $ le_of_not_le hx₀
+  suffices : MonotoneOn (fun x ↦ cos x + x ^ 2 / 2) (Ici 0)
+  · simpa using this left_mem_Ici hx₀ hx₀
+  refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Ici _) (Continuous.continuousOn $ by
+    continuity) (fun x _ ↦ (hasDerivWithinAt_cos ..).add $ (hasDerivWithinAt_pow ..).div_const _)
+    fun x hx ↦ ?_
+  simp [mul_div_cancel_left]
+  exact sin_le $ interior_subset hx
+
+/-- **Jordan's inequality**. -/
+lemma two_div_pi_mul_le (hx₀ : 0 ≤ x) (hx : x ≤ π / 2) : 2 / π * x ≤ sin x := by
+  rw [← sub_nonneg]
+  suffices : ConcaveOn ℝ (Icc 0 (π / 2)) (fun x ↦ sin x - 2 / π * x)
+  · refine (le_min ?_ ?_).trans $ this.min_le_of_mem_Icc ⟨hx₀, hx⟩ <;> field_simp
+  refine concaveOn_of_hasDerivWithinAt2_nonpos (convex_Icc ..)
+    (Continuous.continuousOn $ by continuity) (fun x _ ↦ (hasDerivWithinAt_sin ..).sub $ (hasDerivWithinAt_id ..).const_mul (2 / π)) (fun x _ ↦ (hasDerivWithinAt_cos ..).sub_const _)
+    fun x hx ↦ neg_nonpos.2 $ sin_nonneg_of_mem_Icc $ Icc_subset_Icc_right (by linarith) $
+    interior_subset hx
+
+lemma cos_quadratic_upper_bound (hx : |x| ≤ π) : cos x ≤ 1 - 2 / π ^ 2 * x ^ 2 := by
+  wlog hx₀ : 0 ≤ x
+  · simpa using this (by rwa [abs_neg]) $ neg_nonneg.2 $ le_of_not_le hx₀
+  rw [abs_of_nonneg hx₀] at hx
+  -- TODO: `compute_deriv` tactic?
+  have hderiv (x) : HasDerivAt (fun x ↦ 1 - 2 / π ^ 2 * x ^ 2 - cos x) _ x :=
+    (((hasDerivAt_pow ..).const_mul _).const_sub _).sub $ hasDerivAt_cos _
+  simp only [Nat.cast_ofNat, Nat.succ_sub_succ_eq_sub, tsub_zero, pow_one, ← neg_sub', neg_sub,
+    ← mul_assoc] at hderiv
+  have hmono : MonotoneOn (fun x ↦ 1 - 2 / π ^ 2 * x ^ 2 - cos x) (Icc 0 (π / 2))
+  · refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc ..) (Continuous.continuousOn $
+      by continuity) (fun x _ ↦ (hderiv _).hasDerivWithinAt) fun x hx ↦ sub_nonneg.2 ?_
+    have ⟨hx₀, hx⟩ := interior_subset hx
+    calc
+      _ = 2 / π * (2 / π * x) := by ring
+      _ ≤ 1 * sin x := by
+          gcongr; exacts [div_le_one_of_le two_le_pi (by positivity), two_div_pi_mul_le hx₀ hx]
+      _ = sin x := one_mul _
+  have hconc : ConcaveOn ℝ (Icc (π / 2) π) (fun x ↦ 1 - 2 / π ^ 2 * x ^ 2 - cos x)
+  · refine concaveOn_of_hasDerivWithinAt2_nonpos (convex_Icc ..)
+      (Continuous.continuousOn $ by continuity) (fun x _ ↦ (hderiv _).hasDerivWithinAt)
+      (fun x _ ↦ (hasDerivWithinAt_sin ..).sub $ (hasDerivWithinAt_id ..).const_mul _)
+      fun x hx ↦ ?_
+    have ⟨hx, hx'⟩ := interior_subset hx
+    calc
+      _ ≤ (0 : ℝ) - 0 := by
+          gcongr
+          · exact cos_nonpos_of_pi_div_two_le_of_le hx $ hx'.trans $ by linarith
+          · positivity
+      _ = 0 := sub_zero _
+  rw [← sub_nonneg]
+  obtain hx' | hx' := le_total x (π / 2)
+  · simpa using hmono (left_mem_Icc.2 $ by positivity) ⟨hx₀, hx'⟩ hx₀
+  · refine (le_min ?_ ?_).trans $ hconc.min_le_of_mem_Icc ⟨hx', hx⟩ <;> field_simp <;> norm_num

LeanAPAP/Mathlib/Data/Complex/Abs.lean

@@ -0,0 +1,8 @@
+import Mathlib.Data.Complex.Abs
+
+namespace Complex
+
+lemma abs_add_mul_I (x y : ℝ) : abs (x + y * I) = (x ^ 2 + y ^ 2).sqrt := by
+  rw [← normSq_add_mul_I]; rfl
+
+end Complex

LeanAPAP/Mathlib/Data/Complex/Basic.lean

@@ -1,16 +1,11 @@
 import Mathlib.Data.Complex.Basic
 
-/-!
-### TODO
-
-`Complex.ext` lemma is a bad `ext` lemma to have globally.
--/
-
 namespace Complex
 
 attribute [simp] I_ne_zero
 
-@[norm_cast] lemma ofReal'_nsmul (n : ℕ) (r : ℝ) : ofReal' (n • r) = n • ofReal' r := by simp
+@[norm_cast] lemma ofReal_nsmul (n : ℕ) (r : ℝ) : ↑(n • r) = n • (r : ℂ) := by simp
+@[norm_cast] lemma ofReal_zsmul (n : ℤ) (r : ℝ) : ↑(n • r) = n • (r : ℂ) := by simp
 
 lemma re_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).re = z.re *  r := by simp [ofReal']
 lemma im_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).im = z.im *  r := by simp [ofReal']

LeanAPAP/Prereqs/Circle/ArcLength.lean

@@ -1,27 +1,14 @@
 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
 import Mathlib.Analysis.SpecialFunctions.Complex.Log
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Arg
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 
+open Set
 open scoped Real
 
 namespace Complex
 variable {a x y : ℂ}
 
-lemma abs_add_mul_I (x y : ℝ) : abs (x + y * I) = (x ^ 2 + y ^ 2).sqrt := by
-  rw [← normSq_add_mul_I]; rfl
-
-lemma abs_eq_one_iff' : abs x = 1 ↔ ∃ θ ∈ Set.Ioc (-π) π, exp (θ * I) = x := by
-  rw [abs_eq_one_iff]
-  constructor
-  · rintro ⟨θ, rfl⟩
-    refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
-    · convert toIocMod_mem_Ioc _ _ _
-      ring
-    · rw [eq_sub_of_add_eq $ toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
-      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
-  · rintro ⟨θ, _, rfl⟩
-    exact ⟨θ, rfl⟩
-
 /-- Chord-length is always less than arc-length. -/
 lemma norm_sub_le_arcLength (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ‖x - y‖ ≤ arcLength x y := by
   clear a
@@ -39,7 +26,7 @@ lemma norm_sub_le_arcLength (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ‖x - y‖
   rw [norm_eq_abs, abs_add_mul_I, Real.sqrt_le_left (by positivity), ← _root_.abs_pow, abs_sq]
   calc
     _ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq
-    _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; sorry
+    _ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.cos_quadratic_lower_bound
     _ = _ := by ring
   · convert hθ
     ring
@@ -63,7 +50,8 @@ lemma mul_arcLength_le_norm (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : 2 / π * arc
   rw [mul_pow, ← _root_.abs_pow, abs_sq]
   calc
     _ = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) := by ring
-    _ ≤ 2 * (1 - θ.cos) := by gcongr; sorry
+    _ ≤ 2 * (1 - θ.cos) := by
+        gcongr; exact Real.cos_quadratic_upper_bound $ abs_le.2 $ Ioc_subset_Icc_self hθ
     _  = _ := by linear_combination -θ.cos_sq_add_sin_sq
   · convert hθ
     ring