Grace/Cumulus/Int/AbsoluteValueOrder.g17

Open in Workbench Download source

Imports

OrderMul

Declarations

Source

1-- The absolute value of an integer and the order: triangle inequalities,2-- bounds, and the characterization by sign3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Int.AbsoluteValueOrder9import OrderMul1011theorem integerAbs.value (z : Integer)12  shows integerAbs(z) = integerOfNat(integerNatAbs(z))13proof14  simp [integerAbs]1516theorem integerAbs.nonneg (z : Integer)17  shows 0 ≤ integerAbs(z)18proof19  have magnitude := integerNatAbs.natural at z20  rw integerAbs.value21  exact integerLe.ofNat_nonneg with *2223theorem integerAbs.ofNat (n : Nat)24  shows integerAbs(integerOfNat(n)) = integerOfNat(n)25proof26  rw [integerAbs.value, integerNatAbs.ofNat]27  rfl2829theorem integerAbs.negative_ofNat (n : Nat)30  shows integerAbs(integerNegativeOfNat(n)) = integerOfNat(n)31proof32  rw [integerAbs.value, integerNatAbs.ofNegativeNat]33  rfl3435theorem integerAbs.of_nonneg (z : Integer)36  requires nonnegative : 0 ≤ z37  shows integerAbs(z) = z38proof39  have shape := integerLe.zero_iff.forward with nonnegative40  obtain ⟨n, nNat, equation⟩ := IntegerNonnegative.exists_natural with shape41  rw equation42  exact integerAbs.ofNat with *4344theorem integerAbs.of_nonpos (z : Integer)45  requires nonpositive : z ≤ 046  shows integerAbs(z) = -z47proof48  obtain ⟨n, nNat, equation⟩ := integerLe.exists_negative with nonpositive49  rw [equation, integerAbs.negative_ofNat, integerNegativeOfNat.neg]50  rfl5152theorem integerAbs.zero53  shows integerAbs(integerZero) = integerZero54proof55  have reflexive := integerLe.reflexive at integerZero56  exact integerAbs.of_nonneg with reflexive5758theorem integerAbs.one59  shows integerAbs(integerOne) = integerOne60proof61  have one := integerLe.zero_one62  exact integerAbs.of_nonneg with one6364theorem integerAbs.cases (z : Integer)65  shows integerAbs(z) = z ∨ integerAbs(z) = -z66proof67  have split := integerLe.cases_sign at z68  cases split with nonnegative | nonpositive69  . left70    exact integerAbs.of_nonneg with nonnegative71  . right72    exact integerAbs.of_nonpos with nonpositive7374theorem integerAbs.le_self (z : Integer)75  shows z ≤ integerAbs(z)76proof77  have split := integerLe.cases_sign at z78  cases split with nonnegative | nonpositive79  . have value := integerAbs.of_nonneg with nonnegative80    rw value81    exact integerLe.reflexive with *82  . have bound := integerAbs.nonneg at z83    exact integerLe.transitive with nonpositive, bound8485theorem integerAbs.neg_le_self (z : Integer)86  shows -z ≤ integerAbs(z)87proof88  have flipped := integerAbs.neg at z89  have bound := integerAbs.le_self at -z90  rw flipped at bound91  exact bound9293theorem integerAbs.mul (x y : Integer)94  shows integerAbs(x * y) = integerAbs(x) * integerAbs(y)95proof96  have xNat := integerNatAbs.natural at x97  have yNat := integerNatAbs.natural at y98  have magnitudes := integerNatAbs.mul at x, y99  rw [integerAbs.value, integerAbs.value, integerAbs.value, magnitudes]100  exact integerOfNat.mul with *101102theorem integerAbs.eq_zero_iff (z : Integer)103  shows integerAbs(z) = 0 ↔ z = 0104proof105  have magnitude := integerNatAbs.natural at z106  constructor107  . intro zero108    rw [integerAbs.value, ← integerOfNat.zero] at zero109    have vanish := integerOfNat.injective with zero110    exact integerNatAbs.zero_iff.forward with vanish111  . intro zero112    rw zero113    exact integerAbs.zero114115theorem integerAbs.positive_of_nonzero (z : Integer)116  requires nonzero : z ≠ 0117  shows 0 < integerAbs(z)118proof119  have nonnegative := integerAbs.nonneg at z120  have distinct : 0 ≠ integerAbs(z)121    intro zero122    symm at zero123    have same := integerAbs.eq_zero_iff.forward with zero124    exact nonzero with same125  exact integerLess.of_le_ne with nonnegative, distinct126127theorem integerAbs.le_iff (z b : Integer)128  shows integerAbs(z) ≤ b ↔ -b ≤ z ∧ z ≤ b129proof130  have lower := integerAbs.le_self at z131  have upper := integerAbs.neg_le_self at z132  constructor133  . intro bound134    constructor135    . have negated := integerLe.transitive with upper, bound136      have flipped := integerLe.neg.forward with negated137      have restore : -(-z) = z by ring138      rw restore at flipped139      exact flipped140    . exact integerLe.transitive with lower, bound141  . intro both142    have split := integerAbs.cases at z143    cases split with positive | negative144    . rw positive145      exact both.right146    . rw negative147      have flipped := integerLe.neg.forward with both.left148      have restore : -(-b) = b by ring149      rw restore at flipped150      exact flipped151152theorem integerAbs.lt_iff (z b : Integer)153  shows integerAbs(z) < b ↔ -b < z ∧ z < b154proof155  have lower := integerAbs.le_self at z156  have upper := integerAbs.neg_le_self at z157  constructor158  . intro bound159    constructor160    . have negated := integerLe.transitive_less with upper, bound161      have flipped := integerLess.neg.forward with negated162      have restore : -(-z) = z by ring163      rw restore at flipped164      exact flipped165    . exact integerLe.transitive_less with lower, bound166  . intro both167    have split := integerAbs.cases at z168    cases split with positive | negative169    . rw positive170      exact both.right171    . rw negative172      have flipped := integerLess.neg.forward with both.left173      have restore : -(-b) = b by ring174      rw restore at flipped175      exact flipped176177theorem integerAbs.triangle (x y : Integer)178  shows integerAbs(x + y) ≤ integerAbs(x) + integerAbs(y)179proof180  have xAbs := integerAbs.integer at x181  have yAbs := integerAbs.integer at y182  have split := integerAbs.cases at x + y183  cases split with positive | negative184  . rw positive185    have xBound := integerAbs.le_self at x186    have yBound := integerAbs.le_self at y187    exact integerLe.add with xBound, yBound188  . rw negative189    have shape : -(x + y) = (-x) + (-y) by ring190    rw shape191    have xBound := integerAbs.neg_le_self at x192    have yBound := integerAbs.neg_le_self at y193    exact integerLe.add with xBound, yBound194195theorem integerAbs.sub_abs_le (x y : Integer)196  shows integerAbs(x) - integerAbs(y) ≤ integerAbs(x - y)197proof198  have xAbs := integerAbs.integer at x199  have yAbs := integerAbs.integer at y200  have differenceAbs := integerAbs.integer at x - y201  have restore : x = (x - y) + y by ring202  have bound := integerAbs.triangle at x - y, y203  rw ← restore at bound204  have shifted := integerLe.sub_right at integerAbs(x),205    integerAbs(x - y) + integerAbs(y), integerAbs(y) with bound206  have cancel : integerAbs(x - y) + integerAbs(y) - integerAbs(y) =207      integerAbs(x - y)208    ring209  rw cancel at shifted210  exact shifted211212theorem integerAbs.sub_commutative (x y : Integer)213  shows integerAbs(x - y) = integerAbs(y - x)214proof215  have shape : y - x = -(x - y) by ring216  rw [shape, integerAbs.neg]217  rfl218219theorem integerAbs.square (z : Integer)220  shows integerAbs(z) * integerAbs(z) = z * z221proof222  have split := integerAbs.cases at z223  cases split with positive | negative224  . rw positive225    rfl226  . rw negative227    ring228229theorem integerAbs.eq_iff (x y : Integer)230  shows integerAbs(x) = integerAbs(y) ↔ x = y ∨ x = -y231proof232  constructor233  . intro same234    have xSquare := integerAbs.square at x235    have ySquare := integerAbs.square at y236    rw same at xSquare237    have squares : x * x = y * y238      rw [← xSquare, ← ySquare]239      rfl240    have product : (x - y) * (x + y) = 0241      have shape : (x - y) * (x + y) = x * x - y * y by ring242      rw [shape, squares]243      ring244    have split := integerMulValue.eq_zero with product245    cases split with first | second246    . left247      linear_combination first248    . right249      linear_combination second250  . intro split251    cases split with same | negated252    . rw same253      rfl254    . rw [negated, integerAbs.neg]255      rfl256257theorem integerAbs.monotone_nonneg (x y : Integer)258  requires nonnegative : 0 ≤ x259  requires below : x ≤ y260  shows integerAbs(x) ≤ integerAbs(y)261proof262  have yNonnegative := integerLe.transitive with nonnegative, below263  have xValue := integerAbs.of_nonneg with nonnegative264  have yValue := integerAbs.of_nonneg at y with yNonnegative265  rw [xValue, yValue]266  exact below267268theorem integerAbs.le_of_abs_le (x b : Integer)269  requires bound : integerAbs(x) ≤ b270  shows x ≤ b271proof272  have both := integerAbs.le_iff.forward with bound273  exact both.right274275theorem integerAbs.sub_le_of_le (x y b : Integer)276  requires lower : y - b ≤ x277  requires upper : x ≤ y + b278  shows integerAbs(x - y) ≤ b279proof280  apply integerAbs.le_iff.backward281  constructor282  . have shifted := integerLe.sub_right at y - b, x, y with lower283    have shape : y - b - y = -b by ring284    rw shape at shifted285    exact shifted286  . have shifted := integerLe.sub_right at x, y + b, y with upper287    have shape : y + b - y = b by ring288    rw shape at shifted289    exact shifted290