Grace/Cumulus/Real/PositiveMultiplication.g17

Open in Workbench Download source

Imports

Multiplication

Declarations

Source

1-- Positive multiplication lemmas for 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.PositiveMultiplication8import Multiplication910-- Two points of a lower cut have a common point strictly above both.  This is11-- the elementary directedness fact used whenever two open-cut witnesses must12-- be represented with a common factor.13theorem DedekindCut.exists_above_pair (A a b : Set)14  requires cut : DedekindCut(A)15  requires aInA : a ∈ A16  requires bInA : b ∈ A17  shows ∃ c ∈ A,18    relates(rationalLess, a, c) ∧ relates(rationalLess, b, c)19proof20  obtain ⟨u, uInA, aLessU⟩ := DedekindCut.no_greatest with cut, aInA21  by_contra noCommonUpper22  have subset := DedekindCut.subset_rationals with cut23  have uInQ := subset with u, uInA24  have bInQ := subset with b, bInA25  have aInQ := subset with a, aInA26  have aRational : Rational(a) by exact aInQ27  have uRational : Rational(u) by exact uInQ28  have distinct : u ≠ b29    intro equal30    obtain ⟨v, vInA, uLessV⟩ := DedekindCut.no_greatest with cut, uInA31    have vInQ := subset with v, vInA32    have vRational : Rational(v) by exact vInQ33    apply noCommonUpper34    refine ⟨v, vInA, _, _⟩35    . exact rationalLess.transitive at a, u, v with36        aRational, uRational, vRational, aLessU, uLessV37    . rw ← equal38      exact uLessV39  have connected := rationalLess.connected_on40  have comparison := connected with u, uInQ, b, bInQ, distinct41  cases comparison with uLessB | bLessU42  . obtain ⟨w, wInA, bLessW⟩ :=43      DedekindCut.no_greatest with cut, bInA44    have wInQ := subset with w, wInA45    have uLessW := rationalLess.transitive with uLessB, bLessW46    apply noCommonUpper47    refine ⟨w, wInA, _, bLessW⟩48    exact rationalLess.transitive with aLessU, uLessW49  . apply noCommonUpper50    refine ⟨u, uInA, aLessU, bLessU⟩5152-- In a positive real cut, every chosen member can be replaced by a strictly53-- larger positive member.  Thus later product arguments may work entirely54-- with the familiar positive witnesses.55theorem RealLess.exists_positive_member_above (A : Real) (b : Rational)56  requires positive : 0 < A57  requires bInA : b ∈ A58  shows ∃ c ∈ A, b < c ∧ rationalZero < c59proof60  obtain ⟨a, aInA, positiveA⟩ := RealLess.exists_positive_member with positive61  have cutA := Real.characterization.forward with assumption62  obtain ⟨c, cInA, bLessC, aLessC⟩ := DedekindCut.exists_above_pair with cutA, bInA, aInA63  have subsetA := DedekindCut.subset_rationals with cutA64  have aRational : Rational(a)65    unfold Rational66    exact subsetA with a, aInA67  have cRational : Rational(c)68    unfold Rational69    exact subsetA with c, cInA70  refine ⟨c, cInA, bLessC, _⟩71  exact rationalLess.transitive with rationalZero.rational, aRational, cRational, positiveA, aLessC7273-- A member of the positive-cut product of two positive reals always admits74-- positive factor witnesses, including when membership originally75-- came from the product's negative lower tail.76theorem realPosMulCut.positive_factors (A B : Real) (q : Rational)77  requires positiveA : 0 < A78  requires positiveB : 0 < B79  requires qInProduct : q ∈ realPosMulCut(A, B)80  shows ∃ a ∈ ℚ, a ∈ A ∧ ∃ b ∈ ℚ, b ∈ B ∧81    rationalZero < a ∧ rationalZero < b ∧ q < a * b82proof83  obtain ⟨qInQ, rest⟩ := realPosMulCut.membership.forward with qInProduct84  cases rest with qNegative | product85  . obtain ⟨a, aInA, aPositive⟩ :=86      RealLess.exists_positive_member with positiveA87    obtain ⟨b, bInB, bPositive⟩ := RealLess.exists_positive_member with positiveB88    have cutA := Real.characterization.forward at A with assumption89    have cutB := Real.characterization.forward at B with assumption90    have subsetA := DedekindCut.subset_rationals with cutA91    have subsetB := DedekindCut.subset_rationals with cutB92    have aInQ := subsetA with a, aInA93    have bInQ := subsetB with b, bInB94    have aRational : Rational(a) by exact aInQ95    have bRational : Rational(b) by exact bInQ96    have productPositive := rationalLess.mul_positive with aRational, bRational, aPositive, bPositive97    have productRational := rationalMulValue.rational with aRational, bRational98    have qRational : Rational(q) by typecheck99    refine ⟨a, aInQ, aInA, b, bInQ, bInB,100      aPositive, bPositive, _⟩101    exact rationalLess.transitive with102      qRational, rationalZero.rational, productRational, qNegative, productPositive103  . rcases product with104      ⟨a2, a2InQ, a2InA, b2, b2InQ, b2InB,105        a2Positive, b2Positive, qBelow⟩106    refine ⟨a2, a2InQ, a2InA, b2, b2InQ, b2InB,107      a2Positive, b2Positive, qBelow⟩108109-- Monotonicity in the second summand, derived by commutativity so that the110-- public API supports the two-sided monotonicity argument.111theorem realAddCut.subset_right (A B C : Real)112  requires subset : A ⊆ B113  shows realAddCut(C, A) ⊆ realAddCut(C, B)114proof115  have left := realAddCut.subset_left at A, B, C with116    *{3}, subset117  have ca := realAddCut.commutative at C, A with *118  have cb := realAddCut.commutative at C, B with *119  rwa [ca, cb]120121theorem realAddCut.nonnegative (A B : Real)122  requires nonnegativeA : realZero ⊆ A123  requires nonnegativeB : realZero ⊆ B124  shows realZero ⊆ realAddCut(A, B)125proof126  have first := realAddCut.subset_left at realZero, A, realZero with127    realZero.real, assumption, realZero.real, nonnegativeA128  have second := realAddCut.subset_right at realZero, B, A with129    realZero.real, *{2}, nonnegativeB130  have zeroSum := realAddCut.zero_left with realZero.real131  rw zeroSum at first132  exact Subset.transitive with first, second133134theorem realAddValue.positive (A B : Real)135  requires positiveA : 0 < A136  requires positiveB : 0 < B137  shows 0 < A + B138proof139  have aboveB := realLess.add_right at realZero, A, B with140    realZero.real, *{2}, positiveA141  have zeroLeft := realAddValue.zero_left at B142  rw zeroLeft at aboveB143  have sumReal := realAddValue.real at A, B with *144  exact realLess.transitive at realZero, B, A + B with145    realZero.real, assumption, sumReal,146    positiveB, aboveB147148-- The positive product is monotone in each cut argument.  This proof149-- transports the displayed factor witness; no arithmetic search is involved.150theorem realPosMulCut.subset_left (A B C : Real)151  requires subset : A ⊆ B152  shows realPosMulCut(A, C) ⊆ realPosMulCut(B, C)153proof154  intros q qInProduct155  obtain ⟨qInQ, rest⟩ := realPosMulCut.membership.forward with qInProduct156  apply realPosMulCut.membership.backward157  refine ⟨qInQ, _⟩158  cases rest with negative | product159  . left160    exact negative161  . rcases product with162      ⟨a, aInQ, aInA, c, cInQ, cInC,163        positiveA, positiveC, qBelow⟩164    have aInB : a ∈ B by exact subset with a, aInA165    right166    refine ⟨a, aInQ, aInB, c, cInQ, cInC,167      positiveA, positiveC, qBelow⟩168169theorem realPosMulCut.subset_right (A B C : Real)170  requires subset : A ⊆ B171  shows realPosMulCut(C, A) ⊆ realPosMulCut(C, B)172proof173  have left := realPosMulCut.subset_left at A, B, C with174    *{3}, subset175  have ca := realPosMulCut.commutative at C, A with *176  have cb := realPosMulCut.commutative at C, B with *177  rwa [ca, cb]178179-- A nonnegative real is either zero or strictly positive.  This is the180-- linear-order dichotomy, stated in the subset language used by181-- Dedekind cuts.182theorem Real.nonnegative_cases (A : Real)183  requires nonnegative : realZero ⊆ A184  shows A = realZero ∨ 0 < A185proof186  by_contra neither187  have notZero : ¬(A = realZero)188    intro equal189    apply neither190    left191    exact equal192  have notPositive : ¬(0 < A)193    intro positive194    apply neither195    right196    exact positive197  apply notPositive198  apply realLess.characterization.backward199  unfold RealLess200  refine ⟨realZero.real, assumption, _⟩201  unfold ProperSubset202  refine ⟨nonnegative, _⟩203  intro equal204  apply notZero205  rw equal206  rfl207208-- One direction of distributivity for three positive cuts.  Starting from209-- q < a*x with x < b+c, we move b, c, and then a slightly inward.  The210-- resulting boundary products are members of A*B and A*C, while211-- rational distributivity supplies their sum.212theorem realPosMulCut.distrib_subset (A B C : Real)213  requires positiveA : 0 < A214  requires positiveB : 0 < B215  requires positiveC : 0 < C216  shows realPosMulCut(A, realAddCut(B, C)) ⊆217    realAddCut(realPosMulCut(A, B), realPosMulCut(A, C))218proof219  intros q qInLeft220  have qData := realPosMulCut.membership.forward with qInLeft221  rcases qData with ⟨qInQ, qRest⟩222  have qRational : Rational(q) by exact qInQ223  have sumReal := realAddCut.real at B, C with *224  have sumPositiveValue := realAddValue.positive with *{2}, positiveB, positiveC225  have sumCut := realAddValue.cut at B, C with *226  have sumPositive : realZero < realAddCut(B, C)227    rwa ← sumCut228  obtain ⟨a, aInQ, aInA, x, xInQ, xInSum,229      positiveRA, positiveX, qBelowAX⟩ :=230    realPosMulCut.positive_factors at A, realAddCut(B, C), q with231      assumption, sumReal, qRational,232      positiveA, sumPositive, qInLeft233  have aRational : Rational(a) by exact aInQ234  have xRational : Rational(x) by exact xInQ235  obtain ⟨xAgain, b, bInB, c, cInC, xBelowSum⟩ := realAddCut.membership_value.forward with xInSum236  rw ← rationalAddValue.notation at xBelowSum237  have cutB := Real.characterization.forward at B with assumption238  have cutC := Real.characterization.forward at C with assumption239  have subsetB := DedekindCut.subset_rationals with cutB240  have subsetC := DedekindCut.subset_rationals with cutC241  have bInQ := subsetB with b, bInB242  have cInQ := subsetC with c, cInC243  have bRational : Rational(b) by exact bInQ244  have cRational : Rational(c) by exact cInQ245  obtain ⟨b2, b2InB, bLessB2, positiveB2⟩ := RealLess.exists_positive_member_above with246    assumption, bRational, positiveB, bInB247  obtain ⟨c2, c2InC, cLessC2, positiveC2⟩ := RealLess.exists_positive_member_above with248    assumption, cRational, positiveC, cInC249  have b2InQ := subsetB with b2, b2InB250  have c2InQ := subsetC with c2, c2InC251  have b2Rational : Rational(b2) by exact b2InQ252  have c2Rational : Rational(c2) by exact c2InQ253  have firstGrowth := rationalLess.add_right with bRational, b2Rational, cRational, bLessB2254  have secondGrowth := rationalLess.add_left with cRational, c2Rational, b2Rational, cLessC2255  have enlargedSumRational := rationalAddValue.rational with b2Rational, c2Rational256  have xBelowEnlarged : x < b2 + c2257    calc258      x < b + c := xBelowSum259      _ < b2 + c := firstGrowth260      _ < b2 + c2 := secondGrowth261  have scaled := rationalLess.mul_left with262    xRational, enlargedSumRational, aRational, positiveRA, xBelowEnlarged263  have axRational := rationalMulValue.rational with aRational, xRational264  have enlargedProductRational := rationalMulValue.rational with aRational, enlargedSumRational265  have qBelowExpanded : q < a * (b2 + c2)266    exact rationalLess.transitive with qRational, axRational, enlargedProductRational, qBelowAX, scaled267  have distributed := rationalMulValue.distributive_left with aRational, b2Rational, c2Rational268  have qBelowProducts : q < a * b2 + a * c2269    rwa ← distributed270  obtain ⟨a2, a2InA, aLessA2, positiveA2⟩ := RealLess.exists_positive_member_above with271    assumption, aRational, positiveA, aInA272  have cutA := Real.characterization.forward at A with assumption273  have subsetA := DedekindCut.subset_rationals with cutA274  have a2InQ := subsetA with a2, a2InA275  have a2Rational : Rational(a2) by exact a2InQ276  have leftBoundary := rationalLess.mul_right with aRational, a2Rational, b2Rational, positiveB2, aLessA2277  have rightBoundary := rationalLess.mul_right with aRational, a2Rational, c2Rational, positiveC2, aLessA2278  have leftRational := rationalMulValue.rational with aRational, b2Rational279  have rightRational := rationalMulValue.rational with aRational, c2Rational280  have leftInProduct : a * b2 ∈ realPosMulCut(A, B)281    apply realPosMulCut.membership.backward282    refine ⟨leftRational, _⟩283    right284    refine ⟨a2, a2InQ, a2InA, b2, b2InQ, b2InB,285      positiveA2, positiveB2, leftBoundary⟩286  have rightInProduct : a * c2 ∈ realPosMulCut(A, C)287    apply realPosMulCut.membership.backward288    refine ⟨rightRational, _⟩289    right290    refine ⟨a2, a2InQ, a2InA, c2, c2InQ, c2InC,291      positiveA2, positiveC2, rightBoundary⟩292  rw rationalAddValue.notation at qBelowProducts293  apply realAddCut.membership_value.backward294  refine ⟨qInQ, a * b2, leftInProduct,295    a * c2, rightInProduct, qBelowProducts⟩296297-- The reverse inclusion uses a common factor from A above the two displayed298-- product witnesses.  Rounding b and c upward makes b+c a member of299-- the sum cut, after which rational distributivity closes the estimate.300theorem realPosMulCut.distrib_reverse_subset (A B C : Real)301  requires positiveA : 0 < A302  requires positiveB : 0 < B303  requires positiveC : 0 < C304  shows realAddCut(realPosMulCut(A, B), realPosMulCut(A, C)) ⊆305    realPosMulCut(A, realAddCut(B, C))306proof307  intros q qInRight308  obtain ⟨qInQ, x, xInAB, y, yInAC, qBelowXY⟩ := realAddCut.membership_value.forward with qInRight309  rw ← rationalAddValue.notation at qBelowXY310  have subsetAB := realPosMulCut.subset_rationals at A, B311  have subsetAC := realPosMulCut.subset_rationals at A, C312  have xInQ := subsetAB with x, xInAB313  have yInQ := subsetAC with y, yInAC314  have xRational : Rational(x) by exact xInQ315  have yRational : Rational(y) by exact yInQ316  obtain ⟨a, aInQ, aInA, b, bInQ, bInB, positiveRA, positiveBFactor, xBelowAB⟩ := realPosMulCut.positive_factors with317    *{2}, xRational, positiveA, positiveB, xInAB318  obtain ⟨c, cInQ, cInA, d, dInQ, dInC, positiveRC, positiveDFactor, yBelowCD⟩ := realPosMulCut.positive_factors with319    *{2}, yRational, positiveA, positiveC, yInAC320  have aRational : Rational(a) by exact aInQ321  have bRational : Rational(b) by exact bInQ322  have cRational : Rational(c) by exact cInQ323  have dRational : Rational(d) by exact dInQ324  have cutA := Real.characterization.forward at A with assumption325  obtain ⟨e, eInA, aLessE, cLessE⟩ := DedekindCut.exists_above_pair with cutA, aInA, cInA326  have subsetA := DedekindCut.subset_rationals with cutA327  have eInQ := subsetA with e, eInA328  have eRational : Rational(e) by exact eInQ329  have positiveE := rationalLess.transitive with330    rationalZero.rational, aRational, eRational, positiveRA, aLessE331  have abRational := rationalMulValue.rational with aRational, bRational332  have cdRational := rationalMulValue.rational with cRational, dRational333  have ebRational := rationalMulValue.rational with eRational, bRational334  have edRational := rationalMulValue.rational with eRational, dRational335  have xGrowth := rationalLess.add_right with xRational, abRational, yRational, xBelowAB336  have yGrowth := rationalLess.add_left with yRational, cdRational, abRational, yBelowCD337  have abGrowth := rationalLess.mul_right with positiveBFactor, aLessE338  have cdGrowth := rationalLess.mul_right with positiveDFactor, cLessE339  have firstProductGrowth := rationalLess.add_right with abRational, ebRational, cdRational, abGrowth340  have secondProductGrowth := rationalLess.add_left with cdRational, edRational, ebRational, cdGrowth341  have qBelowCommonSum : q < e * b + e * d342    calc343      q < x + y := qBelowXY344      _ < a * b + y := xGrowth345      _ < a * b + c * d := yGrowth346      _ < e * b + c * d := firstProductGrowth347      _ < e * b + e * d := secondProductGrowth348  have distributed := rationalMulValue.distributive_left with eRational, bRational, dRational349  have qBelowFactored : q < e * (b + d) by rwa distributed350  have cutB := Real.characterization.forward at B with assumption351  have cutC := Real.characterization.forward at C with assumption352  have subsetB := DedekindCut.subset_rationals with cutB353  have subsetC := DedekindCut.subset_rationals with cutC354  obtain ⟨b2, b2InB, bLessB2, positiveB2⟩ := RealLess.exists_positive_member_above with355    assumption, bRational, positiveB, bInB356  obtain ⟨d2, d2InC, dLessD2, positiveD2⟩ := RealLess.exists_positive_member_above with357    assumption, dRational, positiveC, dInC358  have b2InQ := subsetB with b2, b2InB359  have d2InQ := subsetC with d2, d2InC360  have b2Rational : Rational(b2) by exact b2InQ361  have d2Rational : Rational(d2) by exact d2InQ362  have bGrowth := rationalLess.add_right with bRational, b2Rational, dRational, bLessB2363  have dGrowth := rationalLess.add_left with dRational, d2Rational, b2Rational, dLessD2364  have sumBelowRounded : b + d < b2 + d2365    calc366      b + d < b2 + d := bGrowth367      _ < b2 + d2 := dGrowth368  have bdRational := rationalAddValue.rational with bRational, dRational369  have zeroPlusD := rationalAddValue.zero_left with dRational370  have dBelowSum := rationalLess.add_right with rationalZero.rational, bRational, dRational, positiveBFactor371  rw zeroPlusD at dBelowSum372  have positiveSum := rationalLess.transitive with373    rationalZero.rational, dRational, bdRational, positiveDFactor, dBelowSum374  have sumInCut : b + d ∈ realAddCut(B, C)375    apply realAddCut.membership_value.backward376    refine ⟨bdRational, b2, b2InB, d2, d2InC, _⟩377    rwa ← rationalAddValue.notation378  apply realPosMulCut.membership.backward379  refine ⟨qInQ, _⟩380  right381  refine ⟨e, eInQ, eInA, b + d, _, sumInCut,382    positiveE, positiveSum, qBelowFactored⟩383  exact bdRational384385theorem realPosMulCut.distributive_of_positive (A B C : Real)386  requires positiveA : 0 < A387  requires positiveB : 0 < B388  requires positiveC : 0 < C389  shows realPosMulCut(A, realAddCut(B, C)) =390    realAddCut(realPosMulCut(A, B), realPosMulCut(A, C))391proof392  apply Subset.antisymmetric393  . exact realPosMulCut.distrib_subset at A, B, C with394      *{3},395      positiveA, positiveB, positiveC396  . exact realPosMulCut.distrib_reverse_subset at A, B, C with397      *{3},398      positiveA, positiveB, positiveC399