LowModeConvergence.lean

1 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
2 import Mathlib.Analysis.Asymptotics.Defs
3 import Mathlib.Tactic
4 
5 /-! Author: Komorebi P. The printed second-order estimate, with its exact constant. -/
6 namespace KomorebiPaperVI.LowModeConvergence
7 
8 theorem sine_square_error (x : ℝ) :
9     0 ≤ x^2-Real.sin x^2 ∧ x^2-Real.sin x^2 ≤ x^4/3 := by
10   have hlo : 0 ≤ x^2-Real.sin x^2 := sub_nonneg.mpr Real.sin_sq_le_sq
11   have hp : |x+Real.sin x| ≤ 2*|x| :=
12     (abs_add_le _ _).trans (by linarith [Real.abs_sin_le_abs (x := x)])
13   have h := mul_le_mul (Real.abs_sub_sin_le x) hp (abs_nonneg _) (by positivity)
14   rw [← abs_mul] at h
15   have he : (x-Real.sin x)*(x+Real.sin x)=x^2-Real.sin x^2 := by ring
16   rw [he,abs_of_nonneg hlo] at h
17   constructor
18   · exact hlo
19   · calc
20       _ ≤ |x|^3/6*(2*|x|) := h
21       _ = x^4/3 := by rw [show |x|^3/6*(2*|x|)=|x|^4/3 by ring, (show Even (4:ℕ) by decide).pow_abs]
22 
23 noncomputable def eigenvalue (w h : ℝ) : ℝ := 4/h^2*Real.sin (w*h/2)^2
24 
25 theorem low_mode_error (w h : ℝ) (hh : h≠0) :
26     0 ≤ w^2-eigenvalue w h ∧ w^2-eigenvalue w h ≤ w^4/12*h^2 := by
27   have hs := sine_square_error (w*h/2)
28   have hpos : 0 ≤ 4/h^2 := by positivity
29   have he : w^2-eigenvalue w h=4/h^2*((w*h/2)^2-Real.sin (w*h/2)^2) := by
30     unfold eigenvalue
31     field_simp
32     ring
33   rw [he]
34   constructor
35   · exact mul_nonneg hpos hs.1
36   · calc
37       _ ≤ 4/h^2*((w*h/2)^4/3) := mul_le_mul_of_nonneg_left hs.2 hpos
38       _ = w^4/12*h^2 := by field_simp; ring
39 
40 end KomorebiPaperVI.LowModeConvergence

Back to source controls