LowModeConvergence.lean

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

Back to source controls