GuardedInterfaces.lean

1 import CoupledGuardedMajorant
2 noncomputable section
3 open Komorebi.SpecialFunctions.Coupled.Scales
4 
5 example : buildLadder (1/2) 2 2 = .ok ([2,1],1/2) := by norm_num [buildLadder]
6 example : buildLadder (1/2) 1 2 = .error .steps := by norm_num [buildLadder]
7 example : guardedFold (fun _ => true) (2/3) [2,1] = .ok (500/81) := by
8   norm_num [guardedFold,majorantStep]
9 example : guardedMajorant (1/2) 2 (fun _ => true) 2 = .ok (500/81) := by
10   norm_num [guardedMajorant,buildLadder,guardedFold,majorantSeed,majorantStep]
11 example : guardedMajorant (1/2) 1 (fun _ => false) 2 = .error .steps := by
12   norm_num [guardedMajorant,buildLadder]
13 example : guardedMajorant (1/2) 2 (fun _ => false) 2 = .error .bits := by
14   norm_num [guardedMajorant,buildLadder,guardedFold]
15 example : guardedMajorant (1/2) 0 (fun _ => true) 1 = .error .steps := by
16   exact guarded_majorant_no_steps _ _ _ (by norm_num)
17 example : checkedMajorant (⟨1/2,1/2,1/2,1/2⟩ : RationalScales) 0 none none = .ok 0 := by
18   exact checked_zero_before_resources _ _ _ (by norm_num [RationalScales.strictRational])
19 example : checkedMajorant (⟨1,1/2,1/2,1/2⟩ : RationalScales) 0 none none = .error .scales := by
20   exact checked_invalid_scales _ _ _ _ (by norm_num [RationalScales.strictRational])
21 example : checkedMajorant (⟨1/2,1/2,1/2,1/2⟩ : RationalScales) (3/4)
22     (some 0) (some 1) = .ok (12/7) := by
23   have h := checked_small_seed_unchecked (⟨1/2,1/2,1/2,1/2⟩ : RationalScales) (3/4) 0 0
24     (by norm_num [RationalScales.strictRational]) (by norm_num) (by norm_num)
25   norm_num [majorantSeed] at h ⊢
26   exact h
27 example : sizeFits 1 (12/7) = false := by
28   have h12 : Nat.log2 12 = 3 := (Nat.log2_eq_iff (by decide)).mpr (by decide)
29   have h7 : Nat.log2 7 = 2 := (Nat.log2_eq_iff (by decide)).mpr (by decide)
30   norm_num [sizeFits,rationalBitSize,integerWidth,h12,h7]
31 example : checkedMajorant (⟨1/2,1/2,1/2,1/2⟩ : RationalScales) 2 (some 2) (some 1) =
32     .error (.resource .bits) := by
33   have h13 : Nat.log2 13 = 3 := (Nat.log2_eq_iff (by decide)).mpr (by decide)
34   have h9 : Nat.log2 9 = 3 := (Nat.log2_eq_iff (by decide)).mpr (by decide)
35   norm_num [checkedMajorant,RationalScales.strictRational,guardedMajorant,buildLadder,guardedFold,
36     majorantSeed,majorantStep,sizeFits,rationalBitSize,integerWidth,RationalScales.maxScale,h13,h9]
37 example (Q R t : ℚ) (xs : List ℚ) (h : LadderTrace Q R xs t) : Q^xs.length*R < 1 :=
38   ladder_adequate Q R t xs h
39 example (p : RationalScales) (hs : p.toReal.positive)
40     (hc : p.toReal.q < 1 ∧ p.toReal.r < 1 ∧ p.toReal.a < 1 ∧ p.toReal.b < 1)
41     (R B : ℚ) (hR : 0 ≤ R) (budget : ℕ) (fits : ℚ → Bool)
42     (h : guardedMajorant p.maxScale budget fits R = .ok B) (i : Fin 2)
43     (z : ℂ) (hz : ‖z‖ ≤ (R : ℝ)) : ‖p.toReal.complexComponent i z‖ ≤ (B : ℝ) :=
44   guarded_majorant_disk_bound p hs hc R B hR budget fits h i z hz

Back to source controls