Grace/Cumulus/Geometry/Distance.g17

Open in Workbench Download source

Imports

Plane · Real.Sqrt

Declarations

Source

1-- Euclidean distance in the plane and the triangle inequality.2-- 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.Geometry.Distance8import Plane9import Real.Sqrt1011namespace Euclidean12export open Euclidean1314-- Section: Cauchy-Schwarz in the plane1516-- The difference of the two sides is the square of a cross term.17theorem angleDot.cauchy_schwarz (a b c : Point)18  shows angleDot(a, b, c) * angleDot(a, b, c) ≤ Euclidean.distanceSquared(b, a) * Euclidean.distanceSquared(b, c)19proof20  have dotRule := angleDot.coordinates at a, b, c with *21  have firstRule := Euclidean.distanceSquared.coordinates at b, a with *22  have secondRule := Euclidean.distanceSquared.coordinates at b, c with *23  have crossNonnegative := realMulValue.square_nonnegative at (x(a) - x(b)) * (y(c) - y(b)) - (y(a) - y(b)) * (x(c) - x(b)) with *24  have difference : Euclidean.distanceSquared(b, a) * Euclidean.distanceSquared(b, c) - angleDot(a, b, c) * angleDot(a, b, c) =25      ((x(a) - x(b)) * (y(c) - y(b)) - (y(a) - y(b)) * (x(c) - x(b))) * ((x(a) - x(b)) * (y(c) - y(b)) - (y(a) - y(b)) * (x(c) - x(b)))26    rw [dotRule, firstRule, secondRule]27    ring28  have nonnegativeDifference : 0 ≤ Euclidean.distanceSquared(b, a) * Euclidean.distanceSquared(b, c) - angleDot(a, b, c) * angleDot(a, b, c)29    rwa difference30  exact realLe.of_nonnegative_difference with *3132-- Section: Distance3334theorem Euclidean.distanceSquared.nonnegative_real (a b : Point)35  shows NonnegativeReal(Euclidean.distanceSquared(a, b))36proof37  have le := Euclidean.distanceSquared.nonnegative at a, b with *38  exact NonnegativeReal.of_le with *3940def distance (a b : Point) : Real := sqrt(Euclidean.distanceSquared(a, b))4142theorem distance.real (a b : Point)43  shows Real(distance(a, b))44proof45  typecheck4647theorem distance.nonnegative (a b : Point)48  shows 0 ≤ distance(a, b)49proof50  have nonnegative := Euclidean.distanceSquared.nonnegative_real at a, b with *51  have root := sqrt.nonnegative with nonnegative52  unfold distance53  exact root5455theorem distance.square (a b : Point)56  shows distance(a, b) * distance(a, b) = Euclidean.distanceSquared(a, b)57proof58  have nonnegative := Euclidean.distanceSquared.nonnegative_real at a, b with *59  have square := sqrt.square with nonnegative60  unfold distance61  cc6263theorem distance.symmetric (a b : Point)64  shows distance(a, b) = distance(b, a)65proof66  have swap := Euclidean.distanceSquared.symmetric at a, b with *67  unfold distance68  cc6970theorem distance.eq_zero_iff (a b : Point)71  shows distance(a, b) = 0 ↔ a = b72proof73  have squared := Euclidean.distanceSquared.zero_iff at a, b with *74  have square := distance.square at a, b with *75  constructor76  . intro zero77    have squareZero : Euclidean.distanceSquared(a, b) = 078      rw [← square, zero]79      exact realMulValue.zero_left with realZero.real80    exact squared.forward with squareZero81  . intro equal82    have squareZero := squared.backward with equal83    have root : distance(a, b) * distance(a, b) = 0 by rwa square84    exact realMulValue.square_eq_zero_iff.forward with root8586theorem distance.positive_of_ne (a b : Point)87  requires distinct : a ≠ b88  shows 0 < distance(a, b)89proof90  have nonnegative := Euclidean.distanceSquared.nonnegative_real at a, b with *91  have positiveSquare := Euclidean.distanceSquared.positive with *92  have nonzero : Euclidean.distanceSquared(a, b) ≠ 093    intro zero94    rw zero at positiveSquare95    exact realLess.not_self with realZero.real, positiveSquare96  have root := sqrt.positive with nonnegative, nonzero97  unfold distance98  exact root99100-- Section: Triangle inequality101102-- Cauchy-Schwarz as a lower bound on the dot product of two rays.103theorem angleDot.lower_bound (a b c : Point)104  shows 0 ≤ angleDot(a, b, c) + distance(b, a) * distance(b, c)105proof106  have dotReal := angleDot.real at a, b, c with *107  have firstNonnegative := distance.nonnegative at b, a with *108  have secondNonnegative := distance.nonnegative at b, c with *109  have productNonnegative := realMulValue.nonnegative at distance(b, a), distance(b, c) with *110  have firstSquare := distance.square at b, a with *111  have secondSquare := distance.square at b, c with *112  have productSquare : (distance(b, a) * distance(b, c)) * (distance(b, a) * distance(b, c)) = Euclidean.distanceSquared(b, a) * Euclidean.distanceSquared(b, c)113    rw [← firstSquare, ← secondSquare]114    ring115  have schwarz := angleDot.cauchy_schwarz at a, b, c with *116  rw ← productSquare at schwarz117  have sign := Real.sign_cases with dotReal118  cases sign with nonpositive | nonnegative119  . have negReal := realNegValue.real at angleDot(a, b, c) with dotReal120    have negNonnegative := realNegValue.nonnegative_of_nonpositive with nonpositive121    have negLe := realLe.of_subset with realZero.real, negNonnegative122    have negSquare := realMulValue.neg_both at angleDot(a, b, c), angleDot(a, b, c) with *123    have negSchwarz : (-angleDot(a, b, c)) * (-angleDot(a, b, c)) ≤ (distance(b, a) * distance(b, c)) * (distance(b, a) * distance(b, c))124      rwa negSquare125    have negLeProduct := realMulValue.le_of_square_le at -angleDot(a, b, c), distance(b, a) * distance(b, c) with *126    have shifted := realLe.add_right at -angleDot(a, b, c), distance(b, a) * distance(b, c), angleDot(a, b, c) with *127    have cancel : -angleDot(a, b, c) + angleDot(a, b, c) = 0 by ring128    rw cancel at shifted129    have swap : distance(b, a) * distance(b, c) + angleDot(a, b, c) = angleDot(a, b, c) + distance(b, a) * distance(b, c)130      ring131    rwa swap at shifted132  . have dotLe := realLe.of_subset at realZero, angleDot(a, b, c) with realZero.real, nonnegative133    have sum := realLe.add at realZero, angleDot(a, b, c), realZero, distance(b, a) * distance(b, c) with *134    have zeroZero := realAddValue.zero_right with realZero.real135    rwa zeroZero at sum136137theorem distance.triangle (a b c : Point)138  shows distance(a, c) ≤ distance(a, b) + distance(b, c)139proof140  have acNonnegative := distance.nonnegative at a, c with *141  have abNonnegative := distance.nonnegative at a, b with *142  have bcNonnegative := distance.nonnegative at b, c with *143  have sumNonnegative : 0 ≤ distance(a, b) + distance(b, c)144    have step := realLe.add at realZero, distance(a, b), realZero, distance(b, c) with *145    have zeroZero := realAddValue.zero_right with realZero.real146    rwa zeroZero at step147  have acSquare := distance.square at a, c with *148  have abSquare := distance.square at a, b with *149  have bcSquare := distance.square at b, c with *150  have symmetric := distance.symmetric at b, a with *151  have bound := angleDot.lower_bound at a, b, c with *152  rw symmetric at bound153  have identity := cosine_identity at a, b, c with *154  have doubled : 0 ≤ (angleDot(a, b, c) + distance(a, b) * distance(b, c)) + (angleDot(a, b, c) + distance(a, b) * distance(b, c))155    have step := realLe.add at realZero, angleDot(a, b, c) + distance(a, b) * distance(b, c), realZero, angleDot(a, b, c) + distance(a, b) * distance(b, c) with *156    have zeroZero := realAddValue.zero_right with realZero.real157    rwa zeroZero at step158  have difference : (distance(a, b) + distance(b, c)) * (distance(a, b) + distance(b, c)) - distance(a, c) * distance(a, c) =159      (angleDot(a, b, c) + distance(a, b) * distance(b, c)) + (angleDot(a, b, c) + distance(a, b) * distance(b, c))160    linear_combination abSquare + bcSquare - acSquare - identity161  have nonnegativeDifference : 0 ≤ (distance(a, b) + distance(b, c)) * (distance(a, b) + distance(b, c)) - distance(a, c) * distance(a, c)162    rwa difference163  have squares := realLe.of_nonnegative_difference with *164  exact realMulValue.le_of_square_le with *165166end Euclidean167