Grace/Cumulus/Real/Metric.g17

Open in Workbench Download source

Imports

AbsoluteValue · Natural

Declarations

Source

1-- The standard metric 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.Metric8import AbsoluteValue9import Natural1011-- The field-theoretic half of a real. Its laws come from the generic12-- ordered-field development rather than the Dedekind-cut construction.13def half (A : Real) : Real :=14  fieldHalf(realAdd, realMul, realOne, realInv, A)1516theorem half.real (A : Real)17  shows Real(half(A))18proof19  unfold half20  unfold Real21  have realA : A ∈ ℝ by simp [Real]22  exact IsOrderedField.half_closed with reals.ordered_field, realA2324theorem half.positive (A : Real)25  requires positive : 0 < A26  shows 0 < half(A)27proof28  unfold half29  exact IsOrderedField.half_positive with reals.ordered_field, positive3031theorem half.add_self (A : Real)32  shows half(A) + half(A) = A33proof34  have realA : A ∈ ℝ by simp [Real]35  have generic := IsOrderedField.half_add_self with reals.ordered_field, realA36  unfold half37  exact generic3839theorem half.lt_self (A : Real)40  requires positive : 0 < A41  shows half(A) < A42proof43  have halfReal := half.real at A44  have halfPositive := half.positive with positive45  have step := realLess.add_left with realZero.real, halfReal, halfReal, halfPositive46  have zero := realAddValue.zero_right with halfReal47  have doubled := half.add_self at A48  rwa [zero, doubled] at step4950def dist (A B : Real) : Real := abs(A - B)5152theorem dist.real (A B : Real)53  shows Real(dist(A, B))54proof55  unfold dist56  have differenceReal := realSubValue.real at A, B with *57  exact abs.real with differenceReal5859theorem dist.nonnegative (A B : Real)60  shows 0 ≤ dist(A, B)61proof62  unfold dist63  have differenceReal := realSubValue.real at A, B with *64  exact abs.nonnegative with differenceReal6566theorem dist.self (A : Real)67  shows dist(A, A) = 068proof69  unfold dist70  have selfDifference := realSubValue.self at A71  rw selfDifference72  exact abs.zero7374theorem realSubValue.eq_zero_iff (A B : Real)75  shows A - B = 0 ↔ A = B76proof77  constructor78  . intro differenceZero79    have cancelled := realSubValue.add_right_cancel at A, B with80      *{2}81    have zeroLeft := realAddValue.zero_left at B82    rw [differenceZero, zeroLeft] at cancelled83    rw cancelled84    rfl85  . intro equal86    rw equal87    exact realSubValue.self with assumption8889theorem dist.eq_zero_iff (A B : Real)90  shows dist(A, B) = 0 ↔ A = B91proof92  constructor93  . intro zeroDistance94    unfold dist at zeroDistance95    have zeroDifference := abs.eq_zero_iff.forward with zeroDistance96    exact realSubValue.eq_zero_iff.forward with zeroDifference97  . intro equal98    unfold dist99    rw equal100    have selfDifference := realSubValue.self at B101    rw selfDifference102    exact abs.zero103104theorem dist.positive_of_ne (A B : Real)105  requires unequal : A ≠ B106  shows 0 < dist(A, B)107proof108  unfold dist109  have differenceReal := realSubValue.real at A, B with110    *{2}111  apply abs.positive_of_ne with differenceReal112  intro differenceZero113  apply unequal114  exact realSubValue.eq_zero_iff.forward with differenceZero115116theorem dist.symmetric (A B : Real)117  shows dist(A, B) = dist(B, A)118proof119  have differenceReal := realSubValue.real at A, B with *120  have swapped := realSubValue.neg_swap at A, B with *121  have absoluteNeg := abs.neg with differenceReal122  simp [dist]123124theorem dist.triangle (A B C : Real)125  shows dist(A, C) ≤ dist(A, B) + dist(B, C)126proof127  have firstDifferenceReal := realSubValue.real at A, B with128    *{2}129  have secondDifferenceReal := realSubValue.real at B, C with130    *{2}131  have path : A - C = (A - B) + (B - C)132    unfold realSubValue133    have negBReal := realNegValue.real at B134    have negCReal := realNegValue.real at C135    have secondReal := realAddValue.real at B, -C with assumption, negCReal136    have outerAssoc := realAddValue.associative at A, -B, B + (-C) with137      assumption, negBReal, secondReal138    have innerAssoc := realAddValue.associative at -B, B, -C with139      negBReal, assumption, negCReal140    have inverse := realAddValue.neg_left at B141    have identity := realAddValue.zero_left with negCReal142    cc143  have triangle := abs.triangle with firstDifferenceReal, secondDifferenceReal144  unfold dist145  rwa path146147def openBall (C E : Real) : Set :=148  { X ∈ ℝ | dist(X, C) < E }149150theorem openBall.center (C E : Real)151  requires positive : 0 < E152  shows C ∈ openBall(C, E)153proof154  have typedC : Real(C) by typecheck155  have realC : C ∈ ℝ by simp [Real]156  have selfDistance := dist.self with typedC157  apply openBall.membership.backward158  constructor159  . exact realC160  . rw selfDistance161    exact positive162163theorem openBall.symmetric (X C E : Real)164  shows X ∈ openBall(C, E) ↔ C ∈ openBall(X, E)165proof166  have symmetry := dist.symmetric at X, C with *167  have realX : X ∈ ℝ by simp [Real]168  have realC : C ∈ ℝ by simp [Real]169  constructor170  . intro member171    have data := openBall.membership.forward with member172    rcases data with ⟨realX, within⟩173    apply openBall.membership.backward174    constructor175    . exact realC176    . rw ← symmetry177      exact within178  . intro member179    have data := openBall.membership.forward with member180    rcases data with ⟨realC, within⟩181    apply openBall.membership.backward182    constructor183    . exact realX184    . rw symmetry185      exact within186187theorem openBall.mono (X C E D : Real)188  requires member : X ∈ openBall(C, E)189  requires radii : E ≤ D190  shows X ∈ openBall(C, D)191proof192  obtain ⟨realX, within⟩ := openBall.membership.forward with member193  have typedX : Real(X) by exact realX194  have distanceReal := dist.real at X, C with typedX, assumption195  apply openBall.membership.backward196  constructor197  . exact realX198  . exact realLess.transitive_le at dist(X, C), E, D with199      distanceReal, *{2}, within, radii200201-- Metric balls compose additively: an E-step followed by a D-step remains202-- inside the ball of radius E + D.203theorem openBall.triangle (X Y Z E D : Real)204  requires xy : X ∈ openBall(Y, E)205  requires yz : Y ∈ openBall(Z, D)206  shows X ∈ openBall(Z, E + D)207proof208  have xyData := openBall.membership.forward with xy209  have yzData := openBall.membership.forward with yz210  rcases xyData with ⟨realX, xyLess⟩211  rcases yzData with ⟨realY, yzLess⟩212  have typedX : Real(X) by exact realX213  have typedY : Real(Y) by exact realY214  have xyReal := dist.real with typedX, typedY215  have yzReal := dist.real at Y, Z with typedY, assumption216  have xzReal := dist.real at X, Z with typedX, assumption217  have sumDistancesReal := realAddValue.real with xyReal, yzReal218  have radiusReal := realAddValue.real at E, D with *219  have firstLess := realLess.add_right at220    dist(X, Y), E, dist(Y, Z) with221      xyReal, assumption, yzReal, xyLess222  have secondLess := realLess.add_left at223    dist(Y, Z), D, E with224      yzReal, *{2}, yzLess225  have sumLess := realLess.transitive with firstLess, secondLess226  have triangle := dist.triangle at X, Y, Z with typedX, typedY, assumption227  apply openBall.membership.backward228  constructor229  . exact realX230  . exact realLe.transitive_less at231      dist(X, Z), dist(X, Y) + dist(Y, Z), E + D with232        xzReal, sumDistancesReal,233        radiusReal, triangle, sumLess234235-- Two balls whose common radius is half the distance between their centers236-- cannot share a point unless the centers coincide.237theorem openBall.half_radius_unique (X A B : Real)238  requires nearA : X ∈ openBall(A, half(dist(A, B)))239  requires nearB : X ∈ openBall(B, half(dist(A, B)))240  shows A = B241proof242  have distanceReal := dist.real at A, B with *243  have radiusReal := half.real with distanceReal244  have aNearX := openBall.symmetric.forward at245    X, A, half(dist(A, B)) with246      *{2}, radiusReal, nearA247  have path := openBall.triangle at248    A, X, B, half(dist(A, B)), half(dist(A, B)) with249      *{3}, radiusReal, radiusReal,250      aNearX, nearB251  have doubled := half.add_self with distanceReal252  rw doubled at path253  have pathData := openBall.membership.forward at254    B, dist(A, B), A with path255  rcases pathData with ⟨realA, impossible⟩256  exfalso257  exact IsOrderedField.irreflexive with reals.ordered_field, impossible258259theorem dist.add_right (A B C : Real)260  shows dist(A + C, B + C) = dist(A, B)261proof262  have identity : (A + C) - (B + C) = A - B263    unfold realSubValue264    have negSum := realNegValue.add at B, C with *265    rw negSum266    have negBReal := realNegValue.real at B267    have negCReal := realNegValue.real at C268    have shuffle := realAddValue.four_shuffle at A, C, -B, -C with269      *{2}, negBReal, negCReal270    have inverse := realAddValue.neg_right at C271    have differenceReal := realAddValue.real at A, -B with272      assumption, negBReal273    have zero := realAddValue.zero_right with differenceReal274    cc275  simp [dist]276277theorem dist.add_left (A B C : Real)278  shows dist(C + A, C + B) = dist(A, B)279proof280  have leftCommutative := realAddValue.commutative at C, A with281    *{2}282  have rightCommutative := realAddValue.commutative at C, B with283    *{2}284  rw [leftCommutative, rightCommutative]285  exact dist.add_right with *286287theorem dist.neg (A B : Real)288  shows dist(-A, -B) = dist(A, B)289proof290  have differenceReal := realSubValue.real at A, B with *291  have identity : (-A) - (-B) = -(A - B)292    unfold realSubValue293    have negBReal := realNegValue.real at B294    have leftInvolutive := realNegValue.involutive at B295    have rightDistribution := realNegValue.add at A, -B with296      assumption, negBReal297    cc298  unfold dist299  rw identity300  exact abs.neg with differenceReal301302-- Pointwise addition is Lipschitz in both arguments.303theorem dist.add_add (A B C D : Real)304  shows dist(A + B, C + D) ≤ dist(A, C) + dist(B, D)305proof306  have firstDifferenceReal := realSubValue.real at A, C with307    *{2}308  have secondDifferenceReal := realSubValue.real at B, D with309    *{2}310  have identity : (A + B) - (C + D) = (A - C) + (B - D)311    unfold realSubValue312    have negSum := realNegValue.add at C, D with *313    have negCReal := realNegValue.real at C314    have negDReal := realNegValue.real at D315    rw negSum316    exact realAddValue.four_shuffle with *{2}, negCReal, negDReal317  have triangle := abs.triangle with firstDifferenceReal, secondDifferenceReal318  unfold dist319  rwa identity320321-- Adding points in two balls adds their radii.322theorem openBall.add (A B C D E F : Real)323  requires nearA : A ∈ openBall(C, E)324  requires nearB : B ∈ openBall(D, F)325  shows A + B ∈ openBall(C + D, E + F)326proof327  have dataA := openBall.membership.forward with nearA328  have dataB := openBall.membership.forward with nearB329  rcases dataA with ⟨realA, closeA⟩330  rcases dataB with ⟨realB, closeB⟩331  have distanceACReal := dist.real at A, C with *332  have distanceBDReal := dist.real at B, D with *333  have sumDistancesReal := realAddValue.real with distanceACReal, distanceBDReal334  have radiusReal := realAddValue.real at E, F with *335  have sumReal := realAddValue.real at A, B with *336  have centerReal := realAddValue.real at C, D with *337  have totalDistanceReal := dist.real with sumReal, centerReal338  have distanceBound := dist.add_add at A, B, C, D with339    *{4}340  have radiiBound := realLess.add at341    dist(A, C), E, dist(B, D), F with342      distanceACReal, assumption, distanceBDReal, assumption,343      closeA, closeB344  have within := realLe.transitive_less with345    totalDistanceReal, sumDistancesReal, radiusReal, distanceBound, radiiBound346  apply openBall.membership.backward347  constructor348    exact sumReal349  . exact within350351-- A point near B has absolute value at most its distance from B plus |B|.352-- This is the standard local boundedness estimate used in limit proofs.353theorem abs.le_dist_add_abs (A B : Real)354  shows abs(A) ≤ dist(A, B) + abs(B)355proof356  have differenceReal := realSubValue.real at A, B with *357  have cancellation := realSubValue.add_right_cancel at A, B with358    *{2}359  have triangle := abs.triangle at A - B, B with differenceReal, assumption360  unfold dist361  rwa cancellation at triangle362363-- The familiar reciprocal-difference identity, stated in the orientation364-- used by epsilon estimates.365theorem realSubValue.inv_inv (A B : Real)366  requires nonzeroA : A ≠ 0367  requires nonzeroB : B ≠ 0368  shows realInvValue(A) - realInvValue(B) =369    (B - A) * (realInvValue(A) * realInvValue(B))370proof371  have inverseAReal := realInvValue.real at A372  have inverseBReal := realInvValue.real at B373  have negAReal := realNegValue.real at A374  have inverseProductReal := realMulValue.real with inverseAReal, inverseBReal375  have inverseA := realInvValue.mul_right with nonzeroA376  have inverseB := realInvValue.mul_right with nonzeroB377  have distribute := realMulValue.distributive_right at378    B, -A, realInvValue(A) * realInvValue(B) with379      assumption, negAReal, inverseProductReal380  have negProduct := realMulValue.neg_left at381    A, realInvValue(A) * realInvValue(B) with382      assumption, inverseProductReal383  have commuteBInvA := realMulValue.commutative at B, realInvValue(A) with384    assumption, inverseAReal385  have assocB := realMulValue.associative at386    B, realInvValue(A), realInvValue(B) with387      assumption, inverseAReal, inverseBReal388  have assocInvAB := realMulValue.associative at389    realInvValue(A), B, realInvValue(B) with390      inverseAReal, assumption, inverseBReal391  have assocA := realMulValue.associative at392    A, realInvValue(A), realInvValue(B) with393      assumption, inverseAReal, inverseBReal394  have oneLeftInvA := realMulValue.one_left with inverseAReal395  have oneLeftInvB := realMulValue.one_left with inverseBReal396  have oneRightInvA := realMulValue.one_right with inverseAReal397  unfold realSubValue398  calc399    realInvValue(A) + -realInvValue(B) =400        realInvValue(A) * 1 + -(1 * realInvValue(B)) := by cc401    _ = realInvValue(A) * (B * realInvValue(B)) +402        -((A * realInvValue(A)) * realInvValue(B)) := by cc403    _ = B * (realInvValue(A) * realInvValue(B)) +404        -(A * (realInvValue(A) * realInvValue(B))) := by cc405    _ = (B + -A) * (realInvValue(A) * realInvValue(B)) := by cc406407theorem dist.inv_inv (A B : Real)408  requires nonzeroA : A ≠ 0409  requires nonzeroB : B ≠ 0410  shows dist(realInvValue(A), realInvValue(B)) =411    dist(A, B) * (abs(realInvValue(A)) * abs(realInvValue(B)))412proof413  have inverseAReal := realInvValue.real at A414  have inverseBReal := realInvValue.real at B415  have difference := realSubValue.inv_inv with nonzeroA, nonzeroB416  have baReal := realSubValue.real at B, A with *417  have inverseProductReal := realMulValue.real with inverseAReal, inverseBReal418  have outerAbs := abs.mul with baReal, inverseProductReal419  have innerAbs := abs.mul with inverseAReal, inverseBReal420  have symmetric := dist.symmetric at B, A with *421  unfold dist422  unfold dist at symmetric423  rw [difference, outerAbs, innerAbs]424  have absSymmetric : abs(B - A) = abs(A - B) by exact symmetric425  calc426    abs(B - A) * (abs(realInvValue(A)) * abs(realInvValue(B))) =427        abs(A - B) * (abs(realInvValue(A)) * abs(realInvValue(B))) :=428      by cc429430-- If A lies within half of |B| from a nonzero B, then A remains uniformly431-- away from zero.  This is the standard local lower bound for reciprocals.432theorem abs.half_lt_of_dist_lt_half (A B : Real)433  requires nonzeroB : B ≠ 0434  requires close : dist(A, B) < half(abs(B))435  shows half(abs(B)) < abs(A)436proof437  have absAReal := abs.real at A438  have absBReal := abs.real at B439  have halfAbsBReal := half.real with absBReal440  have distReal := dist.real at A, B with *441  have absBPositive := abs.positive_of_ne with nonzeroB442  have halfPositive := half.positive with absBPositive443  have cutHalf := Real.characterization.forward with halfAbsBReal444  have cutAbsA := Real.characterization.forward with absAReal445  have notAbsBelow : ¬(abs(A) ⊆ half(abs(B)))446    intro absABelow447    have absALeHalf := realLe.of_subset with absABelow448    have first := realLess.add_right with distReal, halfAbsBReal, absAReal, close449    have second := realLe.add_left with absAReal, halfAbsBReal, halfAbsBReal, absALeHalf450    have sumBelow := realLess.transitive_le with first, second451    have doubled := half.add_self with absBReal452    rw doubled at sumBelow453    have triangle := abs.le_dist_add_abs at B, A with454      *{2}455    have symmetric := dist.symmetric at B, A with *456    rw symmetric at triangle457    have cycle := realLe.transitive_less with triangle, sumBelow458    have irreflexive := realLess.irreflexive_on459    exact irreflexive with abs(B), cycle460  have comparable := DedekindCut.comparable with cutHalf, cutAbsA461  cases comparable with halfBelow | absABelow462  . apply realLess.characterization.backward at half(abs(B)), abs(A)463    unfold RealLess464    refine ⟨halfAbsBReal, absAReal, _⟩465    constructor466    . exact halfBelow467    . intro equal468      apply notAbsBelow469      rw ← equal470      exact Subset.reflexive471  . exfalso472    exact notAbsBelow with absABelow473474-- The difference of two products, arranged in the form most useful for475-- analysis: AB - CD = A(B - D) + D(A - C).476theorem realSubValue.mul_mul (A B C D : Real)477  shows A * B - C * D = A * (B - D) + D * (A - C)478proof479  have negDReal := realNegValue.real at D480  have negCReal := realNegValue.real at C481  have abReal := realMulValue.real at A, B with *482  have adReal := realMulValue.real at A, D with *483  have cdReal := realMulValue.real at C, D with *484  have negADReal := realNegValue.real with adReal485  have negCDReal := realNegValue.real with cdReal486  have adPlusNegCDReal := realAddValue.real with adReal, negCDReal487  have distributeA := realMulValue.distributive at A, B, -D with488    *{2}, negDReal489  have distributeD := realMulValue.distributive at D, A, -C with490    *{2}, negCReal491  have negateAD := realMulValue.neg_right at A, D with *492  have negateDC := realMulValue.neg_right at D, C with *493  have commuteDA := realMulValue.commutative at D, A with *494  have commuteDC := realMulValue.commutative at D, C with *495  have cancelAD := realAddValue.neg_left with adReal496  have zeroNegCD := realAddValue.zero_left with negCDReal497  have middleAssoc := realAddValue.associative with negADReal, adReal, negCDReal498  have outerAssoc := realAddValue.associative with abReal, negADReal, adPlusNegCDReal499  unfold realSubValue500  calc501    A * B + -(C * D) = A * B + (0 + -(C * D)) := by cc502    _ = A * B + ((-(A * D) + A * D) + -(C * D)) := by cc503    _ = A * B + (-(A * D) + (A * D + -(C * D))) := by cc504    _ = A * (B + -D) + D * (A + -C) := by cc505506-- Multiplication is locally Lipschitz in the familiar two-term form.507theorem dist.mul_mul (A B C D : Real)508  shows dist(A * B, C * D) ≤509    abs(A) * dist(B, D) + abs(D) * dist(A, C)510proof511  have bdReal := realSubValue.real at B, D with *512  have acReal := realSubValue.real at A, C with *513  have firstReal := realMulValue.real at A, B - D with assumption, bdReal514  have secondReal := realMulValue.real at D, A - C with assumption, acReal515  have decomposition := realSubValue.mul_mul at A, B, C, D with516    *{4}517  have triangle := abs.triangle with firstReal, secondReal518  have firstAbsolute := abs.mul at A, B - D with assumption, bdReal519  have secondAbsolute := abs.mul at D, A - C with assumption, acReal520  unfold dist521  rw decomposition522  rwa [firstAbsolute, secondAbsolute] at triangle523524-- Cancel doubling without introducing a numeral-dependent arithmetic rule.525theorem realAddValue.double_cancel (A B : Real)526  requires doubled : A + A = B + B527  shows A = B528proof529  have halfDouble := half.add_self with realOne.real530  linear_combination half(realOne) * doubled - (A - B) * halfDouble531532-- Keep the small scalar calculation reusable in vector and geometry proofs.533theorem realMulValue.square_of_double (A B : Real)534  requires doubled : A + A = B535  shows B * B = A * A + A * A + A * A + A * A536proof537  rw ← doubled538  ring539540theorem realAddValue.two_nonzero541  shows (2:R) ≠ 0542proof543  intro zero544  have onePositive := realZero.lt_one545  linarith546547-- Recover a value from its doubled equation without expanding its expression.548theorem realDiv.of_double_eq (A B : Real)549  requires doubled : A + A = B550  shows A = B / (2:R)551proof552  have two : Real((2:R)) by typecheck553  have quotient := realDiv.real at B, (2:R) with *554  have cancel := realDiv.mul_left at B, (2:R) with555    assumption, two, realAddValue.two_nonzero556  apply realAddValue.double_cancel with assumption, quotient557  linear_combination doubled - cancel558559-- Halves as quotients by two.560theorem realHalf.add_self561  shows (1:R) / 2 + 1 / 2 = 1562proof563  have twoNonzero : (2:R) ≠ 0564    intro zero565    linarith566  have oneReal : (1:R) ∈ ℝ by typecheck567  have twoReal : (2:R) ∈ ℝ by typecheck568  have halfReal := realDiv.real at (1:R), (2:R) with *569  have half := realDiv.mul_right at (1:R), (2:R) with twoNonzero570  have twice : (1:R) / 2 + 1 / 2 = 1 / 2 * 2 by ring571  rw [twice, half]572  rfl573574theorem realDiv.lt_half (A B : Real)575  requires positive : 0 < B576  requires below : 2 * A < B577  shows A / B < 1 / 2578proof579  have oneReal : (1:R) ∈ ℝ by typecheck580  have twoReal : (2:R) ∈ ℝ by typecheck581  have halfReal := realDiv.real at (1:R), (2:R) with *582  have twice := realHalf.add_self583  have split : 1 / 2 * B + 1 / 2 * B = (1 / 2 + 1 / 2) * B by ring584  rw twice at split585  have unit : (1:R) * B = B by ring586  have halfBelow : A < 1 / 2 * B by linarith587  exact realDiv.lt_of_lt_mul with positive, halfBelow588589-- Division by three and cancellation of tripled real values.590theorem realAddValue.three_nonzero591  shows (3:R) ≠ 0592proof593  intro zero594  have onePositive := realZero.lt_one595  linarith596597def third (A : Real) : Real := A / (3:R)598599theorem third.real (A : Real)600  shows Real(third(A))601proof602  unfold third603  typecheck604605theorem third.add_self (A : Real)606  shows third(A) + third(A) + third(A) = A607proof608  have cancel := realDiv.mul_left with realAddValue.three_nonzero609  unfold third610  linear_combination cancel611612theorem realAddValue.triple_cancel (A B : Real)613  requires tripled : A + A + A = B + B + B614  shows A = B615proof616  have thirdTriple := third.add_self at realOne with *617  linear_combination third(realOne) * tripled - (A - B) * thirdTriple618