RationalSqrtEnclosure.lean

1 import Mathlib.Data.Nat.Sqrt
2 import Mathlib.Algebra.Order.Floor.Ring
3 import Mathlib.Data.Rat.Floor
4 import Mathlib.Analysis.SpecialFunctions.Sqrt
5 import Mathlib.Tactic
6 
7 /-! P84: the least integer square-root ceiling and exact rational grid
8 enclosures are computed with integer square root and a final rational test. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.RationalSqrtEnclosure
11 
12 def integerUpperSqrt (x : ℚ) : ℕ :=
13   let m := Nat.sqrt ⌊x⌋₊
14   if x≤(m : ℚ)^2 then m else m+1
15 
16 theorem floor_sqrt_bounds (x : ℚ) (hx : 0≤x) :
17     ((Nat.sqrt ⌊x⌋₊ : ℕ) : ℚ)^2≤x ∧ x<(((Nat.sqrt ⌊x⌋₊ : ℕ) : ℚ)+1)^2 := by
18   have hlow : ((Nat.sqrt ⌊x⌋₊ : ℕ) : ℚ)^2≤(⌊x⌋₊ : ℚ) := by
19     exact_mod_cast Nat.sqrt_le' ⌊x⌋₊
20   have hu : (⌊x⌋₊ : ℚ)+1≤(((Nat.sqrt ⌊x⌋₊ : ℕ) : ℚ)+1)^2 := by
21     exact_mod_cast Nat.succ_le_iff.mpr (Nat.lt_succ_sqrt' ⌊x⌋₊)
22   exact ⟨hlow.trans (Nat.floor_le hx),(Nat.lt_floor_add_one x).trans_le hu⟩
23 
24 theorem integerUpperSqrt_correct (x : ℚ) (hx : 0≤x) : x≤(integerUpperSqrt x : ℚ)^2 := by
25   dsimp only [integerUpperSqrt]
26   split_ifs with h
27   · exact h
28   · simpa only [Nat.cast_add,Nat.cast_one] using (floor_sqrt_bounds x hx).2.le
29 
30 theorem integerUpperSqrt_minimal (x : ℚ) (hx : 0≤x) (j : ℕ) (hj : x≤(j : ℚ)^2) :
31     integerUpperSqrt x≤j := by
32   dsimp only [integerUpperSqrt]
33   split_ifs with h
34   · have hs : ((Nat.sqrt ⌊x⌋₊ : ℕ) : ℚ)^2≤(j : ℚ)^2 := (floor_sqrt_bounds x hx).1.trans hj
35     have hn : ((Nat.sqrt ⌊x⌋₊ : ℕ) : ℚ)≤(j : ℚ) :=
36       (sq_le_sq₀ (by positivity) (by positivity)).mp hs
37     exact_mod_cast hn
38   · have hn : ((Nat.sqrt ⌊x⌋₊ : ℕ) : ℚ)<(j : ℚ) := by
39       have hm : ((Nat.sqrt ⌊x⌋₊ : ℕ) : ℚ)^2<x := lt_of_not_ge h
40       exact (sq_lt_sq₀ (by positivity) (by positivity)).mp (hm.trans_le hj)
41     have hnat : Nat.sqrt ⌊x⌋₊<j := by exact_mod_cast hn
42     exact hnat
43 
44 def upperSqrt (denominator : ℕ) (x : ℚ) : ℚ :=
45   (integerUpperSqrt (x*(denominator : ℚ)^2) : ℚ)/(denominator : ℚ)
46 
47 theorem upperSqrt_nonneg (denominator : ℕ) (x : ℚ) : 0≤upperSqrt denominator x := by
48   exact div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _)
49 
50 /-- The rational upper endpoint is a true square-root enclosure. -/
51 theorem upperSqrt_squared (denominator : ℕ) (hd : 0<denominator) (x : ℚ) (hx : 0≤x) :
52     x≤(upperSqrt denominator x)^2 := by
53   have hdq : (0 : ℚ)<denominator := by exact_mod_cast hd
54   have h := integerUpperSqrt_correct (x*(denominator : ℚ)^2) (mul_nonneg hx (sq_nonneg _))
55   rw [upperSqrt,div_pow]
56   exact (le_div_iff₀ (sq_pos_of_pos hdq)).mpr h
57 
58 theorem sqrt_le_upperSqrt (denominator : ℕ) (hd : 0<denominator) (x : ℚ) (hx : 0≤x) :
59     Real.sqrt (x : ℝ)≤(upperSqrt denominator x : ℝ) := by
60   have hsq : (x : ℝ)≤(upperSqrt denominator x : ℝ)^2 := by
61     exact_mod_cast upperSqrt_squared denominator hd x hx
62   have hn : (0 : ℝ)≤upperSqrt denominator x := by exact_mod_cast upperSqrt_nonneg denominator x
63   have hxr : (0 : ℝ)≤x := by exact_mod_cast hx
64   nlinarith [Real.sq_sqrt hxr,Real.sqrt_nonneg (x : ℝ)]
65 
66 /-- This is the smallest rational grid numerator meeting the exact final comparison. -/
67 theorem upperSqrt_le_grid (denominator : ℕ) (hd : 0<denominator) (x : ℚ) (hx : 0≤x)
68     (j : ℕ) (hj : x≤((j : ℚ)/(denominator : ℚ))^2) :
69     upperSqrt denominator x≤(j : ℚ)/(denominator : ℚ) := by
70   have hdq : (0 : ℚ)<denominator := by exact_mod_cast hd
71   have hs : x*(denominator : ℚ)^2≤(j : ℚ)^2 := by
72     rw [div_pow] at hj
73     exact (le_div_iff₀ (sq_pos_of_pos hdq)).mp hj
74   have hm := integerUpperSqrt_minimal (x*(denominator : ℚ)^2) (mul_nonneg hx (sq_nonneg _)) j hs
75   apply div_le_div_of_nonneg_right _ hdq.le
76   exact_mod_cast hm
77 
78 /-- An exact mathematical enclosure on real input; on rational input the
79 integer-square-root implementation below gives exactly the same numerator. -/
80 noncomputable def realUpperSqrt (denominator : ℕ) (x : ℝ) : ℚ :=
81   (⌈(denominator : ℝ)*Real.sqrt x⌉₊ : ℚ)/(denominator : ℚ)
82 
83 theorem realUpperSqrt_nonneg (denominator : ℕ) (x : ℝ) : 0≤realUpperSqrt denominator x := by
84   exact div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _)
85 
86 theorem sqrt_le_realUpperSqrt (denominator : ℕ) (hd : 0<denominator) (x : ℝ) :
87     Real.sqrt x≤(realUpperSqrt denominator x : ℝ) := by
88   have hdr : (0 : ℝ)<denominator := by exact_mod_cast hd
89   unfold realUpperSqrt
90   push_cast
91   exact (le_div_iff₀ hdr).mpr (by simpa only [mul_comm] using Nat.le_ceil ((denominator : ℝ)*Real.sqrt x))
92 
93 theorem realUpperSqrt_rat (denominator : ℕ) (hd : 0<denominator) (x : ℚ) (hx : 0≤x) :
94     realUpperSqrt denominator (x : ℝ)=upperSqrt denominator x := by
95   have hdr : (0 : ℝ)<denominator := by exact_mod_cast hd
96   have hxr : (0 : ℝ)≤x := by exact_mod_cast hx
97   have he : ⌈(denominator : ℝ)*Real.sqrt (x : ℝ)⌉₊=
98       integerUpperSqrt (x*(denominator : ℚ)^2) := by
99     apply le_antisymm
100     · apply Nat.ceil_le.mpr
101       have h := sqrt_le_upperSqrt denominator hd x hx
102       dsimp only [upperSqrt] at h
103       push_cast at h
104       simpa only [mul_comm] using (le_div_iff₀ hdr).mp h
105     · apply integerUpperSqrt_minimal _ (mul_nonneg hx (sq_nonneg _))
106       have hc := Nat.le_ceil ((denominator : ℝ)*Real.sqrt (x : ℝ))
107       have hs : (x : ℝ)*(denominator : ℝ)^2≤
108           (⌈(denominator : ℝ)*Real.sqrt (x : ℝ)⌉₊ : ℝ)^2 := by
109         have hsq := pow_le_pow_left₀ (mul_nonneg hdr.le (Real.sqrt_nonneg (x : ℝ))) hc 2
110         rw [mul_pow,Real.sq_sqrt hxr] at hsq
111         simpa only [mul_comm] using hsq
112       exact_mod_cast hs
113   simp only [realUpperSqrt,upperSqrt,he]
114 
115 end Komorebi.LSM.RationalSqrtEnclosure

Back to source controls