Mathlib.Analysis.CertifiedContourIntervalArithmetic
Certified numerical-analysis infrastructure: exact rational intervals, effective certified-real refinement, transcendental enclosures, Lipschitz mesh quadrature, and measurable finite selection.
Basic 18 core · 29 supporting 18 to review This module provides closed intervals with rational endpoints and exact endpoint algorithms for the elementary arithmetic operations. ★ mul_sound
Exact rational interval arithmetic
This module provides closed intervals with rational endpoints and exact endpoint algorithms for the elementary arithmetic operations. Each operation is proved to enclose the corresponding real-number calculation, and the inclusion order records safe refinement of an enclosure.
structure RatInterval unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic
A rational closed interval consists of a rational lower endpoint and a rational upper endpoint, with the lower endpoint no greater than the upper endpoint.
Definition (Lean source)
fields
The rational lower endpoint of the enclosure.
lo :
ℚ
The rational upper endpoint of the enclosure.
hi :
ℚ
The lower endpoint does not exceed the upper endpoint.
lo_le_hi :
lo ≤ hi
def Contains unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
A real number is contained in a rational interval when it lies between the real casts of its endpoints.
Definition (Lean source)
def Contains (I : RatInterval) (x : ℝ) : Prop :=
(I.lo : ℝ) ≤ x ∧ x ≤ (I.hi : ℝ)
def width unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
The width of a rational interval is its upper endpoint minus its lower endpoint.
Definition (Lean source)
def width (I : RatInterval) : ℚ := I.hi - I.lo
def maxAbs unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
The maximum endpoint magnitude is a rational bound for the absolute value of every real number in the interval.
Definition (Lean source)
def maxAbs (I : RatInterval) : ℚ := max |I.lo| |I.hi|
def Subinterval unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Interval inclusion means that every point in the first enclosure also lies in the second.
Definition (Lean source)
def Subinterval (I J : RatInterval) : Prop :=
J.lo ≤ I.lo ∧ I.hi ≤ J.hi
def point unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
A point interval contains exactly one rational value.
Definition (Lean source)
def point (q : ℚ) : RatInterval := ⟨q, q, le_rfl⟩
def hull unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
The convex hull of two rational intervals is their least endpoint-wise hull.
Definition (Lean source)
def hull (I J : RatInterval) : RatInterval :=
⟨min I.lo J.lo, max I.hi J.hi, by
exact (min_le_left _ _).trans (I.lo_le_hi.trans (le_max_left _ _))⟩
def add unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Addition evaluates all possible sums by adding the two lower and two upper endpoints.
Definition (Lean source)
def add (I J : RatInterval) : RatInterval :=
⟨I.lo + J.lo, I.hi + J.hi, add_le_add I.lo_le_hi J.lo_le_hi⟩
def neg unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Negation reverses and negates the endpoints.
Definition (Lean source)
def sub unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Subtraction is addition with the negated second interval.
Definition (Lean source)
def mul unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Multiplication takes the minimum and maximum of the four endpoint products.
Definition (Lean source)
def mul (I J : RatInterval) : RatInterval :=
let a := I.lo * J.lo
let b := I.lo * J.hi
let c := I.hi * J.lo
let d := I.hi * J.hi
⟨min (min a b) (min c d), max (max a b) (max c d), by
exact (min_le_left _ _).trans
((min_le_left _ _).trans ((le_max_left _ _).trans (le_max_left _ _)))⟩
def AwayFromZero unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
An interval is separated from zero when it lies strictly on one side of zero.
Definition (Lean source)
def AwayFromZero (I : RatInterval) : Prop := I.hi < 0 ∨ 0 < I.lo
def inv unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Reciprocal reverses the endpoints of an interval certified away from zero.
Definition (Lean source)
def inv (I : RatInterval) (hI : I.AwayFromZero) : RatInterval :=
⟨I.hi⁻¹, I.lo⁻¹, by
rcases hI with hI | hI
· exact (inv_le_inv_of_neg hI (I.lo_le_hi.trans_lt hI)).2 I.lo_le_hi
· exact (inv_le_inv₀ (hI.trans_le I.lo_le_hi) hI).2 I.lo_le_hi⟩
def div unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Division multiplies by the reciprocal of a denominator interval certified away from zero.
Definition (Lean source)
def npow unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Natural powers are evaluated by repeated rational interval multiplication.
Definition (Lean source)
def tighten unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Conditional intersection keeps the exact intersection when its rational endpoints overlap, and otherwise returns the first interval.
Definition (Lean source)
def tighten (I J : RatInterval) : RatInterval :=
if h : max I.lo J.lo ≤ min I.hi J.hi then
⟨max I.lo J.lo, min I.hi J.hi, h⟩
else I
def expand unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
Widening by a nonnegative rational amount subtracts it below and adds it above.
Definition (Lean source)
def expand (I : RatInterval) (e : ℚ) (he : 0 ≤ e) : RatInterval :=
⟨I.lo - e, I.hi + e, by linarith [I.lo_le_hi]⟩
theorem mul_sound unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.RatInterval
For rational intervals I and J, if x is a real number contained in I and y is a real number contained in J, then the interval-multiplication enclosure mul I J contains the real product x * y.
Formal statement
hypotheses
conclusion
(mul I J).Contains (x * y)
Proof (Lean source)
theorem mul_sound {I J : RatInterval} {x y : ℝ}
(hx : I.Contains x) (hy : J.Contains y) : (mul I J).Contains (x * y) := by
rcases hx with ⟨hxl, hxu⟩
rcases hy with ⟨hyl, hyu⟩
simp only [mul, Contains, Rat.cast_min, Rat.cast_max, Rat.cast_mul]
constructor
· by_cases hx0 : 0 ≤ x
· by_cases hy0 : 0 ≤ y
· by_cases hIl : 0 ≤ (I.lo : ℝ)
· refine (min_le_of_left_le (min_le_of_left_le ?_))
calc
(I.lo : ℝ) * J.lo ≤ I.lo * y := mul_le_mul_of_nonneg_left hyl hIl
_ ≤ x * y := mul_le_mul_of_nonneg_right hxl hy0
· refine (min_le_of_left_le (min_le_of_right_le ?_))
calc
(I.lo : ℝ) * J.hi ≤ I.lo * y := mul_le_mul_of_nonpos_left hyu (le_of_not_ge hIl)
_ ≤ x * y := mul_le_mul_of_nonneg_right hxl hy0
· have hy0' : y ≤ 0 := le_of_not_ge hy0
refine (min_le_of_right_le (min_le_of_left_le ?_))
calc
(I.hi : ℝ) * J.lo ≤ I.hi * y :=
mul_le_mul_of_nonneg_left hyl (hx0.trans hxu)
_ ≤ x * y := mul_le_mul_of_nonpos_right hxu hy0'
· have hx0' : x ≤ 0 := le_of_not_ge hx0
by_cases hy0 : 0 ≤ y
· refine (min_le_of_left_le (min_le_of_right_le ?_))
calc
(I.lo : ℝ) * J.hi ≤ x * J.hi :=
mul_le_mul_of_nonneg_right hxl (hy0.trans hyu)
_ ≤ x * y := mul_le_mul_of_nonpos_left hyu hx0'
· have hy0' : y ≤ 0 := le_of_not_ge hy0
by_cases hIh : (I.hi : ℝ) ≤ 0
· refine (min_le_of_right_le (min_le_of_right_le ?_))
calc
(I.hi : ℝ) * J.hi ≤ I.hi * y := mul_le_mul_of_nonpos_left hyu hIh
_ ≤ x * y := mul_le_mul_of_nonpos_right hxu hy0'
· refine (min_le_of_right_le (min_le_of_left_le ?_))
calc
(I.hi : ℝ) * J.lo ≤ I.hi * y :=
mul_le_mul_of_nonneg_left hyl (le_of_not_ge hIh)
_ ≤ x * y := mul_le_mul_of_nonpos_right hxu hy0'
· by_cases hx0 : 0 ≤ x
· by_cases hy0 : 0 ≤ y
· refine (le_max_of_le_right (le_max_of_le_right ?_))
calc
x * y ≤ (I.hi : ℝ) * y := mul_le_mul_of_nonneg_right hxu hy0
_ ≤ I.hi * J.hi := mul_le_mul_of_nonneg_left hyu (hx0.trans hxu)
· have hy0' : y ≤ 0 := le_of_not_ge hy0
by_cases hIl : 0 ≤ (I.lo : ℝ)
· refine (le_max_of_le_left (le_max_of_le_right ?_))
calc
x * y ≤ (I.lo : ℝ) * y := mul_le_mul_of_nonpos_right hxl hy0'
_ ≤ I.lo * J.hi := mul_le_mul_of_nonneg_left hyu hIl
· refine (le_max_of_le_left (le_max_of_le_left ?_))
calc
x * y ≤ (I.lo : ℝ) * y := mul_le_mul_of_nonpos_right hxl hy0'
_ ≤ I.lo * J.lo := mul_le_mul_of_nonpos_left hyl (le_of_not_ge hIl)
· have hx0' : x ≤ 0 := le_of_not_ge hx0
by_cases hy0 : 0 ≤ y
· by_cases hJl : 0 ≤ (J.lo : ℝ)
· refine (le_max_of_le_right (le_max_of_le_left ?_))
calc
x * y ≤ x * (J.lo : ℝ) := mul_le_mul_of_nonpos_left hyl hx0'
_ ≤ I.hi * J.lo := mul_le_mul_of_nonneg_right hxu hJl
· refine (le_max_of_le_left (le_max_of_le_left ?_))
calc
x * y ≤ x * (J.lo : ℝ) := mul_le_mul_of_nonpos_left hyl hx0'
_ ≤ I.lo * J.lo := mul_le_mul_of_nonpos_right hxl (le_of_not_ge hJl)
· have hy0' : y ≤ 0 := le_of_not_ge hy0
refine (le_max_of_le_left (le_max_of_le_left ?_))
calc
x * y ≤ (I.lo : ℝ) * y := mul_le_mul_of_nonpos_right hxl hy0'
_ ≤ I.lo * J.lo := mul_le_mul_of_nonpos_left hyl (hxl.trans hx0')
29 supporting declarations (lemmas, instances)
-
width_nonnegtheorem — Every rational interval has nonnegative width.Proof (Lean source)
theorem width_nonneg (I : RatInterval) : 0 ≤ I.width := by exact sub_nonneg.mpr I.lo_le_hi -
contains_point_ifftheorem — Containment in a point interval is equality with that rational point.hypothesesq :ℚx :ℝconclusion(point q).Contains x ↔ x = (q : ℝ)Proof (Lean source)
@[simp] theorem contains_point_iff (q : ℚ) (x : ℝ) : (point q).Contains x ↔ x = (q : ℝ) := by constructor · rintro ⟨hlo, hhi⟩ exact le_antisymm hhi hlo · rintro rfl exact ⟨le_rfl, le_rfl⟩ -
subinterval_refltheorem — Subinterval is reflexive.Proof (Lean source)
theorem subinterval_refl (I : RatInterval) : I.Subinterval I := by exact ⟨le_rfl, le_rfl⟩ -
subinterval_transtheorem — Subinterval is transitive.Proof (Lean source)
theorem subinterval_trans {I J K : RatInterval} : I.Subinterval J → J.Subinterval K → I.Subinterval K := by rintro ⟨hlo₁, hhi₁⟩ ⟨hlo₂, hhi₂⟩ exact ⟨hlo₂.trans hlo₁, hhi₁.trans hhi₂⟩ -
monotheorem — A real point contained in a subinterval is contained in the enclosing interval.Proof (Lean source)
theorem Contains.mono {I J : RatInterval} {x : ℝ} (hIJ : I.Subinterval J) (hx : I.Contains x) : J.Contains x := by have hlo : (J.lo : ℝ) ≤ I.lo := by exact_mod_cast hIJ.1 have hhi : (I.hi : ℝ) ≤ J.hi := by exact_mod_cast hIJ.2 exact ⟨hlo.trans hx.1, hx.2.trans hhi⟩ -
width_monotheorem — Inclusion of rational intervals cannot increase their width.Proof (Lean source)
theorem width_mono {I J : RatInterval} (hIJ : I.Subinterval J) : I.width ≤ J.width := by unfold width linarith [hIJ.1, hIJ.2] -
point_soundtheorem — The point interval soundly encloses its rational value viewed as a real.hypothesesq :ℚconclusion(point q).Contains (q : ℝ)Proof (Lean source)
theorem point_sound (q : ℚ) : (point q).Contains (q : ℝ) := by simp -
add_soundtheorem — Rational interval addition encloses the sum of any enclosed real operands.hypothesesconclusion(add I J).Contains (x + y)Proof (Lean source)
theorem add_sound {I J : RatInterval} {x y : ℝ} (hx : I.Contains x) (hy : J.Contains y) : (add I J).Contains (x + y) := by constructor <;> simp only [add, Contains, Rat.cast_add] · exact add_le_add hx.1 hy.1 · exact add_le_add hx.2 hy.2 -
neg_soundtheorem — Rational interval negation encloses the negation of every enclosed real operand.Proof (Lean source)
theorem neg_sound {I : RatInterval} {x : ℝ} (hx : I.Contains x) : I.neg.Contains (-x) := by constructor <;> simp only [neg, Contains, Rat.cast_neg] · exact neg_le_neg hx.2 · exact neg_le_neg hx.1 -
sub_soundtheorem — Rational interval subtraction encloses the difference of any enclosed real operands.hypothesesconclusion(sub I J).Contains (x - y)Proof (Lean source)
theorem sub_sound {I J : RatInterval} {x y : ℝ} (hx : I.Contains x) (hy : J.Contains y) : (sub I J).Contains (x - y) := by simpa [sub_eq_add_neg, sub] using add_sound hx (neg_sound hy) -
ne_zero_of_containstheorem — A real number contained in an interval separated from zero is nonzero.Proof (Lean source)
theorem ne_zero_of_contains {I : RatInterval} {x : ℝ} (hI : I.AwayFromZero) (hx : I.Contains x) : x ≠ 0 := by rcases hI with hI | hI · have hI' : (I.hi : ℝ) < 0 := by exact_mod_cast hI exact ne_of_lt (hx.2.trans_lt hI') · have hI' : (0 : ℝ) < I.lo := by exact_mod_cast hI exact ne_of_gt (hI'.trans_le hx.1) -
inv_soundtheorem — Rational interval reciprocal encloses the reciprocal of every enclosed real operand.hypothesesconclusion(inv I hI).Contains x⁻¹Proof (Lean source)
theorem inv_sound {I : RatInterval} {x : ℝ} (hI : I.AwayFromZero) (hx : I.Contains x) : (inv I hI).Contains x⁻¹ := by rcases hI with hneg | hpos · have hhineg : (I.hi : ℝ) < 0 := by exact_mod_cast hneg have hloneg : (I.lo : ℝ) < 0 := by exact_mod_cast I.lo_le_hi.trans_lt hneg have hxneg : x < 0 := hx.2.trans_lt hhineg simp only [inv, Contains, Rat.cast_inv] exact ⟨(inv_le_inv_of_neg hhineg hxneg).2 hx.2, (inv_le_inv_of_neg hxneg hloneg).2 hx.1⟩ · have hlopos : (0 : ℝ) < I.lo := by exact_mod_cast hpos have hhipos : (0 : ℝ) < I.hi := by exact_mod_cast hpos.trans_le I.lo_le_hi have hxpos : 0 < x := hlopos.trans_le hx.1 simp only [inv, Contains, Rat.cast_inv] exact ⟨(inv_le_inv₀ hhipos hxpos).2 hx.2, (inv_le_inv₀ hxpos hlopos).2 hx.1⟩ -
div_soundtheorem — Rational interval division encloses every quotient whose denominator interval avoids zero.hypothesesconclusion(div I J hJ).Contains (x / y)Proof (Lean source)
theorem div_sound {I J : RatInterval} {x y : ℝ} (hJ : J.AwayFromZero) (hx : I.Contains x) (hy : J.Contains y) : (div I J hJ).Contains (x / y) := by simpa [div, div_eq_mul_inv] using mul_sound hx (inv_sound hJ hy) -
npow_soundtheorem — Repeated interval multiplication encloses every natural power of an enclosed real number.Proof (Lean source)
theorem npow_sound {I : RatInterval} {x : ℝ} (hx : I.Contains x) (n : ℕ) : (I.npow n).Contains (x ^ n) := by induction n with | zero => simpa [npow] using point_sound 1 | succ n ih => simpa [npow, pow_succ] using mul_sound ih hx -
tighten_soundtheorem — Tightening two intervals that share an enclosed real point returns their intersection and continues to enclose that point.hypothesesconclusion(tighten I J).Contains xProof (Lean source)
theorem tighten_sound {I J : RatInterval} {x : ℝ} (hI : I.Contains x) (hJ : J.Contains x) : (tighten I J).Contains x := by have hlohi : max I.lo J.lo ≤ min I.hi J.hi := by apply max_le · apply le_min I.lo_le_hi exact_mod_cast hI.1.trans hJ.2 · apply le_min · exact_mod_cast hJ.1.trans hI.2 · exact J.lo_le_hi simp only [tighten, hlohi, dif_pos, Contains, Rat.cast_max, Rat.cast_min] exact ⟨max_le hI.1 hJ.1, le_min hI.2 hJ.2⟩ -
tighten_subinterval_lefttheorem — Tightening by another sound interval produces a subinterval of the first interval.hypothesesconclusion(tighten I J).Subinterval IProof (Lean source)
theorem tighten_subinterval_left {I J : RatInterval} {x : ℝ} (hI : I.Contains x) (hJ : J.Contains x) : (tighten I J).Subinterval I := by have hlohi : max I.lo J.lo ≤ min I.hi J.hi := by apply max_le · apply le_min I.lo_le_hi exact_mod_cast hI.1.trans hJ.2 · apply le_min · exact_mod_cast hJ.1.trans hI.2 · exact J.lo_le_hi simp only [tighten, hlohi, dif_pos, Subinterval] exact ⟨le_max_left _ _, min_le_left _ _⟩ -
add_monotheorem — Addition is inclusion-isotone in both interval arguments.hypothesesconclusion(add I J).Subinterval (add I' J')Proof (Lean source)
theorem add_mono {I I' J J' : RatInterval} (hI : I.Subinterval I') (hJ : J.Subinterval J') : (add I J).Subinterval (add I' J') := by exact ⟨add_le_add hI.1 hJ.1, add_le_add hI.2 hJ.2⟩ -
neg_monotheorem — Negation preserves interval inclusion.Proof (Lean source)
theorem neg_mono {I J : RatInterval} (hIJ : I.Subinterval J) : I.neg.Subinterval J.neg := by exact ⟨neg_le_neg hIJ.2, neg_le_neg hIJ.1⟩ -
sub_monotheorem — Subtraction is inclusion-isotone in both interval arguments.hypothesesconclusion(sub I J).Subinterval (sub I' J')Proof (Lean source)
theorem sub_mono {I I' J J' : RatInterval} (hI : I.Subinterval I') (hJ : J.Subinterval J') : (sub I J).Subinterval (sub I' J') := by exact add_mono hI (neg_mono hJ) -
mul_monotheorem — Multiplication is inclusion-isotone in both interval arguments.hypothesesProof (Lean source)
theorem mul_mono {I I' J J' : RatInterval} (hI : I.Subinterval I') (hJ : J.Subinterval J') : (mul I J).Subinterval (mul I' J') := by have Ilo : I.Contains (I.lo : ℝ) := ⟨le_rfl, by exact_mod_cast I.lo_le_hi⟩ have Ihi : I.Contains (I.hi : ℝ) := ⟨by exact_mod_cast I.lo_le_hi, le_rfl⟩ have Jlo : J.Contains (J.lo : ℝ) := ⟨le_rfl, by exact_mod_cast J.lo_le_hi⟩ have Jhi : J.Contains (J.hi : ℝ) := ⟨by exact_mod_cast J.lo_le_hi, le_rfl⟩ have p₁ : (mul I' J').Contains ((I.lo : ℝ) * (J.lo : ℝ)) := mul_sound (Contains.mono hI Ilo) (Contains.mono hJ Jlo) have p₂ : (mul I' J').Contains ((I.lo : ℝ) * (J.hi : ℝ)) := mul_sound (Contains.mono hI Ilo) (Contains.mono hJ Jhi) have p₃ : (mul I' J').Contains ((I.hi : ℝ) * (J.lo : ℝ)) := mul_sound (Contains.mono hI Ihi) (Contains.mono hJ Jlo) have p₄ : (mul I' J').Contains ((I.hi : ℝ) * (J.hi : ℝ)) := mul_sound (Contains.mono hI Ihi) (Contains.mono hJ Jhi) simp only [Subinterval, mul] constructor · apply le_min · apply le_min · exact_mod_cast p₁.1 · exact_mod_cast p₂.1 · apply le_min · exact_mod_cast p₃.1 · exact_mod_cast p₄.1 · apply max_le · apply max_le · exact_mod_cast p₁.2 · exact_mod_cast p₂.2 · apply max_le · exact_mod_cast p₃.2 · exact_mod_cast p₄.2 -
npow_monotheorem — Natural interval powers preserve interval inclusion.hypothesesconclusion(I.npow n).Subinterval (J.npow n)Proof (Lean source)
theorem npow_mono {I J : RatInterval} (hIJ : I.Subinterval J) (n : ℕ) : (I.npow n).Subinterval (J.npow n) := by induction n with | zero => exact subinterval_refl _ | succ n ih => exact mul_mono ih hIJ -
inv_monotheorem — Reciprocal preserves inclusion when both intervals are certified away from zero.hypothesesconclusion(inv I hI).Subinterval (inv J hJ)Proof (Lean source)
theorem inv_mono {I J : RatInterval} (hIJ : I.Subinterval J) (hI : I.AwayFromZero) (hJ : J.AwayFromZero) : (inv I hI).Subinterval (inv J hJ) := by simp only [Subinterval, inv] constructor · rcases hJ with hJneg | hJpos · exact (inv_le_inv_of_neg hJneg (hIJ.2.trans_lt hJneg)).2 hIJ.2 · exact (inv_le_inv₀ (hJpos.trans_le J.lo_le_hi) ((hJpos.trans_le hIJ.1).trans_le I.lo_le_hi)).2 hIJ.2 · rcases hJ with hJneg | hJpos · exact (inv_le_inv_of_neg (I.lo_le_hi.trans_lt (hIJ.2.trans_lt hJneg)) (J.lo_le_hi.trans_lt hJneg)).2 hIJ.1 · exact (inv_le_inv₀ (hJpos.trans_le hIJ.1) hJpos).2 hIJ.1 -
div_monotheorem — Division is inclusion-isotone when both denominator intervals avoid zero.hypothesesI I' J J' :hI :I.Subinterval I'hJ :J.Subinterval J'hJ0 :J.AwayFromZerohJ0' :J'.AwayFromZeroconclusion(div I J hJ0).Subinterval (div I' J' hJ0')Proof (Lean source)
theorem div_mono {I I' J J' : RatInterval} (hI : I.Subinterval I') (hJ : J.Subinterval J') (hJ0 : J.AwayFromZero) (hJ0' : J'.AwayFromZero) : (div I J hJ0).Subinterval (div I' J' hJ0') := by exact mul_mono hI (inv_mono hJ hJ0 hJ0') -
width_addtheorem — Addition makes widths add exactly.Proof (Lean source)
theorem width_add (I J : RatInterval) : (add I J).width = I.width + J.width := by simp [width, add] ring -
width_negtheorem — Negation preserves interval width exactly.Proof (Lean source)
-
width_subtheorem — Subtraction makes widths add exactly.Proof (Lean source)
theorem width_sub (I J : RatInterval) : (sub I J).width = I.width + J.width := by simp [sub, width_add, width_neg] -
width_expandtheorem — Widening an interval by a nonnegative amount on each side increases its width by twice that amount.Proof (Lean source)
theorem width_expand (I : RatInterval) (e : ℚ) (he : 0 ≤ e) : (expand I e he).width = I.width + 2 * e := by simp [expand, width] ring
CertifiedReal 8 core · 5 supporting 8 to review This module represents a real quantity by nested rational enclosures together with a computable precision rule. ★ refine_width
Certified real names and effective refinement
This module represents a real quantity by nested rational enclosures together with a computable precision rule. It turns any positive rational error target into a concrete interval that still contains the quantity and is no wider than that target.
abbrev PosRat unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic
A positive rational is a rational number bundled with a proof that it is strictly positive.
Definition (Lean source)
abbrev PosRat := {q : ℚ // 0 < q}
structure CertifiedReal unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic
A certified real name represents a real number by a sequence of rational interval enclosures indexed by precision that is nested — each successive enclosure a subinterval of the one before — and always contains the represented value, together with a computable rule selecting, for any requested positive rational error, a precision level whose enclosure is no wider than that error.
Definition (Lean source)
fields
The real number denoted by the certified name.
value :
ℝ
The rational enclosure returned at each natural precision.
approx :
ℕ → RatInterval
Increasing precision produces a subinterval of the preceding enclosure.
nested :
∀ n, (approx (n + 1)).Subinterval (approx n)
Every rational approximation encloses the denoted real value.
contains :
∀ n, (approx n).Contains value
The computable precision selected for a requested positive rational width.
modulus :
PosRat → ℕ
The interval at the selected precision has at most the requested width.
width_modulus :
∀ ε : PosRat, (approx (modulus ε)).width ≤ ε.1
def refine unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CertifiedReal
Refinement evaluates the certified modulus and returns its rational enclosure.
Definition (Lean source)
theorem refine_width unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CertifiedReal
For a certified real number x and a requested positive rational tolerance ε, refining x to the precision selected by ε's modulus yields an enclosure whose width is at most ε.
Formal statement
Proof (Lean source)
theorem refine_width (x : CertifiedReal) (ε : PosRat) :
(x.refine ε).width ≤ ε.1 := by
exact x.width_modulus ε
def ofRat unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CertifiedReal
A rational number has the constant point interval as a certified real name.
Definition (Lean source)
def ofRat (q : ℚ) : CertifiedReal where
value := q
approx := fun _ => RatInterval.point q
nested := by
intro n
exact RatInterval.subinterval_refl _
contains := by
intro n
exact RatInterval.point_sound q
modulus := fun _ => 0
width_modulus := by
intro ε
simpa [RatInterval.width, RatInterval.point] using ε.2.le
def neg unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CertifiedReal
Negating a certified name negates every rational enclosure and preserves its modulus.
Definition (Lean source)
def neg (x : CertifiedReal) : CertifiedReal where
value := -x.value
approx := fun n => (x.approx n).neg
nested := by
intro n
exact RatInterval.neg_mono (x.nested n)
contains := by
intro n
exact RatInterval.neg_sound (x.contains n)
modulus := x.modulus
width_modulus := by
intro ε
simpa [RatInterval.width_neg] using x.width_modulus ε
def add unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CertifiedReal
Adding certified names adds equal-precision interval enclosures and uses half of the requested tolerance for each input.
Definition (Lean source)
def add (x y : CertifiedReal) : CertifiedReal where
value := x.value + y.value
approx := fun n => RatInterval.add (x.approx n) (y.approx n)
nested := by
intro n
exact RatInterval.add_mono (x.nested n) (y.nested n)
contains := by
intro n
exact RatInterval.add_sound (x.contains n) (y.contains n)
modulus := fun ε =>
max (x.modulus ⟨ε.1 / 2, div_pos ε.2 (by decide)⟩)
(y.modulus ⟨ε.1 / 2, div_pos ε.2 (by decide)⟩)
width_modulus := by
intro ε
let δ : PosRat := ⟨ε.1 / 2, div_pos ε.2 (by norm_num)⟩
have hx : (x.approx (max (x.modulus δ) (y.modulus δ))).width ≤ δ.1 :=
(RatInterval.width_mono (x.approx_mono (le_max_left _ _))).trans
(x.width_modulus δ)
have hy : (y.approx (max (x.modulus δ) (y.modulus δ))).width ≤ δ.1 :=
(RatInterval.width_mono (y.approx_mono (le_max_right _ _))).trans
(y.width_modulus δ)
rw [RatInterval.width_add]
dsimp [δ] at hx hy ⊢
linarith
def sub unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CertifiedReal
Subtracting certified names adds the first enclosure to the negation of the second.
Definition (Lean source)
5 supporting declarations (lemmas, instances)
-
approx_monotheorem — Nestedness extends from successive precisions to every pair of ordered precisions.Proof (Lean source)
theorem approx_mono (x : CertifiedReal) {m n : ℕ} (hmn : m ≤ n) : (x.approx n).Subinterval (x.approx m) := by induction n, hmn using Nat.le_induction with | base => exact RatInterval.subinterval_refl _ | succ n hmn ih => exact RatInterval.subinterval_trans (x.nested n) ih -
refine_containstheorem — Refinement always encloses the real value named by the certificate.Proof (Lean source)
theorem refine_contains (x : CertifiedReal) (ε : PosRat) : (x.refine ε).Contains x.value := by exact x.contains (x.modulus ε) -
exists_refinementtheorem — Every positive rational tolerance admits an explicitly returned enclosing interval of at most that width.hypothesesconclusion∃ n : ℕ, (x.approx n).Contains x.value ∧ (x.approx n).width ≤ εProof (Lean source)
theorem exists_refinement (x : CertifiedReal) (ε : ℚ) (hε : 0 < ε) : ∃ n : ℕ, (x.approx n).Contains x.value ∧ (x.approx n).width ≤ ε := by exact ⟨x.modulus ⟨ε, hε⟩, x.contains _, x.width_modulus ⟨ε, hε⟩⟩ -
sub_valuetheorem — Certified subtraction denotes the difference of the two named real values.Proof (Lean source)
-
value_eq_of_common_approximationstheorem — Two certified names whose every approximation is shared denote the same real value.Proof (Lean source)
theorem value_eq_of_common_approximations (x y : CertifiedReal) (hxy : ∀ n, x.approx n = y.approx n) : x.value = y.value := by apply le_antisymm · by_contra h have hlt : y.value < x.value := lt_of_not_ge h obtain ⟨ε, hεpos, hεlt⟩ : ∃ ε : ℚ, 0 < ε ∧ (ε : ℝ) < x.value - y.value := by exact exists_pos_rat_lt (sub_pos.mpr hlt) let n := x.modulus ⟨ε, hεpos⟩ have hx := x.contains n have hy : (x.approx n).Contains y.value := by simpa [hxy n] using y.contains n have hw : ((x.approx n).width : ℝ) ≤ ε := by exact_mod_cast x.width_modulus ⟨ε, hεpos⟩ have hspan : x.value - y.value ≤ ((x.approx n).width : ℝ) := by simp only [RatInterval.width, Rat.cast_sub] linarith [hx.2, hy.1] exact (not_lt_of_ge (hspan.trans hw)) hεlt · by_contra h have hlt : x.value < y.value := lt_of_not_ge h obtain ⟨ε, hεpos, hεlt⟩ : ∃ ε : ℚ, 0 < ε ∧ (ε : ℝ) < y.value - x.value := by exact exists_pos_rat_lt (sub_pos.mpr hlt) let n := x.modulus ⟨ε, hεpos⟩ have hx := x.contains n have hy : (x.approx n).Contains y.value := by simpa [hxy n] using y.contains n have hw : ((x.approx n).width : ℝ) ≤ ε := by exact_mod_cast x.width_modulus ⟨ε, hεpos⟩ have hspan : y.value - x.value ≤ ((x.approx n).width : ℝ) := by simp only [RatInterval.width, Rat.cast_sub] linarith [hy.2, hx.1] exact (not_lt_of_ge (hspan.trans hw)) hεlt
Mesh 19 core · 10 supporting 19 to review This module provides rational rectangles for complex values and finite uniform mesh enclosures for the infimum and supremum of a real function. ★ infEnclosure_sound
Certified finite mesh extrema
This module provides rational rectangles for complex values and finite uniform mesh enclosures for the infimum and supremum of a real function. A supplied Lipschitz bound turns rational node enclosures into global enclosures with an explicit mesh-error allowance.
structure ComplexRatInterval unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic
A rational rectangle in the complex plane consists of a rational interval enclosing the real coordinate and a rational interval enclosing the imaginary coordinate.
Definition (Lean source)
fields
The rational interval enclosing the real coordinate.
re :
The rational interval enclosing the imaginary coordinate.
im :
def Contains unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.ComplexRatInterval
A complex number belongs to a rational rectangle when both coordinates belong to their intervals.
Definition (Lean source)
def Contains (I : ComplexRatInterval) (z : ℂ) : Prop :=
I.re.Contains z.re ∧ I.im.Contains z.im
def Subinterval unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.ComplexRatInterval
Coordinatewise inclusion is the refinement relation for complex rational rectangles.
Definition (Lean source)
def Subinterval (I J : ComplexRatInterval) : Prop :=
I.re.Subinterval J.re ∧ I.im.Subinterval J.im
def add unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.ComplexRatInterval
Complex rectangle addition is rational interval addition in both coordinates.
Definition (Lean source)
def add (I J : ComplexRatInterval) : ComplexRatInterval :=
⟨I.re.add J.re, I.im.add J.im⟩
def smulRat unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.ComplexRatInterval
Multiplication by a rational scalar uses real interval multiplication in both coordinates.
Definition (Lean source)
def smulRat (q : ℚ) (I : ComplexRatInterval) : ComplexRatInterval :=
⟨(RatInterval.point q).mul I.re, (RatInterval.point q).mul I.im⟩
def expand unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.ComplexRatInterval
Coordinatewise widening by a nonnegative rational error produces a larger rectangle.
Definition (Lean source)
def expand (I : ComplexRatInterval) (e : ℚ) (he : 0 ≤ e) : ComplexRatInterval :=
⟨I.re.expand e he, I.im.expand e he⟩
def zero unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.ComplexRatInterval
The point rectangle at complex zero is the neutral enclosure for finite recursive sums.
Definition (Lean source)
def zero : ComplexRatInterval := ⟨RatInterval.point 0, RatInterval.point 0⟩
def meshPoint unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
A uniform mesh node divides its whole-number position by the positive mesh size on the unit parameter interval.
Definition (Lean source)
noncomputable def meshPoint (n k : ℕ) : ℝ := (k : ℝ) / n
def circleMap unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The standard once-around parameterization of a circle with a specified center and nonnegative radius.
def circleTangent unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The derivative of the standard unit-interval circle parameterization.
def circleIntegrand unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The parameterized contour integrand is the function value times the circle tangent.
Definition (Lean source)
noncomputable def circleIntegrand (f : ℂ → ℂ) (c : ℂ) (r : ℝ) (u : ℝ) : ℂ :=
f (circleMap c r u) * circleTangent r u
def circleContourIntegral unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The contour integral around a circle is represented deterministically as an interval integral over one unit-length parameter cycle.
Definition (Lean source)
noncomputable def circleContourIntegral (f : ℂ → ℂ) (c : ℂ) (r : ℝ) : ℂ :=
∫ u in (0 : ℝ)..1, circleIntegrand f c r u
def minLoUpTo unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The minimum lower endpoint among the nodes from the initial node through the requested terminal node is computed by primitive recursion.
Definition (Lean source)
def minLoUpTo (nodes : ℕ → RatInterval) : ℕ → ℚ
| 0 => (nodes 0).lo
| n + 1 => min (minLoUpTo nodes n) (nodes (n + 1)).lo
def minHiUpTo unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The minimum upper endpoint among the nodes from the initial node through the requested terminal node is computed by primitive recursion.
Definition (Lean source)
def minHiUpTo (nodes : ℕ → RatInterval) : ℕ → ℚ
| 0 => (nodes 0).hi
| n + 1 => min (minHiUpTo nodes n) (nodes (n + 1)).hi
def maxLoUpTo unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The maximum lower endpoint among the nodes from the initial node through the requested terminal node is computed by primitive recursion.
Definition (Lean source)
def maxLoUpTo (nodes : ℕ → RatInterval) : ℕ → ℚ
| 0 => (nodes 0).lo
| n + 1 => max (maxLoUpTo nodes n) (nodes (n + 1)).lo
def maxHiUpTo unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The maximum upper endpoint among the nodes from the initial node through the requested terminal node is computed by primitive recursion.
Definition (Lean source)
def maxHiUpTo (nodes : ℕ → RatInterval) : ℕ → ℚ
| 0 => (nodes 0).hi
| n + 1 => max (maxHiUpTo nodes n) (nodes (n + 1)).hi
def infEnclosure unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The infimum enclosure widens the minimum node enclosure downward by one Lipschitz mesh step.
Definition (Lean source)
def infEnclosure (nodes : ℕ → RatInterval) (L : ℚ) (hL : 0 ≤ L)
(n : ℕ) (hn : 0 < n) : RatInterval :=
⟨minLoUpTo nodes n - L / n, minHiUpTo nodes n, by
have hdiv : 0 ≤ L / (n : ℚ) := div_nonneg hL (by positivity)
linarith [minEndpoints_le nodes n]⟩
def supEnclosure unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The supremum enclosure widens the maximum node enclosure upward by one Lipschitz mesh step.
Definition (Lean source)
def supEnclosure (nodes : ℕ → RatInterval) (L : ℚ) (hL : 0 ≤ L)
(n : ℕ) (hn : 0 < n) : RatInterval :=
⟨maxLoUpTo nodes n, maxHiUpTo nodes n + L / n, by
have hdiv : 0 ≤ L / (n : ℚ) := div_nonneg hL (by positivity)
linarith [maxEndpoints_le nodes n]⟩
theorem infEnclosure_sound unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
Certified infimum enclosure on the unit mesh. Fix a nonnegative Lipschitz constant and a positive number of mesh nodes, and suppose the real function is Lipschitz on [0, 1] with that constant and each rational node interval contains the function's value at the corresponding mesh point. Then the infimum enclosure built from those node intervals contains the true infimum of the function over [0, 1].
Formal statement
hypotheses
f :
ℝ → ℝ
nodes :
ℕ → RatInterval
L :
ℚ
hL :
0 ≤ L
n :
ℕ
hn :
0 < n
hLip :
∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1, |f s - f t| ≤ (L : ℝ) * |s - t|
hnodes :
∀ k ≤ n, (nodes k).Contains (f (meshPoint n k))
conclusion
(infEnclosure nodes L hL n hn).Contains (sInf (f '' Icc (0 : ℝ) 1))
Proof (Lean source)
theorem infEnclosure_sound {f : ℝ → ℝ} {nodes : ℕ → RatInterval}
{L : ℚ} (hL : 0 ≤ L) {n : ℕ} (hn : 0 < n)
(hLip : ∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1,
|f s - f t| ≤ (L : ℝ) * |s - t|)
(hnodes : ∀ k ≤ n, (nodes k).Contains (f (meshPoint n k))) :
(infEnclosure nodes L hL n hn).Contains (sInf (f '' Icc (0 : ℝ) 1)) := by
have hL' : (0 : ℝ) ≤ L := by exact_mod_cast hL
have hcont : ContinuousOn f (Icc (0 : ℝ) 1) :=
continuousOn_of_lipschitz_bound hL' (by simpa [Real.norm_eq_abs] using hLip)
have hbdd : BddBelow (f '' Icc (0 : ℝ) 1) := isCompact_Icc.bddBelow_image hcont
have hne : (f '' Icc (0 : ℝ) 1).Nonempty :=
⟨f 0, ⟨0, ⟨le_rfl, zero_le_one⟩, rfl⟩⟩
constructor
· simp only [infEnclosure, RatInterval.Contains, Rat.cast_sub, Rat.cast_div,
Rat.cast_natCast]
apply le_csInf hne
rintro y ⟨x, hx, rfl⟩
obtain ⟨k, hk, hdist⟩ := exists_near_meshPoint hn hx
have hm := hnodes k hk
have hmesh := meshPoint_mem hn hk
have hlip := hLip x hx (meshPoint n k) hmesh
have hLo : ((minLoUpTo nodes n : ℚ) : ℝ) ≤ (nodes k).lo := by
exact_mod_cast minLoUpTo_le nodes hk
have : f (meshPoint n k) - (L : ℝ) / n ≤ f x := by
have hdist' : |x - meshPoint n k| ≤ (n : ℝ)⁻¹ := by
simpa [one_div] using hdist
have habs : |f x - f (meshPoint n k)| ≤ (L : ℝ) / n :=
by simpa [div_eq_mul_inv] using
hlip.trans (mul_le_mul_of_nonneg_left hdist' hL')
linarith [neg_le_of_abs_le habs]
linarith [hm.1]
· simp only [infEnclosure, RatInterval.Contains]
obtain ⟨k, hk, heq⟩ := exists_minHiUpTo nodes n
have hs : sInf (f '' Icc (0 : ℝ) 1) ≤ f (meshPoint n k) :=
csInf_le hbdd ⟨meshPoint n k, meshPoint_mem hn hk, rfl⟩
have hhi := (hnodes k hk).2
rw [heq]
exact hs.trans hhi
10 supporting declarations (lemmas, instances)
-
exttheorem∀ {x y : ComplexRatInterval}, x.re = y.re → x.im = y.im → x = yProof (Lean source)
@[ext] -
ext_ifftheorem∀ {x y : ComplexRatInterval}, x = y ↔ x.re = y.re ∧ x.im = y.imProof (Lean source)
@[ext] -
add_soundtheorem — Complex rectangle addition encloses sums of enclosed complex numbers.hypothesesconclusion(I.add J).Contains (z + w)Proof (Lean source)
theorem add_sound {I J : ComplexRatInterval} {z w : ℂ} (hz : I.Contains z) (hw : J.Contains w) : (I.add J).Contains (z + w) := by exact ⟨RatInterval.add_sound hz.1 hw.1, RatInterval.add_sound hz.2 hw.2⟩ -
smulRat_soundtheorem — Rational scalar multiplication encloses the corresponding complex scalar multiple.hypothesesconclusion(smulRat q I).Contains ((q : ℂ) * z)Proof (Lean source)
theorem smulRat_sound {I : ComplexRatInterval} {z : ℂ} (q : ℚ) (hz : I.Contains z) : (smulRat q I).Contains ((q : ℂ) * z) := by constructor · simpa [smulRat] using RatInterval.mul_sound (RatInterval.point_sound q) hz.1 · simpa [smulRat] using RatInterval.mul_sound (RatInterval.point_sound q) hz.2 -
expand_containstheorem — Coordinatewise widening preserves containment.hypothesesconclusion(I.expand e he).Contains zProof (Lean source)
theorem expand_contains {I : ComplexRatInterval} {z : ℂ} {e : ℚ} (he : 0 ≤ e) (hz : I.Contains z) : (I.expand e he).Contains z := by have he' : (0 : ℝ) ≤ e := by exact_mod_cast he constructor <;> constructor <;> simp only [expand, RatInterval.expand, RatInterval.Contains, Rat.cast_sub, Rat.cast_add] <;> linarith [hz.1.1, hz.1.2, hz.2.1, hz.2.2] -
meshPoint_memtheorem — A node of a nonempty uniform mesh lies in the unit parameter interval.Proof (Lean source)
theorem meshPoint_mem {n k : ℕ} (hn : 0 < n) (hk : k ≤ n) : meshPoint n k ∈ Icc (0 : ℝ) 1 := by constructor · exact div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _) · rw [meshPoint, div_le_one (by exact_mod_cast hn)] exact_mod_cast hk -
continuousOn_of_lipschitz_boundtheorem — A function satisfying a finite Lipschitz bound on the unit interval is continuous there.hypothesesE :C :ℝhC :0 ≤ Ch :∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1, ‖g s - g t‖ ≤ C * |s - t|conclusionContinuousOn g (Icc (0 : ℝ) 1)Proof (Lean source)
theorem continuousOn_of_lipschitz_bound {E : Type*} [NormedAddCommGroup E] {g : ℝ → E} {C : ℝ} (hC : 0 ≤ C) (h : ∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1, ‖g s - g t‖ ≤ C * |s - t|) : ContinuousOn g (Icc (0 : ℝ) 1) := by intro x hx rw [Metric.continuousWithinAt_iff] intro ε hε refine ⟨ε / (C + 1), div_pos hε (by linarith), ?_⟩ intro y hy hyx change ‖y - x‖ < ε / (C + 1) at hyx rw [dist_eq_norm] rw [Real.norm_eq_abs] at hyx by_cases hC0 : C = 0 · have hzle : ‖g y - g x‖ ≤ 0 := by simpa [hC0] using h y hy x hx exact (le_antisymm hzle (norm_nonneg _)).trans_lt hε calc ‖g y - g x‖ ≤ C * |y - x| := h y hy x hx _ < C * (ε / (C + 1)) := by exact mul_lt_mul_of_pos_left hyx (lt_of_le_of_ne hC (Ne.symm hC0)) _ < ε := by rw [mul_div_assoc'] exact (div_lt_iff₀ (by linarith : 0 < C + 1)).2 (by nlinarith) -
supEnclosure_soundtheorem — Rational node enclosures and a Lipschitz bound enclose the supremum of a real function on the unit mesh interval.hypothesesf :ℝ → ℝnodes :ℕ → RatIntervalL :ℚhL :0 ≤ Ln :ℕhn :0 < nhLip :∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1, |f s - f t| ≤ (L : ℝ) * |s - t|hnodes :∀ k ≤ n, (nodes k).Contains (f (meshPoint n k))conclusion(supEnclosure nodes L hL n hn).Contains (sSup (f '' Icc (0 : ℝ) 1))Proof (Lean source)
theorem supEnclosure_sound {f : ℝ → ℝ} {nodes : ℕ → RatInterval} {L : ℚ} (hL : 0 ≤ L) {n : ℕ} (hn : 0 < n) (hLip : ∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1, |f s - f t| ≤ (L : ℝ) * |s - t|) (hnodes : ∀ k ≤ n, (nodes k).Contains (f (meshPoint n k))) : (supEnclosure nodes L hL n hn).Contains (sSup (f '' Icc (0 : ℝ) 1)) := by have hL' : (0 : ℝ) ≤ L := by exact_mod_cast hL have hcont : ContinuousOn f (Icc (0 : ℝ) 1) := continuousOn_of_lipschitz_bound hL' (by simpa [Real.norm_eq_abs] using hLip) have hbdd : BddAbove (f '' Icc (0 : ℝ) 1) := isCompact_Icc.bddAbove_image hcont have hne : (f '' Icc (0 : ℝ) 1).Nonempty := ⟨f 0, ⟨0, ⟨le_rfl, zero_le_one⟩, rfl⟩⟩ constructor · simp only [supEnclosure, RatInterval.Contains] obtain ⟨k, hk, heq⟩ := exists_maxLoUpTo nodes n have hs : f (meshPoint n k) ≤ sSup (f '' Icc (0 : ℝ) 1) := le_csSup hbdd ⟨meshPoint n k, meshPoint_mem hn hk, rfl⟩ have hlo := (hnodes k hk).1 rw [heq] exact hlo.trans hs · simp only [supEnclosure, RatInterval.Contains, Rat.cast_add, Rat.cast_div, Rat.cast_natCast] apply csSup_le hne rintro y ⟨x, hx, rfl⟩ obtain ⟨k, hk, hdist⟩ := exists_near_meshPoint hn hx have hm := hnodes k hk have hmesh := meshPoint_mem hn hk have hlip := hLip x hx (meshPoint n k) hmesh have hHi : ((nodes k).hi : ℝ) ≤ maxHiUpTo nodes n := by exact_mod_cast hi_le_maxHiUpTo nodes hk have hdist' : |x - meshPoint n k| ≤ (n : ℝ)⁻¹ := by simpa [one_div] using hdist have habs : |f x - f (meshPoint n k)| ≤ (L : ℝ) / n := by simpa [div_eq_mul_inv] using hlip.trans (mul_le_mul_of_nonneg_left hdist' hL') linarith [hm.2, le_abs_self (f x - f (meshPoint n k))] -
width_infEnclosuretheorem — The infimum enclosure width is at most one mesh error plus the uniform node-enclosure width.hypothesesnodes :ℕ → RatIntervalw L :ℚhw :0 ≤ whL :0 ≤ Ln :ℕhn :0 < nhnodes :∀ k ≤ n, (nodes k).width ≤ wconclusion(infEnclosure nodes L hL n hn).width ≤ w + L / nProof (Lean source)
theorem width_infEnclosure {nodes : ℕ → RatInterval} {w L : ℚ} (hw : 0 ≤ w) (hL : 0 ≤ L) {n : ℕ} (hn : 0 < n) (hnodes : ∀ k ≤ n, (nodes k).width ≤ w) : (infEnclosure nodes L hL n hn).width ≤ w + L / n := by obtain ⟨k, hk, heq⟩ := exists_minLoUpTo nodes n have hhi := minHiUpTo_le nodes hk have hwk := hnodes k hk simp only [infEnclosure, RatInterval.width] rw [heq] unfold RatInterval.width at hwk linarith -
width_supEnclosuretheorem — The supremum enclosure width is at most one mesh error plus the uniform node-enclosure width.hypothesesnodes :ℕ → RatIntervalw L :ℚhw :0 ≤ whL :0 ≤ Ln :ℕhn :0 < nhnodes :∀ k ≤ n, (nodes k).width ≤ wconclusion(supEnclosure nodes L hL n hn).width ≤ w + L / nProof (Lean source)
theorem width_supEnclosure {nodes : ℕ → RatInterval} {w L : ℚ} (hw : 0 ≤ w) (hL : 0 ≤ L) {n : ℕ} (hn : 0 < n) (hnodes : ∀ k ≤ n, (nodes k).width ≤ w) : (supEnclosure nodes L hL n hn).width ≤ w + L / n := by obtain ⟨k, hk, heq⟩ := exists_maxHiUpTo nodes n have hlo := lo_le_maxLoUpTo nodes hk have hwk := hnodes k hk simp only [supEnclosure, RatInterval.width] rw [heq] unfold RatInterval.width at hwk linarith
Exponential 10 core · 6 supporting 10 to review This module computes nested rational intervals for the exponential of a rational input. ★ expScalar_width
Certified rational exponential enclosures
This module computes nested rational intervals for the exponential of a rational input. Range reduction, Taylor bounds, and an explicit precision rule yield a certified real name whose returned interval meets every positive rational error target.
def expScale unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The integer scaling factor reduces a rational exponential argument to absolute value at most one.
def expReduced unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The reduced exponential argument divides by its positive natural scaling factor.
Definition (Lean source)
def expReduced (q : ℚ) : ℚ := q / (expScale q : ℚ)
def expPartial unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The rational Taylor polynomial for the exponential retains all terms through the requested degree.
Definition (Lean source)
def expPartial (q : ℚ) (n : ℕ) : ℚ :=
∑ k ∈ range (n + 1), q ^ k / (k.factorial : ℚ)
def expRemainder unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The rational remainder radius is the explicit exponential-series bound after the retained Taylor terms.
Definition (Lean source)
def expRemainder (q : ℚ) (n : ℕ) : ℚ :=
|q| ^ (n + 1) * ((n + 2 : ℕ) : ℚ) /
(((n + 1).factorial : ℚ) * (n + 1 : ℕ))
def expReducedRaw unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
A reduced rational argument is enclosed by its Taylor polynomial plus or minus the rational remainder radius.
Definition (Lean source)
def expReducedRaw (q : ℚ) (n : ℕ) : RatInterval :=
⟨expPartial q n - expRemainder q n,
expPartial q n + expRemainder q n, by
have hr : 0 ≤ expRemainder q n := by
simp only [expRemainder]
positivity
linarith⟩
def expRaw unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The raw exponential enclosure raises the reduced-argument enclosure to the exact scaling power.
Definition (Lean source)
def expScalar unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
Successive exponential enclosures are intersected to make the returned sequence nested.
Definition (Lean source)
def expScalar (q : ℚ) : ℕ → RatInterval
| 0 => expRaw q 0
| n + 1 => RatInterval.tighten (expScalar q n) (expRaw q (n + 1))
def expPrecision unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The explicit exponential precision is a natural function of the rational input and target width.
Definition (Lean source)
theorem expScalar_width unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
For a rational input q and a requested positive rational tolerance ε, evaluating the certified scalar exponential at the precision level selected for that tolerance yields an enclosure whose width is no larger than ε.
Formal statement
Proof (Lean source)
theorem expScalar_width (q : ℚ) (ε : PosRat) :
(expScalar q (expPrecision q ε)).width ≤ ε.1 := by
let D : ℕ := ε.1.den
let s : ℕ := expScale q
let N : ℕ := expPrecision q ε
let z : ℚ := expReduced q
let R : ℚ := expRemainder z N
let I : RatInterval := expReducedRaw z N
have hD : 0 < D := by simpa [D] using ε.1.den_pos
have hs : 0 < s := by
dsimp [s, expScale]
omega
have hN : 1 ≤ N := by
dsimp [N, expPrecision, D, s]
exact Nat.mul_pos (Nat.mul_pos (Nat.succ_pos _) (Nat.succ_pos _)) (Nat.succ_pos _)
have hz : |z| ≤ 1 := by simpa [z] using abs_expReduced_le_one q
have hz0 : 0 ≤ |z| := abs_nonneg z
have hzpow (k : ℕ) : |z| ^ k ≤ 1 := pow_le_one₀ hz0 hz
have hpartial : |expPartial z N| ≤ 3 := by
calc
|expPartial z N| ≤
∑ k ∈ range (N + 1), |z ^ k / (k.factorial : ℚ)| := by
simpa [expPartial] using
Finset.abs_sum_le_sum_abs (s := range (N + 1))
(f := fun k => z ^ k / (k.factorial : ℚ))
_ ≤ ∑ k ∈ range (N + 1), (1 / k.factorial : ℚ) := by
gcongr with k hk
rw [abs_div, abs_pow, abs_of_nonneg (by positivity : (0 : ℚ) ≤ k.factorial)]
exact div_le_div_of_nonneg_right (hzpow k) (by positivity)
_ = 1 + ∑ k ∈ range (N + 1) with 1 ≤ k,
(1 / k.factorial : ℚ) := by
rw [← Finset.sum_filter_add_sum_filter_not (s := range (N + 1))
(p := fun k => 1 ≤ k) (f := fun k => (1 / k.factorial : ℚ))]
simp [add_comm]
_ ≤ 3 := by
linarith [Complex.sum_div_factorial_le (α := ℚ) 1 (N + 1) (by omega)]
have hfac1 : (1 : ℕ) ≤ N.factorial := by
exact Nat.factorial_pos N
have hrem : R ≤ 1 := by
have hnum : |z| ^ (N + 1) * ((N + 2 : ℕ) : ℚ) ≤
((N + 1).factorial : ℚ) * (N + 1 : ℕ) := by
have hfac1Q : (1 : ℚ) ≤ N.factorial := by exact_mod_cast hfac1
have hNQ : (1 : ℚ) ≤ N := by exact_mod_cast hN
have hsq : ((N + 2 : ℕ) : ℚ) ≤ (N + 1 : ℚ) * (N + 1 : ℚ) := by
push_cast
nlinarith
calc
|z| ^ (N + 1) * ((N + 2 : ℕ) : ℚ) ≤ ((N + 2 : ℕ) : ℚ) := by
nlinarith [hzpow (N + 1)]
_ ≤ (N + 1 : ℚ) * (N + 1 : ℚ) := hsq
_ ≤ ((N + 1).factorial : ℚ) * (N + 1 : ℕ) := by
rw [Nat.factorial_succ]
push_cast
have haux : 0 ≤ ((N.factorial : ℚ) - 1) * (N + 1 : ℚ) ^ 2 :=
mul_nonneg (sub_nonneg.mpr hfac1Q) (sq_nonneg _)
nlinarith
dsimp [R, expRemainder]
exact (div_le_one (by positivity)).2 hnum
have hR0 : 0 ≤ R := by
dsimp [R, expRemainder]
positivity
have hIwidth : I.width = 2 * R := by
simp [I, expReducedRaw, RatInterval.width, R]
ring
have hImax : I.maxAbs ≤ 4 := by
dsimp [I, expReducedRaw, RatInterval.maxAbs]
apply max_le
· calc
|expPartial z N - R| ≤ |expPartial z N| + |R| := abs_sub _ _
_ = |expPartial z N| + R := by rw [abs_of_nonneg hR0]
_ ≤ 4 := by linarith
· calc
|expPartial z N + R| ≤ |expPartial z N| + |R| := abs_add_le _ _
_ = |expPartial z N| + R := by rw [abs_of_nonneg hR0]
_ ≤ 4 := by linarith
have hNlarge : D + 3 * s ≤ N := by
have hsum : D + 1 + (s + 1) * (s + 1) ≤ N := by
dsimp [N, expPrecision]
change D + 1 + (s + 1) * (s + 1) ≤ (D + 1) * (s + 1) * (s + 1)
rw [mul_assoc]
apply add_le_mul
· omega
· nlinarith
have hsquare : 3 * s ≤ 1 + (s + 1) * (s + 1) := by nlinarith
omega
have hpowbound : D * s * 4 ^ s ≤ 2 ^ N := by
calc
D * s * 4 ^ s ≤ 2 ^ D * 2 ^ s * 4 ^ s := by
exact Nat.mul_le_mul (Nat.mul_le_mul (nat_le_two_pow D) (nat_le_two_pow s)) le_rfl
_ = 2 ^ (D + 3 * s) := by
rw [show 4 = 2 ^ 2 by norm_num, ← pow_mul, ← pow_add, ← pow_add]
congr 1
omega
_ ≤ 2 ^ N := Nat.pow_le_pow_right (by omega) hNlarge
have hfactorial : D * s * 4 ^ s ≤ (N + 1).factorial := by
exact hpowbound.trans (by
simpa [Nat.add_comm] using
(@Nat.factorial_mul_pow_le_factorial 1 N))
have hfactorialQ : (D : ℚ) * s * 4 ^ s ≤ ((N + 1).factorial : ℚ) := by
exact_mod_cast hfactorial
have hRfac : R * ((N + 1).factorial : ℚ) ≤ 2 := by
have heq : R * ((N + 1).factorial : ℚ) =
|z| ^ (N + 1) * ((N + 2 : ℕ) : ℚ) / (N + 1 : ℕ) := by
dsimp [R, expRemainder]
field_simp
rw [heq]
norm_num [Nat.cast_add]
apply (div_le_iff₀ (by positivity : (0 : ℚ) < N + 1)).2
nlinarith [hzpow (N + 1)]
have hscaled : (D : ℚ) * s * 4 ^ s * R ≤ 2 := by
calc
(D : ℚ) * s * 4 ^ s * R ≤ ((N + 1).factorial : ℚ) * R := by
exact mul_le_mul_of_nonneg_right hfactorialQ hR0
_ = R * ((N + 1).factorial : ℚ) := by ring
_ ≤ 2 := hRfac
have hraw : (expRaw q N).width ≤ 1 / (D : ℚ) := by
have hp := interval_npow_width_le I s
have hI0 : 0 ≤ I.maxAbs := (abs_nonneg I.lo).trans (le_max_left _ _)
have hpow4 : I.maxAbs ^ (s - 1) ≤ (4 : ℚ) ^ (s - 1) :=
pow_le_pow_left₀ hI0 hImax _
have hbound : (s : ℚ) * I.maxAbs ^ (s - 1) * I.width ≤
(s : ℚ) * 4 ^ (s - 1) * (2 * R) := by
rw [hIwidth]
gcongr
have hDq : (0 : ℚ) < D := by exact_mod_cast hD
have hsform : (4 : ℚ) ^ s = 4 * 4 ^ (s - 1) := by
calc
(4 : ℚ) ^ s = 4 ^ (s - 1 + 1) := by congr 1 <;> omega
_ = 4 ^ (s - 1) * 4 := pow_succ _ _
_ = 4 * 4 ^ (s - 1) := mul_comm _ _
have hfinal : (s : ℚ) * 4 ^ (s - 1) * (2 * R) ≤ 1 / D := by
apply (le_div_iff₀ hDq).2
rw [hsform] at hscaled
nlinarith
simpa [expRaw, I, s] using hp.trans (hbound.trans hfinal)
calc
(expScalar q (expPrecision q ε)).width ≤ (expRaw q N).width := by
apply RatInterval.width_mono
simpa [N] using expScalar_subinterval_raw q N
_ ≤ 1 / (D : ℚ) := hraw
_ ≤ ε.1 := by
simpa [D] using inv_den_le_of_pos ε.1 ε.2
def expName unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
A rational exponential is a certified real with a fully rational endpoint algorithm.
Definition (Lean source)
noncomputable def expName (q : ℚ) : CertifiedReal where
value := exp (q : ℝ)
approx := expScalar q
nested := expScalar_nested q
contains := expScalar_sound q
modulus := expPrecision q
width_modulus := expScalar_width q
6 supporting declarations (lemmas, instances)
-
abs_expReduced_le_onetheorem — Range reduction puts the exponential Taylor argument in the closed unit interval.Proof (Lean source)
theorem abs_expReduced_le_one (q : ℚ) : |expReduced q| ≤ 1 := by have hsN : 0 < expScale q := lt_of_lt_of_le Nat.zero_lt_one (le_max_left _ _) have hs : (0 : ℚ) < expScale q := by exact_mod_cast hsN have hnum : |q| ≤ (q.num.natAbs : ℚ) := by have hd : (0 : ℚ) < q.den := by exact_mod_cast q.den_pos calc |q| = |(q.num : ℚ) / (q.den : ℚ)| := by rw [Rat.num_div_den] _ = (q.num.natAbs : ℚ) / q.den := by rw [abs_div, abs_of_pos hd] norm_num _ ≤ (q.num.natAbs : ℚ) := by apply (div_le_iff₀ hd).2 have hd1 : (1 : ℚ) ≤ q.den := by exact_mod_cast q.den_pos nlinarith rw [expReduced, abs_div, abs_of_pos hs] apply (div_le_iff₀ hs).2 have hscale : (q.num.natAbs : ℚ) ≤ expScale q := by exact_mod_cast (le_max_right 1 q.num.natAbs) simpa only [one_mul] using hnum.trans hscale -
expRaw_soundtheorem — The raw rational exponential interval encloses the real exponential of the rational input.Proof (Lean source)
theorem expRaw_sound (q : ℚ) (n : ℕ) : (expRaw q n).Contains (exp (q : ℝ)) := by let z := expReduced q have hzR : |(z : ℝ)| ≤ 1 := by exact_mod_cast abs_expReduced_le_one q have hb := Real.exp_bound hzR (n := n + 1) (Nat.succ_pos n) have hp : ((expPartial z n : ℚ) : ℝ) = ∑ k ∈ range (n + 1), (z : ℝ) ^ k / (k.factorial : ℝ) := by simp [expPartial] have hr : ((expRemainder z n : ℚ) : ℝ) = |(z : ℝ)| ^ (n + 1) * ((n + 2 : ℕ) : ℝ) / (((n + 1).factorial : ℝ) * (n + 1 : ℕ)) := by simp [expRemainder] rw [← hp] at hb have hb' : |exp (z : ℝ) - (expPartial z n : ℝ)| ≤ (expRemainder z n : ℝ) := by rw [hr] convert hb using 1 <;> norm_num [Nat.cast_succ] <;> ring have hred : (expReducedRaw z n).Contains (exp (z : ℝ)) := by rw [abs_le] at hb' simp only [expReducedRaw, RatInterval.Contains, Rat.cast_sub, Rat.cast_add] constructor <;> linarith [hb'.1, hb'.2] have hpow := RatInterval.npow_sound hred (expScale q) have hs : (expScale q : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt (lt_of_lt_of_le Nat.zero_lt_one (le_max_left 1 q.num.natAbs))) have hq : (q : ℝ) = (expScale q : ℝ) * (z : ℝ) := by dsimp [z, expReduced] push_cast field_simp [hs] simpa [expRaw, ← Real.exp_nat_mul, hq] using hpow -
expScalar_soundtheorem — Every tightened scalar exponential interval encloses the real exponential.Proof (Lean source)
theorem expScalar_sound (q : ℚ) (n : ℕ) : (expScalar q n).Contains (exp (q : ℝ)) := by induction n with | zero => exact expRaw_sound q 0 | succ n ih => exact RatInterval.tighten_sound ih (expRaw_sound q (n + 1)) -
expScalar_nestedtheorem — Scalar exponential enclosures are nested as precision increases.Proof (Lean source)
theorem expScalar_nested (q : ℚ) (n : ℕ) : (expScalar q (n + 1)).Subinterval (expScalar q n) := by exact RatInterval.tighten_subinterval_left (expScalar_sound q n) (expRaw_sound q (n + 1)) -
tighten_subinterval_righttheorem — Tightening two enclosures of the same real value is contained in either input enclosure.hypothesesconclusion(RatInterval.tighten I J).Subinterval JProof (Lean source)
theorem tighten_subinterval_right {I J : RatInterval} {x : ℝ} (hI : I.Contains x) (hJ : J.Contains x) : (RatInterval.tighten I J).Subinterval J := by have hlohi : max I.lo J.lo ≤ min I.hi J.hi := by apply max_le · apply le_min I.lo_le_hi exact_mod_cast hI.1.trans hJ.2 · apply le_min · exact_mod_cast hJ.1.trans hI.2 · exact J.lo_le_hi simp only [RatInterval.tighten, hlohi, dif_pos, RatInterval.Subinterval] exact ⟨le_max_right _ _, min_le_right _ _⟩ -
inv_den_le_of_postheorem — The reciprocal of a positive rational's denominator is no larger than the rational itself.hypothesesu :ℚhu :0 < uconclusion1 / (u.den : ℚ) ≤ uProof (Lean source)
theorem inv_den_le_of_pos (u : ℚ) (hu : 0 < u) : 1 / (u.den : ℚ) ≤ u := by have hnum0 : 0 ≤ u.num := Rat.num_nonneg.mpr hu.le have hnumne : u.num ≠ 0 := by intro h have hu0 : u = 0 := by rw [← Rat.num_div_den u, h] simp linarith have hnum1 : (1 : ℚ) ≤ u.num := by exact_mod_cast (lt_of_le_of_ne hnum0 (Ne.symm hnumne)) calc 1 / (u.den : ℚ) ≤ (u.num : ℚ) / u.den := div_le_div_of_nonneg_right hnum1 (by positivity) _ = u := Rat.num_div_den u
Quadrature 4 core · 3 supporting 4 to review This module turns complex rational node rectangles on a uniform mesh into a sound enclosure of an interval integral. ★ integralEnclosure_sound
Certified trapezoidal contour quadrature
This module turns complex rational node rectangles on a uniform mesh into a sound enclosure of an interval integral. The deterministic trapezoidal rule is widened by an explicit Lipschitz error, and the result specializes to a circle contour through its standard parameterization.
def trapezoidSum unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The unscaled trapezoidal rectangle sum is computed by primitive recursion over mesh cells.
Definition (Lean source)
def trapezoidSum (nodes : ℕ → ComplexRatInterval) : ℕ → ComplexRatInterval
| 0 => ComplexRatInterval.zero
| n + 1 => ComplexRatInterval.add (trapezoidSum nodes n)
(ComplexRatInterval.add (nodes n) (nodes (n + 1)))
def trapezoidEnclosure unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The rational complex trapezoidal enclosure applies the usual half-cell average and mesh scaling to the recursive endpoint sum.
Definition (Lean source)
def trapezoidEnclosure (nodes : ℕ → ComplexRatInterval) (n : ℕ) : ComplexRatInterval :=
ComplexRatInterval.smulRat (1 / (2 * n : ℚ)) (trapezoidSum nodes n)
def integralEnclosure unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
The certified contour enclosure widens the rational trapezoidal enclosure by its Lipschitz discretization error.
Definition (Lean source)
def integralEnclosure (nodes : ℕ → ComplexRatInterval) (L : ℚ) (hL : 0 ≤ L)
(n : ℕ) (hn : 0 < n) : ComplexRatInterval :=
(trapezoidEnclosure nodes n).expand (L / (2 * n)) (by positivity)
theorem integralEnclosure_sound unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.CircleMesh
Certified trapezoidal enclosure of an integral. Fix a nonnegative Lipschitz constant and a positive node count, and suppose the complex-valued integrand is Lipschitz on [0, 1] with that constant and each complex rational rectangle contains the integrand's value at the corresponding mesh point. Then the trapezoidal enclosure built from those rectangles contains the true integral of the integrand over [0, 1].
Formal statement
hypotheses
g :
ℝ → ℂ
nodes :
L :
ℚ
hL :
0 ≤ L
n :
ℕ
hn :
0 < n
hLip :
∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1, ‖g s - g t‖ ≤ (L : ℝ) * |s - t|
hnodes :
∀ k ≤ n, (nodes k).Contains (g (meshPoint n k))
conclusion
(integralEnclosure nodes L hL n hn).Contains (∫ u in (0 : ℝ)..1, g u)
Proof (Lean source)
theorem integralEnclosure_sound {g : ℝ → ℂ} {nodes : ℕ → ComplexRatInterval}
{L : ℚ} (hL : 0 ≤ L) {n : ℕ} (hn : 0 < n)
(hLip : ∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1,
‖g s - g t‖ ≤ (L : ℝ) * |s - t|)
(hnodes : ∀ k ≤ n, (nodes k).Contains (g (meshPoint n k))) :
(integralEnclosure nodes L hL n hn).Contains (∫ u in (0 : ℝ)..1, g u) := by
let T : ℂ := (1 / (2 * n : ℝ)) * ∑ k ∈ range n,
(g (meshPoint n k) + g (meshPoint n (k + 1)))
have hsum := trapezoidSum_sound (N := n) n hnodes
have hT : (trapezoidEnclosure nodes n).Contains T := by
unfold trapezoidEnclosure T
convert ComplexRatInterval.smulRat_sound (1 / (2 * n : ℚ)) hsum using 1 <;>
norm_num [Nat.cast_mul]
have herr : ‖(∫ u in (0 : ℝ)..1, g u) - T‖ ≤ (L : ℝ) / (2 * n) := by
exact norm_integral_sub_trapezoid_le hL hn hLip
unfold integralEnclosure
apply expand_contains_of_norm_sub (he := by positivity) hT
simpa [Rat.cast_div, Rat.cast_natCast] using herr
3 supporting declarations (lemmas, instances)
-
norm_integral_sub_trapezoid_letheorem — A Lipschitz complex function on the unit parameter interval differs from its deterministic trapezoidal rule by at most half a Lipschitz mesh unit.hypothesesg :ℝ → ℂL :ℚhL :0 ≤ Ln :ℕhn :0 < nhLip :∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1, ‖g s - g t‖ ≤ (L : ℝ) * |s - t|Proof (Lean source)
theorem norm_integral_sub_trapezoid_le {g : ℝ → ℂ} {L : ℚ} (hL : 0 ≤ L) {n : ℕ} (hn : 0 < n) (hLip : ∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1, ‖g s - g t‖ ≤ (L : ℝ) * |s - t|) : ‖(∫ u in (0 : ℝ)..1, g u) - ((1 / (2 * n : ℝ)) * ∑ k ∈ range n, (g (meshPoint n k) + g (meshPoint n (k + 1))))‖ ≤ (L : ℝ) / (2 * n) := by have hL' : (0 : ℝ) ≤ L := by exact_mod_cast hL have hn' : (0 : ℝ) < n := by exact_mod_cast hn have hcont : ContinuousOn g (Icc (0 : ℝ) 1) := continuousOn_of_lipschitz_bound hL' hLip have hcell : ∀ k < n, ‖(∫ u in meshPoint n k..meshPoint n (k + 1), g u) - (1 / (2 * n : ℝ)) * (g (meshPoint n k) + g (meshPoint n (k + 1)))‖ ≤ (L : ℝ) / (2 * n * n) := by intro k hk let a := meshPoint n k let b := meshPoint n (k + 1) have hka : k ≤ n := (le_of_lt hk) have hkb : k + 1 ≤ n := hk have hab : a ≤ b := meshPoint_mono hn k.le_succ have ha : a ∈ Icc (0 : ℝ) 1 := meshPoint_mem hn hka have hb : b ∈ Icc (0 : ℝ) 1 := meshPoint_mem hn hkb have hgi : IntervalIntegrable g volume a b := (hcont.mono (by rw [uIcc_of_le hab] intro x hx exact ⟨ha.1.trans hx.1, hx.2.trans hb.2⟩)).intervalIntegrable have hp : ∀ u ∈ uIcc a b, ‖g u - ((1 / 2 : ℝ) : ℂ) * (g a + g b)‖ ≤ (L : ℝ) / (2 * n) := by intro u hu rw [uIcc_of_le hab] at hu have huI : u ∈ Icc (0 : ℝ) 1 := ⟨ha.1.trans hu.1, hu.2.trans hb.2⟩ have hla := hLip u huI a ha have hlb := hLip u huI b hb have hdist : |u - a| + |u - b| = b - a := by rw [abs_of_nonneg (sub_nonneg.mpr hu.1), abs_of_nonpos (sub_nonpos.mpr hu.2)] ring have halg : g u - ((1 / 2 : ℝ) : ℂ) * (g a + g b) = ((1 / 2 : ℝ) : ℂ) * (g u - g a) + ((1 / 2 : ℝ) : ℂ) * (g u - g b) := by norm_num ring rw [halg] calc ‖((1 / 2 : ℝ) : ℂ) * (g u - g a) + ((1 / 2 : ℝ) : ℂ) * (g u - g b)‖ ≤ ‖((1 / 2 : ℝ) : ℂ) * (g u - g a)‖ + ‖((1 / 2 : ℝ) : ℂ) * (g u - g b)‖ := norm_add_le _ _ _ = (1 / 2 : ℝ) * ‖g u - g a‖ + (1 / 2 : ℝ) * ‖g u - g b‖ := by simp [norm_mul] _ ≤ (1 / 2 : ℝ) * ((L : ℝ) * |u - a|) + (1 / 2 : ℝ) * ((L : ℝ) * |u - b|) := by gcongr _ = (L : ℝ) / 2 * (b - a) := by rw [← hdist]; ring _ = (L : ℝ) / (2 * n) := by rw [show b - a = 1 / (n : ℝ) by exact meshPoint_succ_sub hn] ring have hbound : ‖∫ u in a..b, (g u - ((1 / 2 : ℝ) : ℂ) * (g a + g b))‖ ≤ ((L : ℝ) / (2 * n)) * |b - a| := intervalIntegral.norm_integral_le_of_norm_le_const (by intro u hu apply hp u rw [uIcc_of_le hab] rw [show Ι a b = Ioc a b from uIoc_of_le hab] at hu exact ⟨le_of_lt hu.1, hu.2⟩) have hrewrite : (∫ u in a..b, g u) - (1 / (2 * n : ℝ)) * (g a + g b) = ∫ u in a..b, (g u - ((1 / 2 : ℝ) : ℂ) * (g a + g b)) := by have hscale : (1 / (2 * n : ℝ)) * (g a + g b) = (1 / (n : ℝ)) • (((1 / 2 : ℝ) : ℂ) * (g a + g b)) := by rw [Complex.real_smul] push_cast field_simp rw [intervalIntegral.integral_sub hgi intervalIntegrable_const, intervalIntegral.integral_const] rw [show b - a = 1 / (n : ℝ) by exact meshPoint_succ_sub hn] rw [hscale] rw [hrewrite] calc ‖∫ u in a..b, (g u - ((1 / 2 : ℝ) : ℂ) * (g a + g b))‖ ≤ ((L : ℝ) / (2 * n)) * |b - a| := hbound _ = (L : ℝ) / (2 * n * n) := by rw [show b - a = 1 / (n : ℝ) by exact meshPoint_succ_sub hn, abs_of_nonneg (by positivity)] ring rw [sum_cell_integrals hn hcont, Finset.mul_sum, ← Finset.sum_sub_distrib] calc _ ≤ ∑ k ∈ range n, ‖(∫ u in meshPoint n k..meshPoint n (k + 1), g u) - (1 / (2 * n : ℝ)) * (g (meshPoint n k) + g (meshPoint n (k + 1)))‖ := by convert norm_sum_le _ _ using 1 <;> norm_num [Nat.cast_mul] _ ≤ ∑ _k ∈ range n, (L : ℝ) / (2 * n * n) := by gcongr with k hk exact hcell k (Finset.mem_range.mp hk) _ = (L : ℝ) / (2 * n) := by simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul] field_simp -
integralEnclosure_widththeorem — Each coordinate width of the certified integral is bounded by the uniform node width plus one mesh-scale Lipschitz allowance.hypothesesnodes :w L :ℚhw :0 ≤ whL :0 ≤ Ln :ℕhn :0 < nhnodes :∀ k ≤ n, (nodes k).re.width ≤ w ∧ (nodes k).im.width ≤ wconclusion(integralEnclosure nodes L hL n hn).re.width ≤ w + L / n ∧(integralEnclosure nodes L hL n hn).im.width ≤ w + L / nProof (Lean source)
theorem integralEnclosure_width {nodes : ℕ → ComplexRatInterval} {w L : ℚ} (hw : 0 ≤ w) (hL : 0 ≤ L) {n : ℕ} (hn : 0 < n) (hnodes : ∀ k ≤ n, (nodes k).re.width ≤ w ∧ (nodes k).im.width ≤ w) : (integralEnclosure nodes L hL n hn).re.width ≤ w + L / n ∧ (integralEnclosure nodes L hL n hn).im.width ≤ w + L / n := by have hs := width_trapezoidSum hw hnodes have hq : (0 : ℚ) ≤ 1 / (2 * n : ℚ) := by positivity have hscale := width_smulRat_of_nonneg (trapezoidSum nodes n) hq have htre : (trapezoidEnclosure nodes n).re.width ≤ w := by rw [trapezoidEnclosure, hscale.1] calc (1 / (2 * n : ℚ)) * (trapezoidSum nodes n).re.width ≤ (1 / (2 * n : ℚ)) * (2 * n * w) := mul_le_mul_of_nonneg_left hs.1 hq _ = w := by field_simp have htim : (trapezoidEnclosure nodes n).im.width ≤ w := by rw [trapezoidEnclosure, hscale.2] calc (1 / (2 * n : ℚ)) * (trapezoidSum nodes n).im.width ≤ (1 / (2 * n : ℚ)) * (2 * n * w) := mul_le_mul_of_nonneg_left hs.2 hq _ = w := by field_simp have herr : L / (2 * n : ℚ) + L / (2 * n : ℚ) = L / n := by field_simp ring unfold RatInterval.width at htre htim constructor <;> simp only [integralEnclosure, ComplexRatInterval.expand, RatInterval.expand, RatInterval.width] <;> linarith [herr] -
circleContourIntegral_enclosedtheorem — Applying the complex mesh theorem to the parameterized circle integrand encloses the contour integral.hypothesesf :ℂ → ℂc :ℂr :ℝnodes :L :ℚhL :0 ≤ Ln :ℕhn :0 < nhLip :∀ s ∈ Icc (0 : ℝ) 1,∀ t ∈ Icc (0 : ℝ) 1,‖circleIntegrand f c r s - circleIntegrand f c r t‖ ≤ (L : ℝ) * |s - t|hnodes :∀ k ≤ n, (nodes k).Contains (circleIntegrand f c r (meshPoint n k))conclusion(integralEnclosure nodes L hL n hn).Contains (circleContourIntegral f c r)Proof (Lean source)
theorem circleContourIntegral_enclosed {f : ℂ → ℂ} {c : ℂ} {r : ℝ} {nodes : ℕ → ComplexRatInterval} {L : ℚ} (hL : 0 ≤ L) {n : ℕ} (hn : 0 < n) (hLip : ∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1, ‖circleIntegrand f c r s - circleIntegrand f c r t‖ ≤ (L : ℝ) * |s - t|) (hnodes : ∀ k ≤ n, (nodes k).Contains (circleIntegrand f c r (meshPoint n k))) : (integralEnclosure nodes L hL n hn).Contains (circleContourIntegral f c r) := by exact integralEnclosure_sound hL hn hLip hnodes
API 2 core · 0 supporting 2 to review This module collects exact rational interval arithmetic, certified-real refinement, transcendental interval extensions, finite mesh enclosures, and total measurable finite searches into one paper-independent interface.
Packaged certified contour interval arithmetic
This module collects exact rational interval arithmetic, certified-real refinement, transcendental interval extensions, finite mesh enclosures, and total measurable finite searches into one paper-independent interface.
structure CertifiedIntervalArithmetic unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic
This interface packages sound rational interval arithmetic and total certified-real refinement behind a paper-independent interface.
Definition (Lean source)
fields
The packaged outward addition operation.
add :
Packaged addition encloses sums of enclosed real operands.
add_sound :
∀ {I J : RatInterval} {x y : ℝ}
if
I.Contains x
and
J.Contains y
then
(add I J).Contains (x + y)
The packaged outward subtraction operation.
sub :
Packaged subtraction encloses differences of enclosed real operands.
sub_sound :
∀ {I J : RatInterval} {x y : ℝ}
if
I.Contains x
and
J.Contains y
then
(sub I J).Contains (x - y)
The packaged outward multiplication operation.
mul :
Packaged multiplication encloses products of enclosed real operands.
mul_sound :
∀ {I J : RatInterval} {x y : ℝ}
if
I.Contains x
and
J.Contains y
then
(mul I J).Contains (x * y)
The packaged outward division operation requires a denominator interval
separated from zero.
div :
(I J : RatInterval) → J.AwayFromZero → RatInterval
Packaged division encloses quotients of enclosed operands away from zero.
div_sound :
∀ {I J : RatInterval} {x y : ℝ} (hJ : J.AwayFromZero)
if
I.Contains x
and
J.Contains y
then
(div I J hJ).Contains (x / y)
The packaged outward exponential extension at a requested natural precision.
exp :
RatInterval → ℕ → RatInterval
Packaged exponential evaluation encloses exponentials of enclosed reals.
exp_sound :
∀ {I : RatInterval} {x : ℝ}
if
I.Contains x
then
∀ n, (exp I n).Contains (exp x)
The packaged outward logarithm extension requires a strictly positive interval.
log :
(I : RatInterval) → 0 < I.lo → ℕ → RatInterval
Packaged logarithm evaluation encloses logarithms on a certified positive interval.
log_sound :
∀ {I : RatInterval} {x : ℝ} (hI : 0 < I.lo)
if
I.Contains x
then
∀ n, (log I hI n).Contains (log x)
The packaged real-power extension requires a strictly positive base interval.
rpow :
(base exponent : RatInterval) → 0 < base.lo → ℕ → RatInterval
Packaged real-power evaluation encloses real powers on the positive-base domain.
rpow_sound :
∀ {base exponent : RatInterval} {x y : ℝ} (hbase : 0 < base.lo)
if
base.Contains x
and
exponent.Contains y
then
∀ n, (rpow base exponent hbase n).Contains (x ^ y)
The packaged total refinement operation for certified real names.
refine :
Packaged refinement preserves enclosure of the named real value.
refine_contains :
∀ (x : CertifiedReal) (ε : PosRat), (refine x ε).Contains x.value
Packaged refinement returns no more than the requested rational width.
refine_width :
∀ (x : CertifiedReal) (ε : PosRat), (refine x ε).width ≤ ε.1
def certifiedIntervalArithmetic unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic
The concrete certified interval arithmetic implementation uses exact rational primitives, rational Taylor/atanh enclosures, and stored effective moduli for certified real refinement.
Definition (Lean source)
def certifiedIntervalArithmetic : CertifiedIntervalArithmetic where
add := RatInterval.add
add_sound := RatInterval.add_sound
sub := RatInterval.sub
sub_sound := RatInterval.sub_sound
mul := RatInterval.mul
mul_sound := RatInterval.mul_sound
div := RatInterval.div
div_sound := RatInterval.div_sound
exp := Transcendental.expInterval
exp_sound := by
intro I x hx n
exact Transcendental.expInterval_sound hx n
log := Transcendental.logInterval
log_sound := by
intro I x hI hx n
exact Transcendental.logInterval_sound hI hx n
rpow := Transcendental.rpowInterval
rpow_sound := by
intro base exponent x y hbase hx hy n
exact Transcendental.rpowInterval_sound hbase hx hy n
refine := CertifiedReal.refine
refine_contains := CertifiedReal.refine_contains
refine_width := CertifiedReal.refine_width
FiniteSearch 4 core · 13 supporting 4 to review This module provides the finite control flow used by certified numerical procedures. ★ measurable_leastScoreIndex
Total finite searches, deterministic ties, and measurability
This module provides the finite control flow used by certified numerical procedures. It returns a least successful candidate with an explicit fallback, breaks equal real scores by index, and proves that the resulting finite outputs are Borel measurable.
def leastTrue unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.FiniteSearch
The least successful index of a nonempty finite Boolean family is returned, or zero if none succeeds.
def finiteRefine unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.FiniteSearch
Finite refinement returns the first candidate interval meeting a rational width tolerance, with a total fallback.
Definition (Lean source)
def finiteRefine {n : ℕ} (candidates : Fin (n + 1) → RatInterval) (ε : PosRat) :
RatInterval :=
candidates (leastTrue fun i => decide ((candidates i).width ≤ ε.1))
def leastScoreIndex unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.FiniteSearch
The least-score index minimizes lexicographically by real score and then by the original finite index.
Definition (Lean source)
noncomputable def leastScoreIndex {n : ℕ} (score : Fin (n + 1) → ℝ) : Fin (n + 1) := by
classical
let keys : Finset (ℝ ×ₗ Fin (n + 1)) :=
Finset.univ.image (fun i => toLex (score i, i))
have hkeys : keys.Nonempty := by
refine ⟨toLex (score 0, 0), ?_⟩
exact Finset.mem_image.mpr ⟨0, Finset.mem_univ _, rfl⟩
exact (ofLex (keys.min' hkeys)).2
theorem measurable_leastScoreIndex unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.FiniteSearch
For a sample-size index n, the function that selects, from a vector of n+1 real scores, the smallest index attaining the least score is measurable with respect to the Borel σ-algebra on the score vector space and the discrete σ-algebra on the finite index set.
Formal statement
Proof (Lean source)
theorem measurable_leastScoreIndex {n : ℕ} :
Measurable (leastScoreIndex : (Fin (n + 1) → ℝ) → Fin (n + 1)) := by
apply measurable_to_countable'
intro i
have hmeas : MeasurableSet {score : Fin (n + 1) → ℝ |
∀ j, score i < score j ∨ (score i = score j ∧ i ≤ j)} := by
rw [show {score : Fin (n + 1) → ℝ |
∀ j, score i < score j ∨ (score i = score j ∧ i ≤ j)} =
⋂ j, {score | score i < score j ∨ (score i = score j ∧ i ≤ j)} by
ext score
simp]
apply MeasurableSet.iInter
intro j
apply MeasurableSet.union
· exact measurableSet_lt (measurable_pi_apply i) (measurable_pi_apply j)
· apply MeasurableSet.inter
· exact measurableSet_eq_fun (measurable_pi_apply i) (measurable_pi_apply j)
· exact MeasurableSet.const _
rw [show (leastScoreIndex : (Fin (n + 1) → ℝ) → Fin (n + 1)) ⁻¹' {i} =
{score | ∀ j, score i < score j ∨ (score i = score j ∧ i ≤ j)} by
ext score
simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_setOf_eq]
constructor
· intro hselected j
have hmin := leastScoreIndex_minimal score j
rw [hselected] at hmin
rcases lt_or_eq_of_le hmin with hlt | heq
· exact inl hlt
· exact inr ⟨heq, by
have htie := leastScoreIndex_tie score (i := j) (by
rw [hselected]
exact heq.symm)
rwa [hselected] at htie⟩
· intro hall
let k := leastScoreIndex score
have hik : i ≤ k := by
rcases hall k with hlt | heq
· exact elim ((not_lt_of_ge (leastScoreIndex_minimal score i)) hlt)
· exact heq.2
have hki : k ≤ i := by
apply leastScoreIndex_tie score
rcases hall k with hlt | heq
· exact elim ((not_lt_of_ge (leastScoreIndex_minimal score i)) hlt)
· exact heq.1
exact le_antisymm hki hik]
exact hmeas
13 supporting declarations (lemmas, instances)
-
instMeasurableSpaceRatIntervalinstance — Rational intervals carry the countable discrete measurable space used for certified outputs.instance : MeasurableSpace RatInterval := ⊤ -
instMeasurableSpaceComplexRatIntervalinstance — Complex rational rectangles carry the countable discrete measurable space used for certified outputs.instance : MeasurableSpace ComplexRatInterval := ⊤ -
leastTrue_acceptstheorem — When at least one Boolean test succeeds, the returned index succeeds.hypothesesProof (Lean source)
theorem leastTrue_accepts {n : ℕ} {accept : Fin (n + 1) → Bool} (h : ∃ i, accept i = true) : accept (leastTrue accept) = true := by unfold leastTrue split_ifs with hne · have hm := Finset.min'_mem (Finset.univ.filter fun i => accept i) hne exact (Finset.mem_filter.mp hm).2 · obtain ⟨i, hi⟩ := h exfalso apply hne refine ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ i, ?_⟩⟩ exact hi -
leastTrue_letheorem — Every successful index is no smaller than the successful index returned by the search.Proof (Lean source)
theorem leastTrue_le {n : ℕ} {accept : Fin (n + 1) → Bool} {i : Fin (n + 1)} (hi : accept i = true) : leastTrue accept ≤ i := by unfold leastTrue split_ifs with hne · apply Finset.min'_le exact Finset.mem_filter.mpr ⟨Finset.mem_univ i, hi⟩ · exfalso apply hne exact ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ i, hi⟩⟩ -
leastTrue_eq_zerotheorem — If no Boolean test succeeds, the total search returns index zero. -
finiteRefine_widththeorem — If a candidate meets the requested width, finite refinement returns the least such candidate and meets the width.hypothesesconclusion(finiteRefine candidates ε).width ≤ ε.1Proof (Lean source)
theorem finiteRefine_width {n : ℕ} {candidates : Fin (n + 1) → RatInterval} (ε : PosRat) (h : ∃ i, (candidates i).width ≤ ε.1) : (finiteRefine candidates ε).width ≤ ε.1 := by unfold finiteRefine apply of_decide_eq_true apply leastTrue_accepts (accept := fun i => decide ((candidates i).width ≤ ε.1)) obtain ⟨i, hi⟩ := h refine ⟨i, ?_⟩ rw [decide_eq_true_eq] exact hi -
measurable_finiteRefinetheorem — Finite refinement is measurable as a function of a finite vector of rational interval candidates.hypothesesn :ℕε :conclusionProof (Lean source)
theorem measurable_finiteRefine {n : ℕ} (ε : PosRat) : Measurable (fun candidates : Fin (n + 1) → RatInterval => finiteRefine candidates ε) := by letI : Countable RatInterval := countable_ratInterval exact fun s _ => (Set.to_countable _).measurableSet -
leastScoreIndex_minimaltheorem — The selected least-score index has score no larger than every competing score.hypothesesconclusionscore (leastScoreIndex score) ≤ score iProof (Lean source)
theorem leastScoreIndex_minimal {n : ℕ} (score : Fin (n + 1) → ℝ) (i : Fin (n + 1)) : score (leastScoreIndex score) ≤ score i := by classical let keys : Finset (ℝ ×ₗ Fin (n + 1)) := Finset.univ.image (fun j => toLex (score j, j)) have hkeys : keys.Nonempty := by refine ⟨toLex (score 0, 0), ?_⟩ exact Finset.mem_image.mpr ⟨0, Finset.mem_univ _, rfl⟩ have hm := Finset.min'_mem keys hkeys obtain ⟨j, -, hj⟩ := Finset.mem_image.mp hm have hselected : leastScoreIndex score = j := by rw [leastScoreIndex] change (ofLex (keys.min' hkeys)).2 = j rw [← hj] rfl rw [hselected] have hle := Finset.min'_le keys (toLex (score i, i)) (Finset.mem_image.mpr ⟨i, Finset.mem_univ _, rfl⟩) rw [← hj] at hle exact le_of_not_gt fun hgt => by have hlex : toLex (score i, i) < toLex (score j, j) := Prod.Lex.left _ _ hgt exact (not_lt_of_ge hle) hlex -
leastScoreIndex_tietheorem — Equal minimal scores are resolved in favor of the smaller original index.hypothesesconclusionleastScoreIndex score ≤ iProof (Lean source)
theorem leastScoreIndex_tie {n : ℕ} (score : Fin (n + 1) → ℝ) {i : Fin (n + 1)} (hi : score i = score (leastScoreIndex score)) : leastScoreIndex score ≤ i := by classical let keys : Finset (ℝ ×ₗ Fin (n + 1)) := Finset.univ.image (fun j => toLex (score j, j)) have hkeys : keys.Nonempty := by refine ⟨toLex (score 0, 0), ?_⟩ exact Finset.mem_image.mpr ⟨0, Finset.mem_univ _, rfl⟩ have hm := Finset.min'_mem keys hkeys obtain ⟨j, -, hj⟩ := Finset.mem_image.mp hm have hselected : leastScoreIndex score = j := by rw [leastScoreIndex] change (ofLex (keys.min' hkeys)).2 = j rw [← hj] rfl rw [hselected] at hi ⊢ have hle := Finset.min'_le keys (toLex (score i, i)) (Finset.mem_image.mpr ⟨i, Finset.mem_univ _, rfl⟩) rw [← hj] at hle exact le_of_not_gt fun hgt => by have hlex : toLex (score i, i) < toLex (score j, j) := by rw [hi] exact Prod.Lex.right _ hgt exact (not_lt_of_ge hle) hlex -
measurable_leastTruetheorem — A finite least-success search is measurable when every individual success event is measurable.hypothesesconclusionMeasurable (fun ω => leastTrue (fun i => accept i ω))Proof (Lean source)
theorem measurable_leastTrue {Ω : Type*} [MeasurableSpace Ω] {n : ℕ} (accept : Fin (n + 1) → Ω → Bool) (haccept : ∀ i, Measurable (accept i)) : Measurable (fun ω => leastTrue (fun i => accept i ω)) := by have hvector : Measurable (fun ω => fun i => accept i ω) := measurable_pi_lambda _ haccept apply (show Measurable (leastTrue : (Fin (n + 1) → Bool) → Fin (n + 1)) from ?_).comp hvector exact fun s _ => (Set.to_countable _).measurableSet -
measurable_infEnclosuretheorem — The rational infimum enclosure is measurable as a function of its finite rational node vector.hypothesesn :ℕhn :0 < nL :ℚhL :0 ≤ LconclusionMeasurable (fun nodes : Fin (n + 1) → RatInterval => CircleMesh.infEnclosure (fun k => if hk : k < n + 1 then nodes ⟨k, hk⟩ else nodes 0) L hL n hn)Proof (Lean source)
theorem measurable_infEnclosure {n : ℕ} (hn : 0 < n) (L : ℚ) (hL : 0 ≤ L) : Measurable (fun nodes : Fin (n + 1) → RatInterval => CircleMesh.infEnclosure (fun k => if hk : k < n + 1 then nodes ⟨k, hk⟩ else nodes 0) L hL n hn) := by letI : Countable RatInterval := countable_ratInterval exact fun s _ => (Set.to_countable _).measurableSet -
measurable_supEnclosuretheorem — The rational supremum enclosure is measurable as a function of its finite rational node vector.hypothesesn :ℕhn :0 < nL :ℚhL :0 ≤ LconclusionMeasurable (fun nodes : Fin (n + 1) → RatInterval => CircleMesh.supEnclosure (fun k => if hk : k < n + 1 then nodes ⟨k, hk⟩ else nodes 0) L hL n hn)Proof (Lean source)
theorem measurable_supEnclosure {n : ℕ} (hn : 0 < n) (L : ℚ) (hL : 0 ≤ L) : Measurable (fun nodes : Fin (n + 1) → RatInterval => CircleMesh.supEnclosure (fun k => if hk : k < n + 1 then nodes ⟨k, hk⟩ else nodes 0) L hL n hn) := by letI : Countable RatInterval := countable_ratInterval exact fun s _ => (Set.to_countable _).measurableSet -
measurable_integralEnclosuretheorem — The rational complex integral enclosure is measurable as a function of its finite node rectangles.hypothesesn :ℕhn :0 < nL :ℚhL :0 ≤ LconclusionMeasurable (fun nodes : Fin (n + 1) → ComplexRatInterval => CircleMesh.integralEnclosure (fun k => if hk : k < n + 1 then nodes ⟨k, hk⟩ else nodes 0) L hL n hn)Proof (Lean source)
theorem measurable_integralEnclosure {n : ℕ} (hn : 0 < n) (L : ℚ) (hL : 0 ≤ L) : Measurable (fun nodes : Fin (n + 1) → ComplexRatInterval => CircleMesh.integralEnclosure (fun k => if hk : k < n + 1 then nodes ⟨k, hk⟩ else nodes 0) L hL n hn) := by letI : Countable ComplexRatInterval := countable_complexRatInterval exact fun s _ => (Set.to_countable _).measurableSet
Logarithm 8 core · 4 supporting 8 to review This module computes nested rational intervals for the logarithm of a positive rational input. ★ logScalar_width
Certified rational logarithm enclosures
This module computes nested rational intervals for the logarithm of a positive rational input. The atanh series and an explicit geometric remainder bound produce a certified real name with a computable precision for every positive rational error target.
def logCoordinate unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The atanh coordinate sends every positive rational logarithm argument into the open interval from minus one to one.
Definition (Lean source)
def logCoordinate (q : ℚ) : ℚ := (q - 1) / (q + 1)
def logPartial unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The rational logarithm polynomial retains the first requested number of terms of twice the atanh series.
Definition (Lean source)
def logPartial (q : ℚ) (n : ℕ) : ℚ :=
2 * ∑ k ∈ range (n + 1),
(logCoordinate q) ^ (2 * k + 1) / ((2 * k + 1 : ℕ) : ℚ)
def logRemainder unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The rational logarithm remainder bounds the tail of the atanh series geometrically.
Definition (Lean source)
def logRemainder (q : ℚ) (n : ℕ) : ℚ :=
2 * |logCoordinate q| ^ (2 * n + 3) /
(((2 * n + 3 : ℕ) : ℚ) * (1 - |logCoordinate q| ^ 2))
def logRaw unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
A positive rational logarithm argument is enclosed by its atanh polynomial plus or minus its tail bound.
Definition (Lean source)
def logRaw (q : ℚ) (hq : 0 < q) (n : ℕ) : RatInterval :=
⟨logPartial q n - logRemainder q n,
logPartial q n + logRemainder q n, by
have hz := abs_logCoordinate_lt_one_aux q hq
have hsquare : |logCoordinate q| ^ 2 < 1 := by
nlinarith [mul_self_lt_mul_self (abs_nonneg (logCoordinate q)) hz]
have hd : 0 < 1 - |logCoordinate q| ^ 2 := sub_pos.mpr hsquare
have hr : 0 ≤ logRemainder q n := by
simp only [logRemainder]
positivity
linarith⟩
def logScalar unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
Successive positive-logarithm enclosures are intersected to make the sequence nested.
Definition (Lean source)
def logScalar (q : ℚ) (hq : 0 < q) : ℕ → RatInterval
| 0 => logRaw q hq 0
| n + 1 => RatInterval.tighten (logScalar q hq n) (logRaw q hq (n + 1))
def logPrecision unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The explicit logarithm precision is a natural function of the input numerator, denominator, and target width.
Definition (Lean source)
def logPrecision (q : ℚ) (ε : PosRat) : ℕ :=
(ε.1.den + 1) * (q.num.natAbs + q.den + 1) * (q.num.natAbs + q.den + 1)
theorem logScalar_width unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
Precision-driven logarithm enclosure width. For a positive rational number and a requested positive rational tolerance, evaluating the scalar logarithm enclosure at the precision level determined from those two inputs produces an interval no wider than the requested tolerance.
Formal statement
Proof (Lean source)
theorem logScalar_width (q : ℚ) (hq : 0 < q) (ε : PosRat) :
(logScalar q hq (logPrecision q ε)).width ≤ ε.1 := by
let D : ℚ := ε.1.den
let S : ℚ := q.num.natAbs + q.den + 1
let N : ℕ := logPrecision q ε
let r : ℚ := |logCoordinate q|
have hD : 1 ≤ D := by
dsimp [D]
exact_mod_cast ε.1.den_pos
have hS : 2 ≤ S := by
dsimp [S]
have ha : (0 : ℚ) ≤ q.num.natAbs := by positivity
have hb : (1 : ℚ) ≤ q.den := by exact_mod_cast q.den_pos
linarith
have hr0 : 0 ≤ r := by positivity
have hr1 : r < 1 := by simpa [r] using abs_logCoordinate_lt_one q hq
have hrpow : r ^ (2 * N + 3) ≤ 1 := by
exact pow_le_one₀ hr0 hr1.le
have hgap : 1 / S ≤ 1 - r ^ 2 := by
simpa [S, r] using logCoordinate_gap_lower q hq
have hSpos : 0 < S := lt_of_lt_of_le (by norm_num) hS
have hSgap : 1 ≤ S * (1 - r ^ 2) := by
simpa [mul_comm] using (div_le_iff₀ hSpos).mp hgap
have hN : (N : ℚ) = (D + 1) * S * S := by
dsimp [N, D, S, logPrecision]
push_cast
ring
have hden : 4 * D ≤ ((2 * N + 3 : ℕ) : ℚ) * (1 - r ^ 2) := by
have hgap0 : 0 ≤ 1 - r ^ 2 := by nlinarith [sq_nonneg r]
have hlarge := mul_le_mul_of_nonneg_left hSgap
(show 0 ≤ 2 * (D + 1) * S by positivity)
have hstep : 2 * (D + 1) * S ≤
(2 * (D + 1) * S * S) * (1 - r ^ 2) := by
nlinarith
push_cast
rw [hN]
nlinarith [mul_nonneg (show (0 : ℚ) ≤ 3 by norm_num) hgap0]
have hdenpos : 0 < ((2 * N + 3 : ℕ) : ℚ) * (1 - r ^ 2) := by
have : 0 < 1 - r ^ 2 := by nlinarith [sq_nonneg r]
positivity
have hraw : (logRaw q hq N).width ≤ ε.1 := by
have hnum : 4 * r ^ (2 * N + 3) ≤ 4 := by nlinarith
have hfrac : 4 * r ^ (2 * N + 3) /
(((2 * N + 3 : ℕ) : ℚ) * (1 - r ^ 2)) ≤ 1 / D := by
apply (div_le_div_iff₀ hdenpos (show 0 < D by linarith)).2
simpa only [one_mul] using
(mul_le_mul_of_nonneg_right hnum (show 0 ≤ D by linarith)).trans hden
calc
(logRaw q hq N).width =
4 * r ^ (2 * N + 3) /
(((2 * N + 3 : ℕ) : ℚ) * (1 - r ^ 2)) := by
simp [RatInterval.width, logRaw, logRemainder, r]
ring
_ ≤ 1 / D := hfrac
_ ≤ ε.1 := by simpa [D] using inv_den_le_of_pos ε.1 ε.2
exact (RatInterval.width_mono (logScalar_subinterval_raw q hq N)).trans hraw
def logName unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
The logarithm of a positive rational is a certified real with fully rational endpoints.
Definition (Lean source)
noncomputable def logName (q : ℚ) (hq : 0 < q) : CertifiedReal where
value := log (q : ℝ)
approx := logScalar q hq
nested := logScalar_nested q hq
contains := logScalar_sound q hq
modulus := logPrecision q
width_modulus := logScalar_width q hq
4 supporting declarations (lemmas, instances)
-
abs_logCoordinate_lt_onetheorem — A positive rational logarithm argument has atanh coordinate of absolute value strictly below one.Proof (Lean source)
theorem abs_logCoordinate_lt_one (q : ℚ) (hq : 0 < q) : |logCoordinate q| < 1 := by exact abs_logCoordinate_lt_one_aux q hq -
logRaw_soundtheorem — The raw rational logarithm interval encloses the real logarithm of its positive rational input.Proof (Lean source)
theorem logRaw_sound (q : ℚ) (hq : 0 < q) (n : ℕ) : (logRaw q hq n).Contains (log (q : ℝ)) := by let z := logCoordinate q have hz : |(z : ℝ)| < 1 := by exact_mod_cast abs_logCoordinate_lt_one q hq have hb := log_series_remainder_bound (z : ℝ) hz n have hratio : (1 + (z : ℝ)) / (1 - (z : ℝ)) = (q : ℝ) := by have hd : (q : ℝ) + 1 ≠ 0 := by positivity dsimp [z, logCoordinate] push_cast field_simp [hd] ring have hplus : (1 + (z : ℝ)) ≠ 0 := by have := (abs_lt.mp hz).1 linarith have hminus : (1 - (z : ℝ)) ≠ 0 := by have := (abs_lt.mp hz).2 linarith have hlog : log (q : ℝ) = log (1 + (z : ℝ)) - log (1 - (z : ℝ)) := by rw [← Real.log_div hplus hminus, hratio] have hp : ((logPartial q n : ℚ) : ℝ) = 2 * ∑ k ∈ range (n + 1), (z : ℝ) ^ (2 * k + 1) / (2 * k + 1 : ℕ) := by simp [logPartial, z] have hr : ((logRemainder q n : ℚ) : ℝ) = 2 * |(z : ℝ)| ^ (2 * n + 3) / ((2 * n + 3 : ℕ) * (1 - |(z : ℝ)| ^ 2)) := by simp [logRemainder, z] rw [← hlog, ← hp, ← hr] at hb rw [abs_le] at hb simp only [logRaw, RatInterval.Contains, Rat.cast_sub, Rat.cast_add] constructor <;> linarith [hb.1, hb.2] -
logScalar_soundtheorem — Every tightened scalar logarithm interval encloses the real logarithm.Proof (Lean source)
theorem logScalar_sound (q : ℚ) (hq : 0 < q) (n : ℕ) : (logScalar q hq n).Contains (log (q : ℝ)) := by induction n with | zero => exact logRaw_sound q hq 0 | succ n ih => exact RatInterval.tighten_sound ih (logRaw_sound q hq (n + 1)) -
logScalar_nestedtheorem — Scalar logarithm enclosures are nested as precision increases.hypothesesq :ℚhq :0 < qn :ℕProof (Lean source)
theorem logScalar_nested (q : ℚ) (hq : 0 < q) (n : ℕ) : (logScalar q hq (n + 1)).Subinterval (logScalar q hq n) := by exact RatInterval.tighten_subinterval_left (logScalar_sound q hq n) (logRaw_sound q hq (n + 1))
Operations 5 core · 5 supporting 5 to review This module lifts the certified scalar exponential and logarithm constructions to rational input intervals. ★ rpowInterval_sound
Transcendental interval extensions
This module lifts the certified scalar exponential and logarithm constructions to rational input intervals. It supplies sound and nested interval extensions for exponential, positive-domain logarithm, and positive-base real powers.
def expInterval unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
Exponential interval evaluation encloses the exponential of every real number contained in its input interval.
Definition (Lean source)
def expInterval (I : RatInterval) (n : ℕ) : RatInterval :=
⟨expIntervalLo I n, expIntervalHi I n, expInterval_wellFormed I n⟩
def logInterval unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
Positive logarithm interval evaluation encloses the logarithm of every real number contained in its certified positive input interval.
Definition (Lean source)
def logInterval (I : RatInterval) (hI : 0 < I.lo) (n : ℕ) : RatInterval :=
⟨(logScalar I.lo hI n).lo,
(logScalar I.hi (hI.trans_le I.lo_le_hi) n).hi,
logInterval_wellFormed I hI n⟩
def rpowRaw unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
Raw real-power evaluation on a strictly positive base composes logarithm, multiplication, and exponential interval evaluation.
Definition (Lean source)
def rpowRaw (base exponent : RatInterval) (hbase : 0 < base.lo) (n : ℕ) : RatInterval :=
expInterval (RatInterval.mul exponent (logInterval base hbase n)) n
def rpowInterval unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
Real-power interval evaluation tightens all raw evaluations up to the requested precision.
Definition (Lean source)
def rpowInterval (base exponent : RatInterval) (hbase : 0 < base.lo) :
ℕ → RatInterval
| 0 => rpowRaw base exponent hbase 0
| n + 1 => RatInterval.tighten (rpowInterval base exponent hbase n)
(rpowRaw base exponent hbase (n + 1))
theorem rpowInterval_sound unreviewed
⚑ flagged
Causalean.Mathlib.Analysis.CertifiedContourIntervalArithmetic.Transcendental
Certified real-power interval evaluation. For a base rational interval whose lower endpoint is strictly positive that encloses a real base value, and an exponent rational interval enclosing a real exponent value, the real-power interval evaluation of the base and exponent, at any precision level, contains the true value of the base raised to that exponent.
Formal statement
hypotheses
base exponent :
x y :
ℝ
hbase :
0 < base.lo
hx :
base.Contains x
hy :
exponent.Contains y
n :
ℕ
conclusion
(rpowInterval base exponent hbase n).Contains (x ^ y)
Proof (Lean source)
theorem rpowInterval_sound {base exponent : RatInterval} {x y : ℝ}
(hbase : 0 < base.lo) (hx : base.Contains x) (hy : exponent.Contains y) (n : ℕ) :
(rpowInterval base exponent hbase n).Contains (x ^ y) := by
induction n with
| zero => exact rpowRaw_sound hbase hx hy 0
| succ n ih => exact RatInterval.tighten_sound ih (rpowRaw_sound hbase hx hy (n + 1))
5 supporting declarations (lemmas, instances)
-
expInterval_soundtheorem — Exponential interval evaluation encloses the exponential of every enclosed real input.hypothesesconclusion(expInterval I n).Contains (exp x)Proof (Lean source)
theorem expInterval_sound {I : RatInterval} {x : ℝ} (hx : I.Contains x) (n : ℕ) : (expInterval I n).Contains (exp x) := by constructor · exact (expScalar_sound I.lo n).1.trans (Real.exp_monotone hx.1) · exact (Real.exp_monotone hx.2).trans (expScalar_sound I.hi n).2 -
logInterval_soundtheorem — Positive logarithm interval evaluation encloses the logarithm of every enclosed real input.hypothesesconclusion(logInterval I hI n).Contains (log x)Proof (Lean source)
theorem logInterval_sound {I : RatInterval} {x : ℝ} (hI : 0 < I.lo) (hx : I.Contains x) (n : ℕ) : (logInterval I hI n).Contains (log x) := by have hlo : (0 : ℝ) < I.lo := by exact_mod_cast hI have hxpos : 0 < x := (by exact_mod_cast hI : (0 : ℝ) < I.lo).trans_le hx.1 have hhipos : (0 : ℝ) < I.hi := hxpos.trans_le hx.2 constructor · exact (logScalar_sound I.lo hI n).1.trans (Real.strictMonoOn_log.monotoneOn hlo hxpos hx.1) · exact (Real.strictMonoOn_log.monotoneOn hxpos hhipos hx.2).trans (logScalar_sound I.hi (hI.trans_le I.lo_le_hi) n).2 -
expInterval_nestedtheorem — Exponential interval evaluation is nested in its precision argument.Proof (Lean source)
theorem expInterval_nested (I : RatInterval) (n : ℕ) : (expInterval I (n + 1)).Subinterval (expInterval I n) := by change expIntervalLo I n ≤ expIntervalLo I (n + 1) ∧ expIntervalHi I (n + 1) ≤ expIntervalHi I n unfold expIntervalLo expIntervalHi exact ⟨(expScalar_nested I.lo n).1, (expScalar_nested I.hi n).2⟩ -
logInterval_nestedtheorem — Positive logarithm interval evaluation is nested in its precision argument.hypothesesconclusion(logInterval I hI (n + 1)).Subinterval (logInterval I hI n)Proof (Lean source)
theorem logInterval_nested (I : RatInterval) (hI : 0 < I.lo) (n : ℕ) : (logInterval I hI (n + 1)).Subinterval (logInterval I hI n) := by change (logScalar I.lo hI n).lo ≤ (logScalar I.lo hI (n + 1)).lo ∧ (logScalar I.hi (hI.trans_le I.lo_le_hi) (n + 1)).hi ≤ (logScalar I.hi (hI.trans_le I.lo_le_hi) n).hi exact ⟨(logScalar_nested I.lo hI n).1, (logScalar_nested I.hi (hI.trans_le I.lo_le_hi) n).2⟩ -
rpowInterval_nestedtheorem — Real-power interval evaluation is nested in its precision argument.hypothesesconclusion(rpowInterval base exponent hbase (n + 1)).Subinterval (rpowInterval base exponent hbase n)Proof (Lean source)
theorem rpowInterval_nested (base exponent : RatInterval) (hbase : 0 < base.lo) (n : ℕ) : (rpowInterval base exponent hbase (n + 1)).Subinterval (rpowInterval base exponent hbase n) := by rw [rpowInterval_succ] let x : ℝ := base.lo let y : ℝ := exponent.lo have hx : base.Contains x := ⟨le_rfl, by dsimp [x]; exact_mod_cast base.lo_le_hi⟩ have hy : exponent.Contains y := ⟨le_rfl, by dsimp [y]; exact_mod_cast exponent.lo_le_hi⟩ have h₀ := rpowInterval_sound hbase hx hy n have h₁ := rpowRaw_sound hbase hx hy (n + 1) exact RatInterval.tighten_subinterval_left h₀ h₁