Grace/Cumulus/Real/Squares.g17

Open in Workbench Download source

Imports

Inverse · Algebra.OrderedField.Core

Declarations

Source

1-- Squares in the Dedekind real numbers2-- 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.Squares8import Inverse9import Algebra.OrderedField.Core1011-- The product of two nonnegative reals is nonnegative.  This is the12-- non-strict companion to the ordered-field positive-product law.13theorem realMulValue.nonnegative (A B : Real)14  requires nonnegativeA : 0 ≤ A15  requires nonnegativeB : 0 ≤ B16  shows 0 ≤ A * B17proof18  have subsetA := realLe.subset with realZero.real, nonnegativeA19  have subsetB := realLe.subset with realZero.real, nonnegativeB20  have valueCut := realMulValue.cut at A, B with *21  have reduction := realMulCut.of_nonnegative with subsetA, subsetB22  apply realLe.of_subset with realZero.real23  rw [valueCut, reduction]24  exact realPosMulCut.nonnegative2526instance reals.ordered_ring27  shows OrderedRing(ℝ, realAdd, realZero, realNeg, realMul, realOne, realLe)28proof29  constructor30  . exact reals.comm_ring31  . constructor32    . exact reals.ordered_additive_group33    . constructor34        intros x hx y hy xy yx35        have subsetXY := realLe.subset with xy36        have subsetYX := realLe.subset with yx37        exact Subset.antisymmetric with subsetXY, subsetYX38      . intros x hx y hy nonnegativeX nonnegativeY39        exact realMulValue.nonnegative with nonnegativeX, nonnegativeY4041-- The algebraic rearrangement behind multiplicative monotonicity.42theorem realMulValue.add_mul_sub (A B C : Real)43  shows A * C + C * (B - A) = B * C44proof45  have differenceReal := realSubValue.real at B, A with *46  have acReal := realMulValue.real at A, C with *47  have differenceProductReal := realMulValue.real at B - A, C with48    differenceReal, assumption49  have productSwap := realMulValue.commutative at C, B - A with50    assumption, differenceReal51  have distributed := realMulValue.distributive_right at B - A, A, C with52    differenceReal, *{2}53  have cancellation := realSubValue.add_right_cancel at B, A with54    *{2}55  rw cancellation at distributed56  have sumSwap := realAddValue.commutative with acReal, differenceProductReal57  calc58    A * C + C * (B - A) = A * C + (B - A) * C := by cc59    _ = (B - A) * C + A * C := sumSwap60    _ = B * C := by cc6162-- Multiplication by a nonnegative real preserves non-strict order.  The proof63-- is the usual difference argument: B = A + (B - A), and C(B - A) is64-- nonnegative.65theorem realLe.mul_right_of_nonnegative (A B C : Real)66  requires ab : A ≤ B67  requires nonnegativeC : 0 ≤ C68  shows A * C ≤ B * C69proof70  have negAReal := realNegValue.real at A71  have differenceReal := realSubValue.real at B, A with *72  have translated := realLe.add_right at A, B, -A with73    *{2}, negAReal, ab74  have inverse := realAddValue.neg_right at A75  rw inverse at translated76  have differenceNonnegative : 0 ≤ B - A77    unfold realSubValue78    exact translated79  have productNonnegative := realMulValue.nonnegative at C, B - A with80    assumption, differenceReal, nonnegativeC, differenceNonnegative81  have productReal := realMulValue.real at C, B - A with82    assumption, differenceReal83  have acReal := realMulValue.real at A, C with *84  have step := realLe.add_left with realZero.real, productReal, acReal, productNonnegative85  have zero := realAddValue.zero_right with acReal86  rw zero at step87  have expansion := realMulValue.add_mul_sub at A, B, C with88    *{3}89  rwa expansion at step9091theorem realLe.mul_left_of_nonnegative (A B C : Real)92  requires ab : A ≤ B93  requires nonnegativeC : 0 ≤ C94  shows C * A ≤ C * B95proof96  have result := realLe.mul_right_of_nonnegative with ab, nonnegativeC97  have left := realMulValue.commutative at A, C with *98  have right := realMulValue.commutative at B, C with *99  rwa [left, right] at result100101-- The strict companion used in epsilon estimates.102theorem realLess.mul_right_of_positive (A B C : Real)103  requires ab : A < B104  requires positiveC : 0 < C105  shows A * C < B * C106proof107  have negAReal := realNegValue.real at A108  have differenceReal := realSubValue.real at B, A with *109  have translated := realLess.add_right at A, B, -A with110    *{2}, negAReal, ab111  have inverse := realAddValue.neg_right at A112  rw inverse at translated113  have differencePositive : 0 < B - A114    unfold realSubValue115    exact translated116  have productPositive := realMulValue.positive at C, B - A with117    assumption, differenceReal, positiveC, differencePositive118  have productReal := realMulValue.real at C, B - A with119    assumption, differenceReal120  have acReal := realMulValue.real at A, C with *121  have step := realLess.add_left with realZero.real, productReal, acReal, productPositive122  have zero := realAddValue.zero_right with acReal123  rw zero at step124  have expansion := realMulValue.add_mul_sub at A, B, C with125    *{3}126  rwa expansion at step127128theorem realLess.mul_left_of_positive (A B C : Real)129  requires ab : A < B130  requires positiveC : 0 < C131  shows C * A < C * B132proof133  have result := realLess.mul_right_of_positive with ab, positiveC134  have left := realMulValue.commutative at A, C with *135  have right := realMulValue.commutative at B, C with *136  rwa [left, right] at result137138theorem realInvValue.positive (A : Real)139  requires positive : 0 < A140  shows 0 < realInvValue(A)141proof142  have generic := IsOrderedField.positive_inverse with reals.ordered_field, positive143  unfold realInvValue144  exact generic145146-- Reciprocation reverses strict order on the positive reals.147theorem realInvValue.antitone_positive (A B : Real)148  requires positiveA : 0 < A149  requires less : A < B150  shows realInvValue(B) < realInvValue(A)151proof152  have positiveB := realLess.transitive with realZero.real, positiveA, less153  have inverseAPositive := realInvValue.positive with positiveA154  have inverseBPositive := realInvValue.positive with positiveB155  have nonzeroA : A ≠ 0156    intro equal157    rw equal at positiveA158    have irreflexive := realLess.irreflexive_on159    exact irreflexive with realZero, positiveA160  have nonzeroB : B ≠ 0161    intro equal162    rw equal at positiveB163    have irreflexive := realLess.irreflexive_on164    exact irreflexive with realZero, positiveB165  have first := realLess.mul_right_of_positive at166    A, B, realInvValue(A) with167      *{2}, realInvValue.real at A with assumption,168      less, inverseAPositive169  have inverseA := realInvValue.mul_right with nonzeroA170  rw inverseA at first171  have inverseAReal := realInvValue.real at A172  have inverseBReal := realInvValue.real at B173  have bInverseAReal := realMulValue.real at B, realInvValue(A) with174    assumption, inverseAReal175  have second := realLess.mul_left_of_positive with176    realOne.real, bInverseAReal, inverseBReal, first, inverseBPositive177  have inverseB := realInvValue.mul_left with nonzeroB178  have associative := realMulValue.associative at179    realInvValue(B), B, realInvValue(A) with180      inverseBReal, assumption, inverseAReal181  have oneLeft := realMulValue.one_left with inverseAReal182  have oneRight := realMulValue.one_right with inverseBReal183  rwa [oneRight, ← associative, inverseB, oneLeft] at second184185-- Every square is nonnegative.  For a nonpositive A, apply the preceding186-- result to -A and use (-A)(-A) = A².187theorem realMulValue.square_nonnegative (A : Real)188  shows 0 ≤ A * A189proof190  have sign := Real.sign_cases at A191  cases sign with nonpositive | nonnegative192  . have negAReal := realNegValue.real at A193    have negANonnegative := realNegValue.nonnegative_of_nonpositive with nonpositive194    have negALe := realLe.of_subset with realZero.real, negANonnegative195    have square := realMulValue.nonnegative with negALe, negALe196    have negSquare := realMulValue.neg_both at A, A with *197    rwa negSquare at square198  . have nonnegativeLe := realLe.of_subset at realZero, A with199      realZero.real, assumption, nonnegative200    exact realMulValue.nonnegative with nonnegativeLe, nonnegativeLe201202theorem Real.positive_of_nonnegative_of_ne_zero (A : Real)203  requires nonnegative : 0 ≤ A204  requires nonzero : A ≠ 0205  shows 0 < A206proof207  have subset := realLe.subset with realZero.real, nonnegative208  have zeroNeA : realZero ≠ A209    intro zeroA210    apply nonzero211    cc212  apply realLess.characterization.backward213  unfold RealLess214  refine ⟨realZero.real, assumption, _⟩215  constructor216  . exact subset217  . exact zeroNeA218219-- A nonzero square is strictly positive.  This is the order-theoretic heart220-- of the familiar fact that the reals have no nontrivial nilpotents.221theorem realMulValue.square_positive (A : Real)222  requires nonzero : A ≠ 0223  shows 0 < A * A224proof225  have sign := Real.sign_cases at A226  cases sign with nonpositive | nonnegative227  . have negAReal := realNegValue.real at A228    have negANonnegative := realNegValue.nonnegative_of_nonpositive with nonpositive229    have negALe := realLe.of_subset with realZero.real, negANonnegative230    have negANonzero : -A ≠ 0231      intro negAZero232      apply nonzero233      have involutive := realNegValue.involutive at A234      calc235        A = -(-A) := by cc236        _ = -realZero := by cc237        _ = realZero := realNegValue.zero238    have positiveNegA := Real.positive_of_nonnegative_of_ne_zero with negALe, negANonzero239    have positiveSquare := realMulValue.positive with positiveNegA, positiveNegA240    have negSquare := realMulValue.neg_both at A, A with *241    rwa negSquare at positiveSquare242  . have nonnegativeLe := realLe.of_subset at realZero, A with243      realZero.real, assumption, nonnegative244    have positiveA := Real.positive_of_nonnegative_of_ne_zero with nonnegativeLe, nonzero245    exact realMulValue.positive with positiveA, positiveA246247theorem realMulValue.square_eq_zero_iff (A : Real)248  shows A * A = 0 ↔ A = 0249proof250  constructor251  . intro squareZero252    by_contra nonzero253    have positive := realMulValue.square_positive with nonzero254    rw squareZero at positive255    have irreflexive := realLess.irreflexive_on256    exact irreflexive with realZero, positive257  . intro zeroA258    rw zeroA259    exact realMulValue.zero_left with realZero.real260261theorem realAddValue.sum_squares_nonnegative (A B : Real)262  shows 0 ≤ A * A + B * B263proof264  have squareALe := realMulValue.square_nonnegative at A265  have squareBLe := realMulValue.square_nonnegative at B266  have squareASubset := realLe.subset with realZero.real, squareALe267  have squareBSubset := realLe.subset with realZero.real, squareBLe268  apply realLe.of_subset with realZero.real269  exact realAddValue.nonnegative with squareASubset, squareBSubset270271-- A sum of two nonnegative reals can vanish only term by term.272theorem realAddValue.nonnegative_eq_zero (A B : Real)273  requires nonnegativeA : 0 ≤ A274  requires nonnegativeB : 0 ≤ B275  requires zeroSum : A + B = 0276  shows A = 0277proof278  have upper := realLe.add_left at realZero, B, A with279    realZero.real, *{2}, nonnegativeB280  have identity := realAddValue.zero_right at A281  rw [identity, zeroSum] at upper282  have down := realLe.subset at A, realZero with realZero.real, upper283  have up := realLe.subset with realZero.real, nonnegativeA284  exact Subset.antisymmetric with down, up285286theorem realLe.of_nonnegative_difference (A B : Real)287  requires nonnegative : 0 ≤ B - A288  shows A ≤ B289proof290  have shifted := realLe.add_right at realZero, B - A, A with *291  have left : (0:R) + A = A292  . ring293  have right : (B - A) + A = B294  . ring295  rwa [left, right] at shifted296297theorem realLe.mul_right_cancel_positive (A B C : Real)298  requires positive : 0 < C299  requires multiplied : A * C ≤ B * C300  shows A ≤ B301proof302  by_contra contrary303  have reversed := realLess.of_not_le with *304  have strict := realLess.mul_right_of_positive at B, A, C with *305  have ac := realMulValue.real at A, C with *306  have cycle := realLe.transitive_less with *307  have irreflexive := realLess.irreflexive_on308  have member : A * C ∈ ℝ309  . settle with Real310  exact irreflexive with A * C, cycle311312-- A quotient by a positive real is below C once the numerator is below C313-- times the denominator.314theorem realDiv.lt_of_lt_mul (A B C : Real)315  requires positive : 0 < B316  requires below : A < C * B317  shows A / B < C318proof319  have nonzero : B ≠ 0320    intro zero321    linarith322  have nonnegative : (0:R) ≤ B by linarith323  have quotientReal := realDiv.real at A, B with *324  have product := realDiv.mul_right at A, B with nonzero325  by_contra326  have above := realLe.of_not_less at C, A / B with this327  have scaled :=328    realLe.mul_right_of_nonnegative at C, A / B, B with above, nonnegative329  rw product at scaled330  linarith331