DyadicLogThresholds.lean

1 module
2 
3 public import Mathlib.Data.Nat.Log
4 public import Mathlib.Tactic
5 
6 /-!
7 Arithmetic thresholds used to reduce dyadic Newton coefficient estimates to a
8 finite prefix. All tail bounds follow by induction, not by bounded evaluation.
9 -/
10 
11 @[expose] public section
12 
13 namespace KomorebiPaperIX.DyadicLogThresholds
14 
15 theorem log_two_succ_le (n : ℕ) (hn : 1 ≤ n) :
16     Nat.log 2 (n + 1) ≤ Nat.log 2 n + 1 := by
17   calc
18     Nat.log 2 (n + 1) ≤ Nat.log 2 (n * 2) :=
19       Nat.log_mono_right (by omega)
20     _ = Nat.log 2 n + 1 := Nat.log_mul_base (by omega) (by omega)
21 
22 /-- Once an offset-log bound holds at a positive index, it holds thereafter. -/
23 theorem offset_log_bound_of_le (a c n : ℕ) (ha : 1 ≤ a)
24     (hbase : c + Nat.log 2 a ≤ a) (han : a ≤ n) :
25     c + Nat.log 2 n ≤ n := by
26   induction n, han using Nat.le_induction with
27   | base => exact hbase
28   | succ n hn ih =>
29       have hstep := log_two_succ_le n (by omega)
30       omega
31 
32 theorem two_add_log_le (k : ℕ) (hk : 3 ≤ k) :
33     2 + Nat.log 2 k ≤ k := by
34   apply offset_log_bound_of_le 3 2 k (by omega) _ hk
35   decide
36 
37 theorem three_add_log_le (k : ℕ) (hk : 5 ≤ k) :
38     3 + Nat.log 2 k ≤ k := by
39   apply offset_log_bound_of_le 5 3 k (by omega) _ hk
40   decide
41 
42 theorem five_add_log_le (k : ℕ) (hk : 7 ≤ k) :
43     5 + Nat.log 2 k ≤ k := by
44   apply offset_log_bound_of_le 7 5 k (by omega) _ hk
45   decide
46 
47 end KomorebiPaperIX.DyadicLogThresholds

Back to source controls