Grace/Cumulus/Real/AbsoluteValue.g17

Open in Workbench Download source

Imports

Squares · Algebra.OrderedField.Core

Declarations

• realAbsCut def
• realAbsCut.real theorem derivation
• realAbsCut.of_nonnegative theorem derivation
• realAbsCut.of_nonpositive theorem derivation
• realAbs def
• abs def
• realAbs.relates theorem derivation
• realAbs.factors theorem derivation
• realAbs.total theorem derivation
• realAbs.functional theorem derivation
• realAbs.function theorem derivation
• abs.real theorem derivation
• abs.cut theorem derivation
• abs.of_nonnegative theorem derivation
• abs.of_nonpositive theorem derivation
• abs.zero theorem derivation
• realAbs.absolute_value theorem derivation
• realLe.of_less_equal_by theorem derivation
• abs.nonnegative theorem derivation
• abs.eq_zero_iff theorem derivation
• abs.positive_of_ne theorem derivation
• abs.neg theorem derivation
• abs.mul theorem derivation
• abs.inv theorem derivation
• abs.upper theorem derivation
• abs.upper_neg theorem derivation
• abs.triangle theorem derivation

Source

1-- The absolute-value cut on the Dedekind reals2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.AbsoluteValue8import Squares9import Algebra.OrderedField.Core1011-- Absolute value is the sum of the positive and negative parts. This12-- definition is canonical for lower cuts and avoids choosing a sign case.13def realAbsCut (A : Set) : Set :=14  realAddCut(realPositivePart(A), realNegativePart(A))1516theorem realAbsCut.real (A : Real)17  shows Real(realAbsCut(A))18proof19  unfold realAbsCut20  exact realAddCut.real at realPositivePart(A), realNegativePart(A) with21    realPositivePart.real at A with assumption,22    realNegativePart.real at A with assumption2324theorem realAbsCut.of_nonnegative (A : Real)25  requires nonnegative : 0 ≤ A26  shows realAbsCut(A) = A27proof28  have subset := realLe.subset with realZero.real, nonnegative29  have positive := realPositivePart.eq_of_nonnegative with subset30  have negative := realNegativePart.eq_zero_of_nonnegative with subset31  simp [realAbsCut, positive, negative, realAddCut.zero_right]3233theorem realAbsCut.of_nonpositive (A : Real)34  requires nonpositive : A ≤ 035  shows realAbsCut(A) = realNegCut(A)36proof37  have subset := realLe.subset at A, realZero with38    assumption, realZero.real, nonpositive39  have positive := realPositivePart.eq_zero_of_nonpositive with subset40  have negative := realNegativePart.eq_neg_of_nonpositive with subset41  simp [realAbsCut, positive, negative, realAddCut.zero_left]4243-- Absolute value as a total function graph on the real carrier.44def realAbs : Set :=45  { p ∈ (ℝ × ℝ) | ∃ A ∈ ℝ, p = (A ↦ realAbsCut(A)) }4647def abs (A : Real) : Real := realAbs(A)4849theorem realAbs.relates (A : Real)50  shows relates(realAbs, A, realAbsCut(A))51proof52  have realA : A ∈ ℝ by simp [Real]53  unfold relates54  apply realAbs.membership.backward55  constructor56  . apply product.pair at A, realAbsCut(A), ℝ, ℝ57    . exact realA58    . exact realAbsCut.real at A59  . refine ⟨A, realA, rfl⟩6061theorem realAbs.factors (input output : Set)62  requires mapped : relates(realAbs, input, output)63  shows ∃ A ∈ ℝ, input = A ∧ output = realAbsCut(A)64proof65  unfold relates at mapped66  simp [realAbs.membership] at mapped67  rcases mapped with ⟨bounded, A, realA, shape⟩68  obtain ⟨inputShape, outputShape⟩ := orderedPair.injective with shape69  refine ⟨A, realA, inputShape, outputShape⟩7071theorem realAbs.total72  shows TotalBetween(realAbs, ℝ, ℝ)73proof74  intros A realA75  have typedA : Real(A) by exact realA76  refine ⟨realAbsCut(A), realAbsCut.real at A with typedA, realAbs.relates at A with typedA⟩7778theorem realAbs.functional79  shows Functional(realAbs)80proof81  intros input y inputY z inputZ82  obtain ⟨A, realA, inputFirst, outputFirst⟩ := realAbs.factors with inputY83  obtain ⟨B, realB, inputSecond, outputSecond⟩ := realAbs.factors with inputZ84  rw inputFirst at inputSecond85  calc86    y = realAbsCut(A) := outputFirst87    _ = realAbsCut(B) := by simp [inputSecond]88    _ = z := by simp [outputSecond]8990theorem realAbs.function91  shows realAbs : ℝ → ℝ92proof93  constructor94    intros p member95    simp [realAbs.membership] at member96    rcases member with ⟨bounded, witnesses⟩97    exact bounded98  . constructor99    . exact realAbs.functional100    . exact realAbs.total101102theorem abs.real (A : Real)103  shows Real(abs(A))104proof105  have realA : A ∈ ℝ by simp [Real]106  obtain ⟨B, realB, mapped⟩ := FunctionBetween.exists_value with realAbs.function, realA107  have applied := FunctionBetween.apply_value with realAbs.function, mapped108  unfold abs109  rw applied110  exact realB111112theorem abs.cut (A : Real)113  shows abs(A) = realAbsCut(A)114proof115  have mapped := realAbs.relates at A116  unfold abs117  exact FunctionBetween.apply_value with realAbs.function, mapped118119theorem abs.of_nonnegative (A : Real)120  requires nonnegative : 0 ≤ A121  shows abs(A) = A122proof123  calc124    abs(A) = realAbsCut(A) := abs.cut at A with assumption125    _ = A := realAbsCut.of_nonnegative at A with nonnegative126127theorem abs.of_nonpositive (A : Real)128  requires nonpositive : A ≤ 0129  shows abs(A) = -A130proof131  have cut := realNegValue.cut at A132  calc133    abs(A) = realAbsCut(A) := abs.cut at A with assumption134    _ = realNegCut(A) := realAbsCut.of_nonpositive at A with135      assumption, nonpositive136    _ = -A := by simp [cut]137138theorem abs.zero139  shows abs(0) = 0140proof141  have zeroLeZero := realLe.of_subset at realZero, realZero with142    realZero.real, realZero.real, Subset.reflexive at realZero143  exact abs.of_nonnegative with realZero.real, zeroLeZero144145-- The Dedekind construction discharges the generic ordered-field interface146-- once, and the algebraic absolute-value laws below are inherited from it147-- instead of being reproved from cuts.148theorem realAbs.absolute_value149  shows AbsoluteValue(ℝ, realZero, realNeg, realLess, realAbs)150proof151  constructor152  . exact realAbs.function153  . constructor154    . have zero := abs.zero155      unfold abs at zero156      exact zero157    . intros A realA158      have typedA : Real(A) by exact realA159      constructor160      . intro positive161        have nonnegative := realLess.implies_le with realZero.real, positive162        have shape := abs.of_nonnegative with nonnegative163        unfold abs at shape164        assumption165      . intro negative166        have nonpositive := realLess.implies_le with typedA, realZero.real, negative167        have shape := abs.of_nonpositive with nonpositive168        unfold abs at shape169        assumption170171theorem realLe.of_less_equal_by (A B : Real)172  requires order : LessEqualBy(ℝ, realLess, A, B)173  shows A ≤ B174proof175  rcases order with ⟨realA, realB, comparison⟩176  cases comparison with equal | less177  . rw equal178    exact realLe.reflexive with assumption179  . exact realLess.implies_le with less180181theorem abs.nonnegative (A : Real)182  shows 0 ≤ abs(A)183proof184  have sign := Real.sign_cases at A185  cases sign with nonpositive | nonnegative186  . have leZero := realLe.of_subset at A, realZero with187      assumption, realZero.real, nonpositive188    have shape := abs.of_nonpositive with leZero189    have negSubset := realNegValue.nonnegative_of_nonpositive with nonpositive190    have result := realLe.of_subset with realZero.real, negSubset191    rwa shape192  . have result := realLe.of_subset at realZero, A with193      realZero.real, assumption, nonnegative194    have shape := abs.of_nonnegative with result195    rwa shape196197theorem abs.eq_zero_iff (A : Real)198  shows abs(A) = 0 ↔ A = 0199proof200  have realA : A ∈ ℝ by simp [Real]201  have generic := AbsoluteValue.eq_zero_iff with reals.ordered_field, realAbs.absolute_value, realA202  constructor203  . intro zero204    apply generic.forward205    unfold abs at zero206    assumption207  . intro equal208    rw equal209    exact abs.zero210211theorem abs.positive_of_ne (A : Real)212  requires nonzero : A ≠ 0213  shows 0 < abs(A)214proof215  have realA : A ∈ ℝ by simp [Real]216  have positive := AbsoluteValue.positive_of_ne with217    reals.ordered_field, realAbs.absolute_value, realA, nonzero218  unfold abs219  exact positive220221theorem abs.neg (A : Real)222  shows abs(-A) = abs(A)223proof224  have realA : A ∈ ℝ by simp [Real]225  have generic := AbsoluteValue.neg with reals.ordered_field, realAbs.absolute_value, realA226  simp [abs]227228theorem abs.mul (A B : Real)229  shows abs(A * B) = abs(A) * abs(B)230proof231  have realA : A ∈ ℝ by simp [Real]232  have realB : B ∈ ℝ by simp [Real]233  have generic := AbsoluteValue.mul with reals.ordered_field, realAbs.absolute_value, realA, realB234  simp [abs]235236theorem abs.inv (A : Real)237  requires nonzero : A ≠ 0238  shows abs(realInvValue(A)) = realInvValue(abs(A))239proof240  have inverseReal := realInvValue.real at A241  have absANonzero : abs(A) ≠ 0242    intro absoluteZero243    apply nonzero244    exact abs.eq_zero_iff.forward with absoluteZero245  have inverseLaw := realInvValue.mul_right with nonzero246  have multiplicative := abs.mul at A, realInvValue(A) with247    assumption, inverseReal248  have oneNonnegative := realLess.implies_le with realZero.real, realOne.real, realZero.lt_one249  have absoluteOne := abs.of_nonnegative with realOne.real, oneNonnegative250  have candidateLaw : abs(A) * abs(realInvValue(A)) = 1251    calc252      abs(A) * abs(realInvValue(A)) = abs(A * realInvValue(A)) := by cc253      _ = abs(1) := by cc254      _ = 1 := absoluteOne255  exact realInvValue.eq_of_mul_right with absANonzero, candidateLaw256257theorem abs.upper (A : Real)258  shows A ≤ abs(A)259proof260  have realA : A ∈ ℝ by simp [Real]261  have generic := AbsoluteValue.upper with reals.ordered_field, realAbs.absolute_value, realA262  have bound : LessEqualBy(ℝ, realLess, A, abs(A))263    unfold abs264    exact generic265  exact realLe.of_less_equal_by at A, abs(A) with266    assumption, abs.real at A with assumption, bound267268theorem abs.upper_neg (A : Real)269  shows -A ≤ abs(A)270proof271  have realA : A ∈ ℝ by simp [Real]272  have generic := AbsoluteValue.upper_neg with reals.ordered_field, realAbs.absolute_value, realA273  have bound : LessEqualBy(ℝ, realLess, -A, abs(A))274    unfold abs275    exact generic276  exact realLe.of_less_equal_by at -A, abs(A) with277    realNegValue.real at A with assumption,278    abs.real at A with assumption, bound279280-- Both A + B and -(A + B) lie below abs(A) + abs(B); the sign of281-- A + B selects the defining branch of absolute value.282theorem abs.triangle (A B : Real)283  shows abs(A + B) ≤ abs(A) + abs(B)284proof285  have sumReal := realAddValue.real at A, B with *286  have absAReal := abs.real at A287  have absBReal := abs.real at B288  have positiveBound := realLe.add at A, abs(A), B, abs(B) with289    assumption, absAReal, assumption, absBReal,290    abs.upper at A with assumption, abs.upper at B with assumption291  have negAReal := realNegValue.real at A292  have negBReal := realNegValue.real at B293  have negativeBound := realLe.add at -A, abs(A), -B, abs(B) with294    negAReal, absAReal, negBReal, absBReal,295    abs.upper_neg at A with assumption, abs.upper_neg at B with assumption296  have negSum := realNegValue.add at A, B with *297  rw ← negSum at negativeBound298  have sign := Real.sign_cases with sumReal299  cases sign with nonpositive | nonnegative300  . have sumLeZero := realLe.of_subset at A + B, realZero with301      sumReal, realZero.real, nonpositive302    have shape := abs.of_nonpositive with sumLeZero303    rwa shape304  . have zeroLeSum := realLe.of_subset at realZero, A + B with305      realZero.real, sumReal, nonnegative306    have shape := abs.of_nonnegative with zeroLeSum307    rwa shape308