Certificates.lean

1 import Mathlib.Basic.Real.Basic
2 import Mathlib.Tactic.Linarith
3 
4 /-!
5 # Arithmetic consequences of supplied enclosures
6 
7 This module proves what follows from valid exact-real error bounds. It does
8 not prove COS inversion, support/alias bounds, mode-tail estimates, spectral
9 inclusion, or the correctness of mpmath.iv.
10 -/
11 
12 namespace KomorebiQCOS
13 
14 /-- A mathematical enclosure of one exact real number. -/
15 def Enclosed (value lower upper : ℝ) : Prop := lower ≤ value ∧ value ≤ upper
16 
17 /-- An exact-real additive error budget. -/
18 def ErrorBound (value estimate radius : ℝ) : Prop := |value - estimate| ≤ radius
19 
20 theorem enclosed_order {value lower upper : ℝ}
21     (h : Enclosed value lower upper) : lower ≤ upper :=
22   h.1.trans h.2
23 
24 theorem enclosed_add {x y lx ux ly uy : ℝ}
25     (hx : Enclosed x lx ux) (hy : Enclosed y ly uy) :
26     Enclosed (x + y) (lx + ly) (ux + uy) := by
27   exact ⟨add_le_add hx.1 hy.1, add_le_add hx.2 hy.2⟩
28 
29 theorem enclosed_scale {value lower upper a : ℝ}
30     (ha : 0 ≤ a) (h : Enclosed value lower upper) :
31     Enclosed (a * value) (a * lower) (a * upper) := by
32   exact ⟨mul_le_mul_of_nonneg_left h.1 ha, mul_le_mul_of_nonneg_left h.2 ha⟩
33 
34 theorem enclosed_widen {value lower upper lo hi : ℝ}
35     (h : Enclosed value lower upper) (hl : lo ≤ lower) (hu : upper ≤ hi) :
36     Enclosed value lo hi :=
37   ⟨hl.trans h.1, h.2.trans hu⟩
38 
39 /-- Multiple independently valid enclosures may be intersected. -/
40 theorem enclosed_intersect {value l₁ u₁ l₂ u₂ : ℝ}
41     (h₁ : Enclosed value l₁ u₁) (h₂ : Enclosed value l₂ u₂) :
42     Enclosed value (max l₁ l₂) (min u₁ u₂) := by
43   exact ⟨max_le h₁.1 h₂.1, le_min h₁.2 h₂.2⟩
44 
45 theorem errorBound_iff_enclosed (value estimate radius : ℝ) :
46     ErrorBound value estimate radius ↔
47       Enclosed value (estimate - radius) (estimate + radius) := by
48   unfold ErrorBound Enclosed
49   rw [abs_le]
50   constructor
51   · rintro ⟨hl, hu⟩
52     constructor <;> linarith
53   · rintro ⟨hl, hu⟩
54     constructor <;> linarith
55 
56 /-- Error bounds from arithmetic and analysis combine additively. -/
57 theorem errorBound_compose {value middle estimate analytic arithmetic : ℝ}
58     (ha : ErrorBound value middle analytic)
59     (hr : ErrorBound middle estimate arithmetic) :
60     ErrorBound value estimate (analytic + arithmetic) := by
61   unfold ErrorBound at *
62   calc
63     |value - estimate| = |(value - middle) + (middle - estimate)| := by
64       congr 1
65       linarith
66     _ ≤ |value - middle| + |middle - estimate| := abs_add_le _ _
67     _ ≤ analytic + arithmetic := add_le_add ha hr
68 
69 /-- Once the sum of all proved error budgets is within tolerance, the output
70 has the corresponding exact-real absolute error guarantee. -/
71 theorem errorBound_accept {value middle estimate analytic arithmetic tolerance : ℝ}
72     (ha : ErrorBound value middle analytic)
73     (hr : ErrorBound middle estimate arithmetic)
74     (hbudget : analytic + arithmetic ≤ tolerance) :
75     ErrorBound value estimate tolerance :=
76   (errorBound_compose ha hr).trans hbudget
77 
78 /-- A strictly positive lower interval endpoint proves positivity. -/
79 theorem enclosed_positive {value lower upper : ℝ}
80     (h : Enclosed value lower upper) (hl : 0 < lower) : 0 < value :=
81   hl.trans_le h.1
82 
83 /-- Monotone transformations carry an enclosure to their endpoint images.
84 The transformation's monotonicity is an explicit hypothesis. -/
85 theorem enclosed_monotone {f : ℝ → ℝ} (hf : Monotone f)
86     {value lower upper : ℝ} (h : Enclosed value lower upper) :
87     Enclosed (f value) (f lower) (f upper) :=
88   ⟨hf h.1, hf h.2⟩
89 
90 end KomorebiQCOS

Back to source controls