RationalConfidenceArithmetic.lean

1 import KomorebiLSM.RationalSqrtEnclosure
2 import Mathlib.Analysis.SpecialFunctions.Log.Basic
3 import Mathlib.Analysis.Complex.Exponential
4 import Mathlib.Data.Nat.Log
5 
6 /-! P84's logarithms are bounded by integer dyadic ceilings before any
7 rational confidence arithmetic or endpoint rounding is performed. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.RationalConfidenceArithmetic
10 open RationalSqrtEnclosure
11 
12 theorem log_two_lt_seven_tenths : Real.log 2<(7/10 : ℝ) := by
13   have hs := Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ)≤7/10) 5
14   norm_num [Finset.sum_range_succ] at hs
15   have he : (2 : ℝ)<Real.exp (7/10) := by linarith
16   exact (Real.log_lt_iff_lt_exp (by norm_num : (0 : ℝ)<2)).mpr he
17 
18 /-- This is literally the ceiling of the real base-two logarithm. -/
19 noncomputable def ceilLog2 (x : ℝ) : ℤ := ⌈Real.log x/Real.log 2⌉
20 
21 theorem ceilLog2_nonneg (x : ℝ) (hx : 1≤x) : 0≤ceilLog2 x := by
22   apply Int.ceil_nonneg
23   exact div_nonneg (Real.log_nonneg hx) (Real.log_nonneg (by norm_num))
24 
25 theorem log_le_ceilLog2 (x : ℝ) : Real.log x≤(ceilLog2 x : ℝ)*Real.log 2 := by
26   exact (div_le_iff₀ (Real.log_pos (by norm_num : (1 : ℝ)<2))).mp (Int.le_ceil _)
27 
28 /-- The dyadic exponent is computed entirely from rational ceiling and integer clog. -/
29 def rationalCeilLog2 (x : ℚ) : ℕ := Nat.clog 2 ⌈x⌉₊
30 
31 theorem rationalCeilLog2_le_iff (x : ℚ) (n : ℕ) :
32     rationalCeilLog2 x≤n ↔ x≤(2 : ℚ)^n := by
33   rw [rationalCeilLog2,Nat.clog_le_iff_le_pow (by norm_num : 1<(2 : ℕ)),Nat.ceil_le]
34   norm_cast
35 
36 theorem ceilLog2_le_nat_iff (x : ℝ) (hx : 0<x) (n : ℕ) :
37     ceilLog2 x≤(n : ℤ) ↔ x≤(2 : ℝ)^n := by
38   rw [ceilLog2,Int.ceil_le,div_le_iff₀ (Real.log_pos (by norm_num : (1 : ℝ)<2)),Int.cast_natCast,
39     ← Real.log_pow]
40   exact Real.log_le_log_iff hx (pow_pos (by norm_num) _)
41 
42 /-- The exact integer algorithm agrees with the mathematical log ceiling. -/
43 theorem rationalCeilLog2_eq (x : ℚ) (hx : 1≤x) :
44     (rationalCeilLog2 x : ℤ)=ceilLog2 (x : ℝ) := by
45   have hxr : (1 : ℝ)≤x := by exact_mod_cast hx
46   have hxp : (0 : ℝ)<x := by linarith
47   have hz : 0≤ceilLog2 (x : ℝ) := ceilLog2_nonneg _ hxr
48   apply le_antisymm
49   · have hcast : (((ceilLog2 (x : ℝ)).toNat : ℕ) : ℤ)=ceilLog2 (x : ℝ) := Int.toNat_of_nonneg hz
50     have hpowr : (x : ℝ)≤(2 : ℝ)^((ceilLog2 (x : ℝ)).toNat) :=
51       (ceilLog2_le_nat_iff _ hxp _).mp (by rw [hcast])
52     have hpowq : x≤(2 : ℚ)^((ceilLog2 (x : ℝ)).toNat) := by exact_mod_cast hpowr
53     have hn := (rationalCeilLog2_le_iff x _).mpr hpowq
54     have hi : (rationalCeilLog2 x : ℤ)≤(((ceilLog2 (x : ℝ)).toNat : ℕ) : ℤ) := by exact_mod_cast hn
55     rwa [hcast] at hi
56   · apply (ceilLog2_le_nat_iff _ hxp _).mpr
57     have hq := (rationalCeilLog2_le_iff x (rationalCeilLog2 x)).mp le_rfl
58     exact_mod_cast hq
59 
60 theorem logarithm_budget (V delta : ℝ) (hV : 1≤V) (hd : 0<delta) (hd1 : delta≤1) :
61     Real.log V+2*Real.log (1/delta)≤
62       (7/10 : ℝ)*((ceilLog2 V : ℝ)+2*(ceilLog2 (1/delta) : ℝ)) := by
63   have hdi : (1 : ℝ)≤1/delta := (le_div_iff₀ hd).mpr (by linarith)
64   have hk : (0 : ℝ)≤ceilLog2 V := by exact_mod_cast ceilLog2_nonneg V hV
65   have hh : (0 : ℝ)≤ceilLog2 (1/delta) := by exact_mod_cast ceilLog2_nonneg (1/delta) hdi
66   have hsum := add_le_add (log_le_ceilLog2 V)
67     (mul_le_mul_of_nonneg_left (log_le_ceilLog2 (1/delta)) (by norm_num : (0 : ℝ)≤2))
68   have hbound := mul_le_mul_of_nonneg_right log_two_lt_seven_tenths.le (by linarith :
69     0≤(ceilLog2 V : ℝ)+2*(ceilLog2 (1/delta) : ℝ))
70   nlinarith
71 
72 noncomputable def scalarRadius (sigma V delta : ℝ) : ℝ :=
73   sigma*Real.sqrt ((Real.log V+2*Real.log (1/delta))/V)+Real.sqrt (1/V)
74 
75 noncomputable def dyadicRadius (sigma V delta : ℝ) : ℝ :=
76   sigma*Real.sqrt (((7/10 : ℝ)*((ceilLog2 V : ℝ)+2*(ceilLog2 (1/delta) : ℝ)))/V)+
77     Real.sqrt (1/V)
78 
79 theorem scalarRadius_le_dyadic (sigma V delta : ℝ) (hs : 0≤sigma)
80     (hV : 1≤V) (hd : 0<delta) (hd1 : delta≤1) :
81     scalarRadius sigma V delta≤dyadicRadius sigma V delta := by
82   unfold scalarRadius dyadicRadius
83   apply add_le_add _ le_rfl
84   apply mul_le_mul_of_nonneg_left _ hs
85   apply Real.sqrt_le_sqrt
86   exact div_le_div_of_nonneg_right (logarithm_budget V delta hV hd hd1) (by linarith)
87 
88 /-- All quantities in the submitted upper enclosure are rational. -/
89 def rationalRadius (denominator : ℕ) (sigma V : ℚ) (k h : ℤ) : ℚ :=
90   sigma*upperSqrt denominator (((7/10 : ℚ)*((k : ℚ)+2*(h : ℚ)))/V)+
91     upperSqrt denominator (1/V)
92 
93 def computedRadius (denominator : ℕ) (sigma V delta : ℚ) : ℚ :=
94   rationalRadius denominator sigma V (rationalCeilLog2 V) (rationalCeilLog2 (1/delta))
95 
96 /-- Exact real-input version of the same componentwise outer-enclosure
97 protocol; rational inputs admit the integer-only implementation above. -/
98 noncomputable def outerRadius (denominator : ℕ) (sigma : ℚ) (V delta : ℝ) : ℚ :=
99   sigma*realUpperSqrt denominator
100     (((7/10 : ℝ)*((ceilLog2 V : ℝ)+2*(ceilLog2 (1/delta) : ℝ)))/V)+
101       realUpperSqrt denominator (1/V)
102 
103 theorem outerRadius_nonneg (denominator : ℕ) (sigma : ℚ) (hs : 0≤sigma) (V delta : ℝ) :
104     0≤outerRadius denominator sigma V delta :=
105   add_nonneg (mul_nonneg hs (realUpperSqrt_nonneg _ _)) (realUpperSqrt_nonneg _ _)
106 
107 theorem scalarRadius_le_outer (denominator : ℕ) (hden : 0<denominator)
108     (sigma : ℚ) (hs : 0≤sigma) (V delta : ℝ) (hV : 1≤V) (hd : 0<delta) (hd1 : delta≤1) :
109     scalarRadius sigma V delta≤(outerRadius denominator sigma V delta : ℝ) := by
110   apply (scalarRadius_le_dyadic sigma V delta (by exact_mod_cast hs) hV hd hd1).trans
111   have ha := sqrt_le_realUpperSqrt denominator hden
112     (((7/10 : ℝ)*((ceilLog2 V : ℝ)+2*(ceilLog2 (1/delta) : ℝ)))/V)
113   have hb := sqrt_le_realUpperSqrt denominator hden (1/V)
114   have hc := add_le_add (mul_le_mul_of_nonneg_left ha (by exact_mod_cast hs : (0 : ℝ)≤sigma)) hb
115   simpa only [dyadicRadius,outerRadius,Rat.cast_add,Rat.cast_mul] using hc
116 
117 theorem dyadicRadius_le_rational (denominator : ℕ) (hden : 0<denominator)
118     (sigma V delta : ℚ) (hs : 0≤sigma) (hV : 1≤V) (hd : 0<delta) (hd1 : delta≤1) :
119     dyadicRadius sigma V delta≤
120       (rationalRadius denominator sigma V (ceilLog2 V) (ceilLog2 (1/(delta : ℝ))) : ℝ) := by
121   have hVr : (0 : ℚ)<V := by linarith
122   have hdi : (1 : ℝ)≤1/(delta : ℝ) := by
123     apply (le_div_iff₀ (by exact_mod_cast hd : (0 : ℝ)<delta)).mpr
124     have hd1r : (delta : ℝ)≤1 := by exact_mod_cast hd1
125     simpa only [one_mul] using hd1r
126   have hk : 0≤ceilLog2 (V : ℝ) := ceilLog2_nonneg _ (by exact_mod_cast hV)
127   have hh : 0≤ceilLog2 (1/(delta : ℝ)) := ceilLog2_nonneg _ hdi
128   have hx : (0 : ℚ)≤((7/10 : ℚ)*((ceilLog2 (V : ℝ) : ℚ)+2*(ceilLog2 (1/(delta : ℝ)) : ℚ)))/V := by
129     positivity
130   have ha := sqrt_le_upperSqrt denominator hden _ hx
131   have hb := sqrt_le_upperSqrt denominator hden (1/V) (by positivity)
132   have hsr : (0 : ℝ)≤sigma := by exact_mod_cast hs
133   have hc := add_le_add (mul_le_mul_of_nonneg_left ha hsr) hb
134   simpa only [dyadicRadius,rationalRadius,Rat.cast_add,Rat.cast_mul,Rat.cast_div,
135     Rat.cast_intCast,Rat.cast_ofNat,Rat.cast_one] using hc
136 
137 theorem scalarRadius_le_computed (denominator : ℕ) (hden : 0<denominator)
138     (sigma V delta : ℚ) (hs : 0≤sigma) (hV : 1≤V) (hd : 0<delta) (hd1 : delta≤1) :
139     scalarRadius sigma V delta≤(computedRadius denominator sigma V delta : ℝ) := by
140   have hdi : (1 : ℚ)≤1/delta := (le_div_iff₀ hd).mpr (by linarith)
141   have heV := rationalCeilLog2_eq V hV
142   have hed : (rationalCeilLog2 (1/delta) : ℤ)=ceilLog2 (1/(delta : ℝ)) := by
143     simpa only [Rat.cast_div,Rat.cast_one] using rationalCeilLog2_eq (1/delta) hdi
144   have h := (scalarRadius_le_dyadic (sigma : ℝ) V delta (by exact_mod_cast hs)
145     (by exact_mod_cast hV) (by exact_mod_cast hd) (by exact_mod_cast hd1)).trans
146       (dyadicRadius_le_rational denominator hden sigma V delta hs hV hd hd1)
147   simpa only [computedRadius,heV,hed] using h
148 
149 end Komorebi.LSM.RationalConfidenceArithmetic

Back to source controls