Grace/Cumulus/Metric/Line.g17

Open in Workbench Download source

Imports

Uniform · Topology.Real

Declarations

Source

1-- The real line as a metric space: the distance function on ℝ × ℝ, its2-- balls and topology, continuity and convergence in metric terms, and3-- completeness4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Metric.Line10import Uniform11import Topology.Real1213defgraph realDistance (p ∈ ℝ × ℝ) : ℝ :=14  dist(firstProjection(ℝ, ℝ)(p), secondProjection(ℝ, ℝ)(p))15proof16  have first := firstProjection.function at ℝ, ℝ17  have second := secondProjection.function at ℝ, ℝ18  have realA : Real(firstProjection(ℝ, ℝ)(p))19    exact FunctionBetween.apply_closed with first, member20  have realB : Real(secondProjection(ℝ, ℝ)(p))21    exact FunctionBetween.apply_closed with second, member22  exact dist.real with realA, realB2324theorem realDistance.apply (x y : Real)25  shows realDistance(x, y) = dist(x, y)26proof27  have realX : x ∈ ℝ by simp [Real]28  have realY : y ∈ ℝ by simp [Real]29  have pair := product.pair_membership.backward at x, y, ℝ, ℝ with30    ⟨realX, realY⟩31  have value := realDistance.value with pair32  have first := firstProjection.pair at ℝ, ℝ, x, y with realX, realY33  have second := secondProjection.pair at ℝ, ℝ, x, y with realX, realY34  unfold call235  cc3637theorem realDistance.metric38  shows IsMetric(ℝ, realDistance)39proof40  constructor41  . exact realDistance.function42  . constructor43    . intros x hx y hy44      have typedX : Real(x) by exact hx45      have typedY : Real(y) by exact hy46      have value := realDistance.apply at x, y with *47      rw value48      exact dist.nonnegative with typedX, typedY49    . constructor50      . intros x hx y hy51        have typedX : Real(x) by exact hx52        have typedY : Real(y) by exact hy53        have value := realDistance.apply at x, y with *54        rw value55        exact dist.eq_zero_iff at x, y with *56      . constructor57        . intros x hx y hy58          have typedX : Real(x) by exact hx59          have typedY : Real(y) by exact hy60          have valueXY := realDistance.apply at x, y with *61          have valueYX := realDistance.apply at y, x with *62          rw [valueXY, valueYX]63          exact dist.symmetric at x, y with *64        . intros x hx y hy z hz65          have typedX : Real(x) by exact hx66          have typedY : Real(y) by exact hy67          have typedZ : Real(z) by exact hz68          have valueXZ := realDistance.apply at x, z with *69          have valueXY := realDistance.apply at x, y with *70          have valueYZ := realDistance.apply at y, z with *71          rw [valueXZ, valueXY, valueYZ]72          exact dist.triangle at x, y, z with *7374theorem realDistance.ball (x r : Real)75  shows ball(ℝ, realDistance, x, r) = openBall(x, r)76proof77  ext y78  constructor79  . intro hy80    have hyR := ball.point with hy81    have near := ball.distance with hy82    have typedY : Real(y) by exact hyR83    have value := realDistance.apply at x, y with *84    have symmetric := dist.symmetric at x, y with *85    rw [value, symmetric] at near86    apply openBall.membership.backward87    exact ⟨hyR, near⟩88  . intro hy89    obtain ⟨hyR, near⟩ := openBall.membership.forward with hy90    have typedY : Real(y) by exact hyR91    have value := realDistance.apply at x, y with *92    have symmetric := dist.symmetric at x, y with *93    apply ball.of_distance with hyR94    rw [value, symmetric]95    exact near9697theorem realDistance.closedBall (x r : Real)98  shows closedBall(ℝ, realDistance, x, r) = closedInterval(x - r, x + r)99proof100  ext y101  constructor102  . intro hy103    have hyR := closedBall.point with hy104    have near := closedBall.distance with hy105    have typedY : Real(y) by exact hyR106    have value := realDistance.apply at x, y with *107    rw value at near108    unfold dist at near109    have upper := abs.upper at x - y110    have upperNeg := abs.upper_neg at x - y111    apply closedInterval.membership.backward112    refine ⟨hyR, ?_, ?_⟩113    . linarith114    . linarith115  . intro hy116    obtain ⟨hyR, lower, upper⟩ := closedInterval.membership.forward with hy117    have typedY : Real(y) by exact hyR118    have value := realDistance.apply at x, y with *119    apply closedBall.of_distance with hyR120    rw value121    unfold dist122    have sign := realLess.trichotomy at (0:R), x - y123    rcases sign with positive | zero | negative124    . have nonnegative : 0 ≤ x - y by linarith125      have unfolded := abs.of_nonnegative with nonnegative126      rw unfolded127      linarith128    . have nonnegative : 0 ≤ x - y by linarith129      have unfolded := abs.of_nonnegative with nonnegative130      rw unfolded131      linarith132    . have nonpositive : x - y ≤ 0 by linarith133      have unfolded := abs.of_nonpositive with nonpositive134      rw unfolded135      linarith136137theorem realDistance.topology138  shows metricTopology(ℝ, realDistance) = realTopology139proof140  ext U141  constructor142  . intro hU143    obtain ⟨bound, balls⟩ := metricTopology.membership.forward with hU144    have inside := powerset.membership_iff.forward with bound145    apply realTopology.membership.backward146    refine ⟨bound, ?_⟩147    intros x hx148    obtain ⟨E, hE, positive, ballInside⟩ := balls with x, hx149    have typedX : Real(x) by exact inside with x, hx150    have typedE : Real(E) by exact hE151    have same := realDistance.ball at x, E with *152    rw same at ballInside153    exact ⟨E, hE, positive, ballInside⟩154  . intro hU155    obtain ⟨bound, balls⟩ := realTopology.membership.forward with hU156    have inside := powerset.membership_iff.forward with bound157    apply metricTopology.membership.backward158    refine ⟨bound, ?_⟩159    intros x hx160    obtain ⟨E, hE, positive, ballInside⟩ := balls with x, hx161    have typedX : Real(x) by exact inside with x, hx162    have typedE : Real(E) by exact hE163    have same := realDistance.ball at x, E with *164    rw ← same at ballInside165    exact ⟨E, hE, positive, ballInside⟩166167theorem realDistance.hausdorff168  shows IsHausdorff(ℝ, metricTopology(ℝ, realDistance))169proof170  exact metricTopology.hausdorff with realDistance.metric171172-- ε–δ continuity of a real function is metric continuity for realDistance.173theorem realDistance.continuous_iff (f : Set)174  shows Continuous(f) ↔ IsMetricContinuous(f, ℝ, realDistance, ℝ, realDistance)175proof176  have metric := realDistance.metric177  have topological := Continuous.continuous_map at f178  have metrical := IsMetricContinuous.iff_continuous_map at179    f, ℝ, realDistance, ℝ, realDistance with metric, metric180  rw realDistance.topology at metrical181  constructor182  . intro continuous183    exact metrical.backward with (topological.forward with continuous)184  . intro continuous185    exact topological.backward with (metrical.forward with continuous)186187theorem realDistance.converges_iff (u : Set) (L : Real)188  shows ConvergesTo(u, L) ↔ ConvergesIn(ℝ, realDistance, u, L)189proof190  have realL : L ∈ ℝ by simp [Real]191  constructor192  . intro converges193    obtain ⟨sequence, tail⟩ := converges194    have function : u : ℕ → ℝ by exact sequence195    have sequenceIn : SequenceIn(ℝ, u) by exact function196    apply ConvergesIn.of_eventually with sequenceIn, realL197    intros ε hε positive198    obtain ⟨N, hN, near⟩ := tail with ε, hε, positive199    refine ⟨N, hN, ?_⟩200    intros n hn le201    have inBall := near with n, hn, le202    obtain ⟨termR, close⟩ := openBall.membership.forward with inBall203    have typedN : Real(u(n)) by exact termR204    have value := realDistance.apply at L, u(n) with *205    have symmetric := dist.symmetric at L, u(n) with *206    rw [value, symmetric]207    exact close208  . intro converges209    have sequenceIn := ConvergesIn.sequence with converges210    have function := SequenceIn.function with sequenceIn211    have sequence : RealSequence(u) by exact function212    constructor213    . exact sequence214    . intros ε hε positive215      obtain ⟨N, hN, near⟩ := ConvergesIn.eventually with converges, positive216      refine ⟨N, hN, ?_⟩217      intros n hn le218      have close := near with n, hn, le219      have termR := SequenceIn.term_of_member with sequenceIn, hn220      have typedN : Real(u(n)) by exact termR221      have value := realDistance.apply at L, u(n) with *222      have symmetric := dist.symmetric at L, u(n) with *223      rw [value, symmetric] at close224      apply openBall.membership.backward225      exact ⟨termR, close⟩226227-- The real line is complete: a Cauchy sequence is bounded, so it lies in a228-- closed interval, where Bolzano–Weierstrass provides a convergent229-- subsequence, whose limit the whole sequence then approaches.230theorem realDistance.complete231  shows IsComplete(ℝ, realDistance)232proof233  have metric := realDistance.metric234  apply IsComplete.of_limits with metric235  intros u cauchy236  have sequenceIn := IsCauchy.sequence with cauchy237  have function := SequenceIn.function with sequenceIn238  have sequence : RealSequence(u) by exact function239  obtain ⟨r, hr, close⟩ := IsCauchy.bounded with metric, cauchy240  have zero : 0 ∈ ℕ by exact nat.omega.forward at 0 with241    Naturals.constructor.zero242  have term0 := SequenceIn.term_of_member with sequenceIn, zero243  have typed0 : Real(u(0)) by exact term0244  have typedR : Real(r) by exact hr245  have terms : TermsIn(u, closedInterval(u(0) - r, u(0) + r))246    intros n hn247    have termN := SequenceIn.term_of_member with sequenceIn, hn248    have typedN : Real(u(n)) by exact termN249    have near := close with n, hn250    have value := realDistance.apply at u(0), u(n) with *251    rw value at near252    unfold dist at near253    have upper := abs.upper at u(0) - u(n)254    have upperNeg := abs.upper_neg at u(0) - u(n)255    apply closedInterval.membership.backward256    refine ⟨termN, ?_, ?_⟩257    . linarith258    . linarith259  obtain ⟨k, increasing, L, hL, inInterval, converges⟩ :=260    closedInterval.bolzano_weierstrass with sequence, terms261  have typedL : Real(L) by exact hL262  have bridge := realDistance.converges_iff at subsequence(u, k), L with *263  have subConverges := bridge.forward with converges264  unfold subsequence at subConverges265  have limit := IsCauchy.converges_of_subsequence with266    metric, cauchy, increasing, subConverges267  exact ⟨L, hL, limit⟩268