Grace/Cumulus/Real/Sqrt.g17

Open in Workbench Download source

Imports

Squares · Order

Declarations

Source

1-- Square roots of nonnegative reals, from the least-upper-bound property.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.Real.Sqrt8import Squares9import Order1011-- Section: Squares and order1213theorem realMulValue.square_le_of_le (A B : Real)14  requires nonnegativeA : 0 ≤ A15  requires le : A ≤ B16  shows A * A ≤ B * B17proof18  have nonnegativeB : 0 ≤ B19    exact realLe.transitive with *20  have first := realLe.mul_right_of_nonnegative with le, nonnegativeA21  have second := realLe.mul_left_of_nonnegative with le, nonnegativeB22  exact realLe.transitive with *2324theorem realMulValue.square_lt_of_lt (A B : Real)25  requires nonnegativeA : 0 ≤ A26  requires lt : A < B27  shows A * A < B * B28proof29  have positiveB : 0 < B30    exact realLe.transitive_less with *31  have le := realLess.implies_le at A, B with *32  have first := realLe.mul_right_of_nonnegative with le, nonnegativeA33  have second := realLess.mul_left_of_positive with lt, positiveB34  exact realLe.transitive_less with *3536theorem realMulValue.le_of_square_le (A B : Real)37  requires nonnegativeA : 0 ≤ A38  requires nonnegativeB : 0 ≤ B39  requires squares : A * A ≤ B * B40  shows A ≤ B41proof42  have notLess : ¬(B < A)43    intro less44    have strict := realMulValue.square_lt_of_lt with nonnegativeB, less45    exact realLe.not_less with squares, strict46  exact realLe.of_not_less with *4748theorem realMulValue.eq_of_square_eq (A B : Real)49  requires nonnegativeA : 0 ≤ A50  requires nonnegativeB : 0 ≤ B51  requires squares : A * A = B * B52  shows A = B53proof54  have le : A * A ≤ B * B55    rw squares56    exact realLe.reflexive with *57  have ge : B * B ≤ A * A58    rw squares59    exact realLe.reflexive with *60  have ab := realMulValue.le_of_square_le at A, B with *61  have ba := realMulValue.le_of_square_le at B, A with *62  exact realLe.antisymmetric with *6364-- Section: Candidates below the square root6566-- The nonnegative reals whose square does not exceed X.67def sqrtCandidates (X : Real) : Set :=68  { T ∈ ℝ | (0:R) ≤ (T:R) ∧ (T:R) * (T:R) ≤ X }6970theorem sqrtCandidates.subset_reals (X : Real)71  shows sqrtCandidates(X) ⊆ ℝ72proof73  intros T member74  obtain ⟨inReals, _, _⟩ := sqrtCandidates.membership.forward with member75  exact inReals7677theorem sqrtCandidates.zero (X : Real)78  requires nonnegative : 0 ≤ X79  shows realZero ∈ sqrtCandidates(X)80proof81  have zeroIn : realZero ∈ ℝ by typecheck82  have zeroLe := realLe.reflexive with realZero.real83  have square := realMulValue.zero_left with realZero.real84  have squareLe : realZero * realZero ≤ X by rwa square85  have conjunction : realZero ∈ ℝ ∧ 0 ≤ realZero ∧ realZero * realZero ≤ X by refine ⟨zeroIn, zeroLe, squareLe⟩86  exact sqrtCandidates.membership.backward with conjunction8788theorem sqrtCandidates.nonempty (X : Real)89  requires nonnegative : 0 ≤ X90  shows Nonempty(sqrtCandidates(X))91proof92  witness realZero93  exact sqrtCandidates.zero with *9495-- Every candidate is at most X + 1: a larger T would satisfy T < T * T.96theorem sqrtCandidates.bounded (X : Real)97  requires nonnegative : 0 ≤ X98  shows RealUpperBound(sqrtCandidates(X), X + 1)99proof100  have boundReal : Real(X + 1) by typecheck101  have subset := sqrtCandidates.subset_reals at X102  unfold RealUpperBound103  refine ⟨boundReal, subset, _⟩104  intros T member105  obtain ⟨inReals, nonnegativeT, squareLe⟩ := sqrtCandidates.membership.forward with member106  have realT : Real(T) by exact inReals107  have notLess : ¬(X + 1 < T)108    intro less109    have one := realZero.lt_one110    have oneLess : 1 < T by linarith111    have positiveT : 0 < T by linarith112    have grow : T * 1 < T * T113      exact realLess.mul_left_of_positive with *114    have unit := realMulValue.one_right with realT115    rw unit at grow116    linarith117  have le := realLe.of_not_less with *118  exact realLe.subset with le119120-- Section: Existence121122-- The supremum of the candidates squares to X: if its square fell short, a123-- slightly larger candidate would exist; if it exceeded X, a slightly smaller124-- upper bound would.125theorem realSqrt.existence (X : Real)126  requires nonnegative : 0 ≤ X127  shows ∃ T ∈ ℝ, (0:R) ≤ (T:R) ∧ (T:R) * (T:R) = X128proof129  have inhabited := sqrtCandidates.nonempty with *130  have bounded : ∃ B, RealUpperBound(sqrtCandidates(X), B) := ⟨X + 1, sqrtCandidates.bounded at X with *⟩131  obtain ⟨U, least⟩ := Real.least_upper_bound_property with inhabited, bounded132  have upper : RealUpperBound(sqrtCandidates(X), U)133    rcases least with ⟨bound, _⟩134    exact bound135  have minimal : ∀ B, RealUpperBound(sqrtCandidates(X), B) → U ⊆ B136    rcases least with ⟨_, minimal⟩137    exact minimal138  rcases upper with ⟨realU, subsetReals, bounds⟩139  have zeroMember := sqrtCandidates.zero with *140  have zeroSubset := bounds with realZero, zeroMember141  have nonnegativeU : 0 ≤ U by exact realLe.of_subset at realZero, U with realZero.real, realU, zeroSubset142  have uIn : U ∈ ℝ by typecheck143  have compare : U * U = X ∨ U * U ≠ X by tauto144  cases compare with equal | different145  . witness U146    refine ⟨uIn, nonnegativeU, equal⟩147  . have connected := realLess.connected_on148    have order := connected with U * U, X, different149    have one := realZero.lt_one150    cases order with below | above151    . -- The square falls short: U + E is a larger candidate, for a small E.152      exfalso153      have positiveD : 0 < X - U * U by linarith154      have positiveW : 0 < U + U + 1 + (X - U * U) by linarith155      have nonzeroW : U + U + 1 + (X - U * U) ≠ 0156        intro zeroW157        rw zeroW at positiveW158        linarith159      have positiveE : 0 < (X - U * U) / (U + U + 1 + (X - U * U))160        have unfolded := realDiv.eq_mul_inv at X - U * U, U + U + 1 + (X - U * U) with *161        rw unfolded162        have positiveInverse := realInvValue.positive at U + U + 1 + (X - U * U) with *163        exact realMulValue.positive with *164      have cancel := realDiv.mul_right at X - U * U, U + U + 1 + (X - U * U) with *165      have eLessOne : (X - U * U) / (U + U + 1 + (X - U * U)) < 1166        have notLess : ¬(1 ≤ (X - U * U) / (U + U + 1 + (X - U * U)))167          intro oneLe168          have nonnegativeW := realLess.implies_le at realZero, U + U + 1 + (X - U * U) with *169          have scaled := realLe.mul_right_of_nonnegative with oneLe, nonnegativeW170          have oneLeft := realMulValue.one_left at U + U + 1 + (X - U * U)171          rw [oneLeft, cancel] at scaled172          linarith173        exact realLess.of_not_le with *174      have eLeOne := realLess.implies_le at (X - U * U) / (U + U + 1 + (X - U * U)), realOne with *175      have nonnegativeE := realLess.implies_le at realZero, (X - U * U) / (U + U + 1 + (X - U * U)) with *176      have squareLeE : ((X - U * U) / (U + U + 1 + (X - U * U))) * ((X - U * U) / (U + U + 1 + (X - U * U))) ≤ (X - U * U) / (U + U + 1 + (X - U * U))177        have step := realLe.mul_left_of_nonnegative at (X - U * U) / (U + U + 1 + (X - U * U)), realOne, (X - U * U) / (U + U + 1 + (X - U * U)) with *178        have unit := realMulValue.one_right at (X - U * U) / (U + U + 1 + (X - U * U))179        rwa unit at step180      have twoUOneLessW : U + U + 1 < U + U + 1 + (X - U * U) by linarith181      have scaledLess := realLess.mul_left_of_positive at U + U + 1, U + U + 1 + (X - U * U), (X - U * U) / (U + U + 1 + (X - U * U)) with *182      rw cancel at scaledLess183      have expansion : (U + (X - U * U) / (U + U + 1 + (X - U * U))) * (U + (X - U * U) / (U + U + 1 + (X - U * U))) =184          U * U + ((U + U) * ((X - U * U) / (U + U + 1 + (X - U * U))) + ((X - U * U) / (U + U + 1 + (X - U * U))) * ((X - U * U) / (U + U + 1 + (X - U * U))))185        ring186      have regroup : (U + U) * ((X - U * U) / (U + U + 1 + (X - U * U))) + (X - U * U) / (U + U + 1 + (X - U * U)) = ((X - U * U) / (U + U + 1 + (X - U * U))) * (U + U + 1)187        ring188      have squareLe : (U + (X - U * U) / (U + U + 1 + (X - U * U))) * (U + (X - U * U) / (U + U + 1 + (X - U * U))) ≤ X189        linarith190      have nonnegativeSum : 0 ≤ U + (X - U * U) / (U + U + 1 + (X - U * U)) by linarith191      have sumIn : U + (X - U * U) / (U + U + 1 + (X - U * U)) ∈ ℝ by typecheck192      have conjunction : U + (X - U * U) / (U + U + 1 + (X - U * U)) ∈ ℝ ∧ (0:R) ≤ U + (X - U * U) / (U + U + 1 + (X - U * U)) ∧ (U + (X - U * U) / (U + U + 1 + (X - U * U))) * (U + (X - U * U) / (U + U + 1 + (X - U * U))) ≤ X193        refine ⟨sumIn, nonnegativeSum, squareLe⟩194      have sumMember := sqrtCandidates.membership.backward with conjunction195      have sumSubset := bounds with U + (X - U * U) / (U + U + 1 + (X - U * U)), sumMember196      have sumLe := realLe.of_subset at U + (X - U * U) / (U + U + 1 + (X - U * U)), U with *197      linarith198    . -- The square exceeds X: U - E is a smaller upper bound, for a small E.199      exfalso200      have nonzeroU : U ≠ 0201        intro uZero202        rw uZero at above203        have zeroSquare := realMulValue.zero_left with realZero.real204        rw zeroSquare at above205        linarith206      have positiveU := Real.positive_of_nonnegative_of_ne_zero with realU, nonnegativeU, nonzeroU207      have positiveD : 0 < U * U - X by linarith208      have positiveTwoU : 0 < U + U by linarith209      have nonzeroTwoU : U + U ≠ 0210        intro zeroTwoU211        rw zeroTwoU at positiveTwoU212        linarith213      have positiveE : 0 < (U * U - X) / (U + U)214        have unfolded := realDiv.eq_mul_inv at U * U - X, U + U with *215        rw unfolded216        have positiveInverse := realInvValue.positive at U + U with *217        exact realMulValue.positive with *218      have cancel := realDiv.mul_right at U * U - X, U + U with *219      have eLessU : (U * U - X) / (U + U) < U220        have notLe : ¬(U ≤ (U * U - X) / (U + U))221          intro uLe222          have nonnegativeTwoU := realLess.implies_le at realZero, U + U with *223          have scaled := realLe.mul_right_of_nonnegative at U, (U * U - X) / (U + U), U + U with *224          rw cancel at scaled225          have doubled : U * (U + U) = U * U + U * U by ring226          have positiveSquare := realMulValue.square_positive with realU, nonzeroU227          linarith228        exact realLess.of_not_le with *229      have positiveV : 0 < U - (U * U - X) / (U + U) by linarith230      have nonnegativeV := realLess.implies_le at realZero, U - (U * U - X) / (U + U) with *231      have expansion : (U - (U * U - X) / (U + U)) * (U - (U * U - X) / (U + U)) =232          U * U - ((U * U - X) / (U + U)) * (U + U) + ((U * U - X) / (U + U)) * ((U * U - X) / (U + U))233        ring234      rw cancel at expansion235      have nonnegativeSquare := realMulValue.square_nonnegative at (U * U - X) / (U + U)236      have xLeSquare : X ≤ (U - (U * U - X) / (U + U)) * (U - (U * U - X) / (U + U)) by linarith237      have realV : Real(U - (U * U - X) / (U + U)) by typecheck238      have upperV : RealUpperBound(sqrtCandidates(X), U - (U * U - X) / (U + U))239        unfold RealUpperBound240        refine ⟨realV, subsetReals, _⟩241        intros T member242        obtain ⟨inReals, nonnegativeT, squareLe⟩ := sqrtCandidates.membership.forward with member243        have squares : T * T ≤ (U - (U * U - X) / (U + U)) * (U - (U * U - X) / (U + U)) by linarith244        have le := realMulValue.le_of_square_le with *245        exact realLe.subset with le246      have uSubset := minimal with U - (U * U - X) / (U + U), upperV247      have uLe := realLe.of_subset at U, U - (U * U - X) / (U + U) with *248      linarith249250-- Section: The square root251252-- Nonnegative reals as a soft type, so that sqrt has a real result.253predicate NonnegativeReal (X : Set) := Real(X) ∧ (0:R) ≤ (X:R)254255theorem NonnegativeReal.real (X : NonnegativeReal)256  shows Real(X)257proof258  have nonnegative : NonnegativeReal(X) by assumption259  rcases nonnegative with ⟨realX, _⟩260  exact realX261262theorem NonnegativeReal.le (X : NonnegativeReal)263  shows 0 ≤ X264proof265  have nonnegative : NonnegativeReal(X) by assumption266  rcases nonnegative with ⟨_, le⟩267  exact le268269theorem NonnegativeReal.of_le (X : Real)270  requires nonnegative : 0 ≤ X271  shows NonnegativeReal(X)272proof273  have realX : Real(X) by typecheck274  unfold NonnegativeReal275  refine ⟨realX, nonnegative⟩276277theorem realZero.nonnegative_real278  shows NonnegativeReal(realZero)279proof280  have le := realLe.reflexive with realZero.real281  exact NonnegativeReal.of_le with realZero.real, le282283theorem realMulValue.square_nonnegative_real (T : Real)284  shows NonnegativeReal(T * T)285proof286  have le := realMulValue.square_nonnegative at T287  exact NonnegativeReal.of_le with *288289theorem NonnegativeReal.mul (X Y : NonnegativeReal)290  shows NonnegativeReal(X * Y)291proof292  have leX := NonnegativeReal.le at X293  have leY := NonnegativeReal.le at Y294  have le := realMulValue.nonnegative at X, Y with *295  exact NonnegativeReal.of_le with *296297theorem NonnegativeReal.add (X Y : NonnegativeReal)298  shows NonnegativeReal(X + Y)299proof300  have leX := NonnegativeReal.le at X301  have leY := NonnegativeReal.le at Y302  have step := realLe.add at realZero, X, realZero, Y with *303  have zeroZero := realAddValue.zero_right with realZero.real304  rw zeroZero at step305  exact NonnegativeReal.of_le with *306307defunique realSqrt (X : Real) (T ∈ ℝ) := (0:R) ≤ (T:R) ∧ (T:R) * (T:R) = X308requires nonnegative : 0 ≤ X309proof310  exact realSqrt.existence with *311uniqueness312  intros T tMember first S sMember second313  rcases first with ⟨nonnegativeT, squareT⟩314  rcases second with ⟨nonnegativeS, squareS⟩315  have squares : T * T = S * S316    rw [squareT, squareS]317    rfl318  exact realMulValue.eq_of_square_eq with *319320def sqrt (X : NonnegativeReal) : Real := realSqrt(X)321proof322  have le := NonnegativeReal.le at X with assumption323  have realX := NonnegativeReal.real at X with assumption324  have selected := realSqrt.selected at X with realX, le325  rcases selected with ⟨member, _⟩326  unfold sqrt327  unfold Real328  exact member329330notation prefix 90 "√" => sqrt for Real331332theorem sqrt.real (X : NonnegativeReal)333  shows Real(√X)334proof335  typecheck336337theorem sqrt.nonnegative (X : NonnegativeReal)338  shows 0 ≤ √X339proof340  have le := NonnegativeReal.le with assumption341  have realX := NonnegativeReal.real with assumption342  obtain ⟨_, nonnegative, _⟩ := realSqrt.selected with le343  unfold sqrt344  exact nonnegative345346theorem sqrt.square (X : NonnegativeReal)347  shows √X * √X = X348proof349  have le := NonnegativeReal.le with assumption350  obtain ⟨_, _, square⟩ := realSqrt.selected with le351  unfold sqrt352  cc353354theorem sqrt.unique (X : NonnegativeReal) (T : Real)355  requires nonnegative : 0 ≤ T356  requires square : T * T = X357  shows T = √X358proof359  have rootNonnegative := sqrt.nonnegative at X360  have rootSquare := sqrt.square at X361  have squares : T * T = √X * √X362    rw [square, rootSquare]363    rfl364  exact realMulValue.eq_of_square_eq with *365366theorem sqrt.of_square (T : Real)367  requires nonnegative : 0 ≤ T368  shows √(T * T) = T369proof370  have squareNonnegative := realMulValue.square_nonnegative_real at T371  have reflexiveSquare : T * T = T * T by rfl372  have unique := sqrt.unique with squareNonnegative, nonnegative, reflexiveSquare373  cc374375theorem sqrt.zero376  shows √realZero = realZero377proof378  have zeroNonnegative := realZero.nonnegative_real379  have le := realLe.reflexive with realZero.real380  have square := realMulValue.zero_left with realZero.real381  have unique := sqrt.unique with *382  cc383384theorem sqrt.mul (X Y : NonnegativeReal)385  shows √(X * Y) = √X * √Y386proof387  have productNonnegative := NonnegativeReal.mul at X, Y with *388  have rootX := sqrt.nonnegative at X389  have rootY := sqrt.nonnegative at Y390  have squareX := sqrt.square at X391  have squareY := sqrt.square at Y392  have productRoots := realMulValue.nonnegative at √X, √Y with *393  have identity : (√X * √Y) * (√X * √Y) = (√X * √X) * (√Y * √Y) by ring394  rw [squareX, squareY] at identity395  have unique := sqrt.unique with *396  cc397398theorem sqrt.le_of_le (X Y : Real)399  requires nonnegativeX : NonnegativeReal(X)400  requires nonnegativeY : NonnegativeReal(Y)401  requires le : X ≤ Y402  shows √X ≤ √Y403proof404  have rootX := sqrt.nonnegative with nonnegativeX405  have rootY := sqrt.nonnegative with nonnegativeY406  have squareX := sqrt.square with nonnegativeX407  have squareY := sqrt.square with nonnegativeY408  have squares : √X * √X ≤ √Y * √Y by rwa [squareX, squareY]409  exact realMulValue.le_of_square_le with *410411theorem sqrt.positive (X : NonnegativeReal)412  requires nonzero : X ≠ 0413  shows 0 < √X414proof415  have rootNonnegative := sqrt.nonnegative at X416  have square := sqrt.square with assumption417  have rootNonzero : √X ≠ 0418    intro zero419    apply nonzero420    rw zero at square421    have zeroSquare := realMulValue.zero_left with realZero.real422    rw zeroSquare at square423    cc424  exact Real.positive_of_nonnegative_of_ne_zero with *425