Grace/Cumulus/FixedPoint/CubeFunctions.g17

Open in Workbench Download source

Imports

CubeContinuity

Declarations

Source

1-- Real-valued functions on the unit cube that are continuous in the sup2-- metric, and the operations that preserve continuity: constants,3-- coordinates, sums, negatives, products, absolute values, reciprocals of4-- functions at least one, and maxima5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.FixedPoint.CubeFunctions11import CubeContinuity1213predicate CubeFunction (g n : Set) := FunctionBetween(g, unitCube(n), ℝ)1415predicate CubeFunctionContinuousAt (g n x : Set) :=16  ∀ E ∈ ℝ, (0:R) < E → ∃ D ∈ ℝ, (0:R) < D ∧17    (∀ y ∈ unitCube(n), ((∀ i ∈ n, dist(y(i), x(i)) < D) → dist(g(y), g(x)) < E))1819predicate CubeFunctionContinuous (g n : Set) :=20  CubeFunction(g, n) ∧ ∀ x ∈ unitCube(n), CubeFunctionContinuousAt(g, n, x)2122theorem CubeFunction.function (g n : Set)23  requires function : CubeFunction(g, n)24  shows g : unitCube(n) → ℝ25proof26  exact function2728theorem CubeFunction.value (g n x : Set)29  requires function : CubeFunction(g, n)30  requires hx : x ∈ unitCube(n)31  shows g(x) ∈ ℝ32proof33  have between := CubeFunction.function with function34  exact FunctionBetween.apply_closed with between, hx3536theorem CubeFunctionContinuous.function (g n : Set)37  requires continuous : CubeFunctionContinuous(g, n)38  shows CubeFunction(g, n)39proof40  exact continuous.left4142theorem CubeFunctionContinuous.at (g n x : Set)43  requires continuous : CubeFunctionContinuous(g, n)44  requires hx : x ∈ unitCube(n)45  shows CubeFunctionContinuousAt(g, n, x)46proof47  exact continuous.right with hx4849-- A smaller tolerance still works.50theorem CubeFunctionContinuousAt.shrink (g n x : Set) (E D C : Real)51  requires hx : x ∈ unitCube(n)52  requires close : ∀ y ∈ unitCube(n), ((∀ i ∈ n, dist(y(i), x(i)) < D) → dist(g(y), g(x)) < E)53  requires below : C ≤ D54  shows ∀ y ∈ unitCube(n), ((∀ i ∈ n, dist(y(i), x(i)) < C) → dist(g(y), g(x)) < E)55proof56  intros y hy near57  apply close with hy58  intros i hi59  have step := near with hi60  have yReal := unitCube.coordinate_real with hy, hi61  have xReal := unitCube.coordinate_real with hx, hi62  linarith6364-- Two positive reals have a common positive lower bound.65theorem positive.below_both (E W : Real)66  requires positiveE : 0 < E67  requires positiveW : 0 < W68  shows ∃ H ∈ ℝ, (0:R) < H ∧ H < E ∧ H < W69proof70  have halfE := half.lt_self with positiveE71  have halfEPos := half.positive with positiveE72  have halfEReal := half.real at E73  have halfW := half.lt_self with positiveW74  have halfWPos := half.positive with positiveW75  have halfWReal := half.real at W76  have split := realLess.trichotomy at E, W77  cases split with below | rest78  . witness half(E)79    refine ⟨halfEReal, halfEPos, halfE, ?_⟩80    linarith81  . cases rest with same | above82    . witness half(E)83      refine ⟨halfEReal, halfEPos, halfE, ?_⟩84      rwa ← same85    . witness half(W)86      refine ⟨halfWReal, halfWPos, ?_, halfW⟩87      linarith8889-- Two tolerances have a common positive lower bound.90theorem CubeFunctionContinuousAt.common (g h n x : Set) (E : Real)91  requires hx : x ∈ unitCube(n)92  requires gAt : CubeFunctionContinuousAt(g, n, x)93  requires hAt : CubeFunctionContinuousAt(h, n, x)94  requires positive : 0 < E95  shows ∃ D ∈ ℝ, (0:R) < D ∧ (∀ y ∈ unitCube(n), ((∀ i ∈ n, dist(y(i), x(i)) < D) → (dist(g(y), g(x)) < E ∧ dist(h(y), h(x)) < E)))96proof97  have EReal : E ∈ ℝ by typecheck98  obtain ⟨D1, D1Real, D1Pos, gClose⟩ := gAt with EReal, positive99  obtain ⟨D2, D2Real, D2Pos, hClose⟩ := hAt with EReal, positive100  obtain ⟨D, DReal, DPos, DBelow1, DBelow2⟩ := positive.below_both with D1Pos, D2Pos101  have gShrunk := CubeFunctionContinuousAt.shrink with hx, gClose, (realLess.implies_le with DBelow1)102  have hShrunk := CubeFunctionContinuousAt.shrink with hx, hClose, (realLess.implies_le with DBelow2)103  witness D104  constructor105  . exact DReal106  . constructor107    . exact DPos108    . intros y hy near109      constructor110      . exact gShrunk with hy, near111      . exact hShrunk with hy, near112113-- Constants and coordinates.114theorem constantCube.continuous (n : Nat) (c : Set)115  requires cReal : c ∈ ℝ116  shows CubeFunctionContinuous(constantFunction(unitCube(n), ℝ, c), n)117proof118  have function := constantFunction.function at unitCube(n), ℝ, c with cReal119  constructor120  . exact function121  . intros x hx E EReal Epos122    witness E123    constructor124    . exact EReal125    . constructor126      . exact Epos127      . intros y hy near128        have yValue := constantFunction.apply with hy, cReal129        have xValue := constantFunction.apply with hx, cReal130        rw [yValue, xValue]131        have self := dist.self at c132        rwa self133134defgraph coordinateCube (n i : Set) (x ∈ unitCube(n)) : ℝ := x(i)135requires hi : i ∈ n136proof137  exact unitCube.coordinate_real with member, hi138139theorem coordinateCube.continuous (n : Nat) (i : Set)140  requires hi : i ∈ n141  shows CubeFunctionContinuous(coordinateCube(n, i), n)142proof143  have function := coordinateCube.function with hi144  constructor145  . exact function146  . intros x hx E EReal Epos147    witness E148    constructor149    . exact EReal150    . constructor151      . exact Epos152      . intros y hy near153        have yValue := coordinateCube.value with hi, hy154        have xValue := coordinateCube.value with hi, hx155        rw [yValue, xValue]156        exact near with hi157158-- Sums, negatives, and products of cube functions.159defgraph addCube (n g h : Set) (x ∈ unitCube(n)) : ℝ := (g(x):R) + (h(x):R)160requires gFunction : CubeFunction(g, n)161requires hFunction : CubeFunction(h, n)162proof163  have gValue := CubeFunction.value with gFunction, member164  have hValue := CubeFunction.value with hFunction, member165  exact realAddValue.real at g(x), h(x)166167defgraph negCube (n g : Set) (x ∈ unitCube(n)) : ℝ := -(g(x):R)168requires gFunction : CubeFunction(g, n)169proof170  have gValue := CubeFunction.value with gFunction, member171  have neg : Real(-(g(x):R)) by typecheck172  exact neg173174defgraph mulCube (n g h : Set) (x ∈ unitCube(n)) : ℝ := (g(x):R) * (h(x):R)175requires gFunction : CubeFunction(g, n)176requires hFunction : CubeFunction(h, n)177proof178  have gValue := CubeFunction.value with gFunction, member179  have hValue := CubeFunction.value with hFunction, member180  exact realMulValue.real at g(x), h(x)181182theorem addCube.continuous (n : Nat) (g h : Set)183  requires gContinuous : CubeFunctionContinuous(g, n)184  requires hContinuous : CubeFunctionContinuous(h, n)185  shows CubeFunctionContinuous(addCube(n, g, h), n)186proof187  have gFunction := CubeFunctionContinuous.function with gContinuous188  have hFunction := CubeFunctionContinuous.function with hContinuous189  have function := addCube.function with gFunction, hFunction190  constructor191  . exact function192  . intros x hx E EReal Epos193    have halfPos := half.positive with Epos194    have gAt := CubeFunctionContinuous.at with gContinuous, hx195    have hAt := CubeFunctionContinuous.at with hContinuous, hx196    obtain ⟨D, DReal, DPos, close⟩ := CubeFunctionContinuousAt.common with hx, gAt, hAt, halfPos197    witness D198    constructor199    . exact DReal200    . constructor201      . exact DPos202      . intros y hy near203        obtain ⟨gNear, hNear⟩ := close with hy, near204        have yValue := addCube.value with gFunction, hFunction, hy205        have xValue := addCube.value with gFunction, hFunction, hx206        rw [yValue, xValue]207        have gy := CubeFunction.value with gFunction, hy208        have gx := CubeFunction.value with gFunction, hx209        have hy2 := CubeFunction.value with hFunction, hy210        have hx2 := CubeFunction.value with hFunction, hx211        have bound := dist.add_add at g(y), h(y), g(x), h(x)212        have halves := half.add_self at E213        linarith214215theorem negCube.continuous (n : Nat) (g : Set)216  requires gContinuous : CubeFunctionContinuous(g, n)217  shows CubeFunctionContinuous(negCube(n, g), n)218proof219  have gFunction := CubeFunctionContinuous.function with gContinuous220  have function := negCube.function with gFunction221  constructor222  . exact function223  . intros x hx E EReal Epos224    have gAt := CubeFunctionContinuous.at with gContinuous, hx225    obtain ⟨D, DReal, DPos, close⟩ := gAt with EReal, Epos226    witness D227    constructor228    . exact DReal229    . constructor230      . exact DPos231      . intros y hy near232        have gNear := close with hy, near233        have yValue := negCube.value with gFunction, hy234        have xValue := negCube.value with gFunction, hx235        rw [yValue, xValue]236        have gy := CubeFunction.value with gFunction, hy237        have gx := CubeFunction.value with gFunction, hx238        have same := dist.neg at g(y), g(x)239        rwa same240241theorem mulCube.continuous (n : Nat) (g h : Set)242  requires gContinuous : CubeFunctionContinuous(g, n)243  requires hContinuous : CubeFunctionContinuous(h, n)244  shows CubeFunctionContinuous(mulCube(n, g, h), n)245proof246  have gFunction := CubeFunctionContinuous.function with gContinuous247  have hFunction := CubeFunctionContinuous.function with hContinuous248  have function := mulCube.function with gFunction, hFunction249  constructor250  . exact function251  . intros x hx E EReal Epos252    have gx := CubeFunction.value with gFunction, hx253    have hx2 := CubeFunction.value with hFunction, hx254    have gAbs := abs.nonnegative at g(x)255    have hAbs := abs.nonnegative at h(x)256    have gAbsReal := abs.real at g(x)257    have hAbsReal := abs.real at h(x)258    have gScale : (0:R) < abs(g(x)) + 1 by linarith259    have hScale : (0:R) < abs(h(x)) + 1 by linarith260    have gScaleReal : Real(abs(g(x)) + 1) by typecheck261    have hScaleReal : Real(abs(h(x)) + 1) by typecheck262    -- g moves by less than E / (2(|h(x)| + 1)) and h by less than E / (2(|g(x)| + 1)).263    have gRadiusPos := scaledRadius.positive with Epos, hScale264    have hRadiusPos := scaledRadius.positive with Epos, gScale265    have gRadiusReal := scaledRadius.real at E, abs(h(x)) + 1266    have hRadiusReal := scaledRadius.real at E, abs(g(x)) + 1267    have gCancel := scaledRadius.cancel at E, abs(h(x)) + 1 with hScale268    have hCancel := scaledRadius.cancel at E, abs(g(x)) + 1 with gScale269    have onePos : (0:R) < (1:R) by linarith270    obtain ⟨R1, R1Real, R1Pos, R1Below, R1One⟩ := positive.below_both with gRadiusPos, onePos271    have gAt := CubeFunctionContinuous.at with gContinuous, hx272    have hAt := CubeFunctionContinuous.at with hContinuous, hx273    obtain ⟨D1, D1Real, D1Pos, gClose⟩ := gAt with R1Real, R1Pos274    have hRadiusIn : scaledRadius(E, abs(g(x)) + 1) ∈ ℝ by typecheck275    obtain ⟨D2, D2Real, D2Pos, hClose⟩ := hAt with hRadiusIn, hRadiusPos276    obtain ⟨D, DReal, DPos, DBelow1, DBelow2⟩ := positive.below_both with D1Pos, D2Pos277    have gShrunk := CubeFunctionContinuousAt.shrink with hx, gClose, (realLess.implies_le with DBelow1)278    have hShrunk := CubeFunctionContinuousAt.shrink with hx, hClose, (realLess.implies_le with DBelow2)279    witness D280    constructor281    . exact DReal282    . constructor283      . exact DPos284      . intros y hy near285        have gNear := gShrunk with hy, near286        have hNear := hShrunk with hy, near287        have yValue := mulCube.value with gFunction, hFunction, hy288        have xValue := mulCube.value with gFunction, hFunction, hx289        rw [yValue, xValue]290        have gy := CubeFunction.value with gFunction, hy291        have hy2 := CubeFunction.value with hFunction, hy292        have bound := dist.mul_mul at g(y), h(y), g(x), h(x)293        have gyAbs := abs.le_dist_add_abs at g(y), g(x)294        have gyAbsNonneg := abs.nonnegative at g(y)295        have d1Nonneg := dist.nonnegative at g(y), g(x)296        have d2Nonneg := dist.nonnegative at h(y), h(x)297        -- |g(y)| ≤ |g(x)| + 1, so |g(y)| · dist(h(y), h(x)) ≤ (|g(x)| + 1) · dist(h(y), h(x)) < half(E).298        have gyBound : abs(g(y)) ≤ abs(g(x)) + 1 by linarith299        have first := realLe.mul_right_of_nonnegative with gyBound, d2Nonneg300        have hRadiusLe := realLess.implies_le with hNear301        have second := realLe.mul_left_of_nonnegative with hRadiusLe, (realLess.implies_le with gScale)302        rw hCancel at second303        -- |h(x)| · dist(g(y), g(x)) ≤ (|h(x)| + 1) · dist(g(y), g(x)) < half(E).304        have hxBound : abs(h(x)) ≤ abs(h(x)) + 1 by linarith305        have third := realLe.mul_right_of_nonnegative with hxBound, d1Nonneg306        have gRadiusLe : dist(g(y), g(x)) ≤ scaledRadius(E, abs(h(x)) + 1) by linarith307        have fourth := realLe.mul_left_of_nonnegative with gRadiusLe, (realLess.implies_le with hScale)308        rw gCancel at fourth309        have halves := half.add_self at E310        have strict1 : (abs(g(x)) + 1) * dist(h(y), h(x)) < half(E)311          have step := realLess.mul_left_of_positive with hNear, gScale312          rwa hCancel at step313        have strict2 : (abs(h(x)) + 1) * dist(g(y), g(x)) < half(E)314          have gStrict : dist(g(y), g(x)) < scaledRadius(E, abs(h(x)) + 1) by linarith315          have step := realLess.mul_left_of_positive with gStrict, hScale316          rwa gCancel at step317        linarith318319-- The absolute value does not increase distances.320theorem abs.le_of_bounds (A M : Real)321  requires upper : A ≤ M322  requires lower : -A ≤ M323  shows abs(A) ≤ M324proof325  have split := realLess.trichotomy at (0:R), A326  cases split with positive | rest327  . have value := abs.of_nonnegative with (realLess.implies_le with positive)328    rwa value329  . cases rest with zero | negative330    . have nonneg : (0:R) ≤ A by linarith331      have value := abs.of_nonnegative with nonneg332      rwa value333    . have value := abs.of_nonpositive with (realLess.implies_le with negative)334      rwa value335336theorem dist.abs_le (A B : Real)337  shows dist(abs(A), abs(B)) ≤ dist(A, B)338proof339  have first := abs.le_dist_add_abs at A, B340  have second := abs.le_dist_add_abs at B, A341  have symmetric := dist.symmetric at B, A342  rw symmetric at second343  have same : dist(abs(A), abs(B)) = abs(abs(A) - abs(B))344    unfold dist345    rfl346  rw same347  apply abs.le_of_bounds348  . linarith349  . linarith350351defgraph absCube (n g : Set) (x ∈ unitCube(n)) : ℝ := abs((g(x):R))352requires gFunction : CubeFunction(g, n)353proof354  have gValue := CubeFunction.value with gFunction, member355  exact abs.real at g(x)356357theorem absCube.continuous (n : Nat) (g : Set)358  requires gContinuous : CubeFunctionContinuous(g, n)359  shows CubeFunctionContinuous(absCube(n, g), n)360proof361  have gFunction := CubeFunctionContinuous.function with gContinuous362  have function := absCube.function with gFunction363  constructor364  . exact function365  . intros x hx E EReal Epos366    have gAt := CubeFunctionContinuous.at with gContinuous, hx367    obtain ⟨D, DReal, DPos, close⟩ := gAt with EReal, Epos368    witness D369    constructor370    . exact DReal371    . constructor372      . exact DPos373      . intros y hy near374        have gNear := close with hy, near375        have yValue := absCube.value with gFunction, hy376        have xValue := absCube.value with gFunction, hx377        rw [yValue, xValue]378        have gy := CubeFunction.value with gFunction, hy379        have gx := CubeFunction.value with gFunction, hx380        have bound := dist.abs_le at g(y), g(x)381        linarith382383-- Reciprocals of functions that stay at least one.384theorem realInvValue.le_one (A : Real)385  requires atLeastOne : (1:R) ≤ A386  shows (0:R) < realInvValue(A) ∧ realInvValue(A) ≤ (1:R)387proof388  have positive : (0:R) < A by linarith389  have nonzero : A ≠ (0:R)390    intro zero391    rw zero at positive392    linarith393  have cut := realInvValue.of_positive with positive394  have cutPositive := positiveRealInvCut.positive with positive395  have invPositive : (0:R) < realInvValue(A) by rwa cut396  have cancel := realInvValue.mul_right with nonzero397  have step := realLe.mul_left_of_nonnegative with atLeastOne, (realLess.implies_le with invPositive)398  have one := realMulValue.one_right at realInvValue(A)399  have commute := realMulValue.commutative at realInvValue(A), A400  rw [one, commute, cancel] at step401  exact ⟨invPositive, step⟩402403defgraph invCube (n g : Set) (x ∈ unitCube(n)) : ℝ := realInvValue((g(x):R))404requires gFunction : CubeFunction(g, n)405proof406  have gValue := CubeFunction.value with gFunction, member407  exact realInvValue.real at g(x)408409theorem invCube.continuous (n : Nat) (g : Set)410  requires gContinuous : CubeFunctionContinuous(g, n)411  requires atLeastOne : ∀ x ∈ unitCube(n), (1:R) ≤ (g(x):R)412  shows CubeFunctionContinuous(invCube(n, g), n)413proof414  have gFunction := CubeFunctionContinuous.function with gContinuous415  have function := invCube.function with gFunction416  constructor417  . exact function418  . intros x hx E EReal Epos419    have gAt := CubeFunctionContinuous.at with gContinuous, hx420    obtain ⟨D, DReal, DPos, close⟩ := gAt with EReal, Epos421    witness D422    constructor423    . exact DReal424    . constructor425      . exact DPos426      . intros y hy near427        have gNear := close with hy, near428        have yValue := invCube.value with gFunction, hy429        have xValue := invCube.value with gFunction, hx430        rw [yValue, xValue]431        have gy := CubeFunction.value with gFunction, hy432        have gx := CubeFunction.value with gFunction, hx433        obtain ⟨yPos, yLe⟩ := realInvValue.le_one with (atLeastOne with hy)434        obtain ⟨xPos, xLe⟩ := realInvValue.le_one with (atLeastOne with hx)435        have yNonzero : (g(y):R) ≠ (0:R)436          intro zero437          have bound := atLeastOne with hy438          rw zero at bound439          linarith440        have xNonzero : (g(x):R) ≠ (0:R)441          intro zero442          have bound := atLeastOne with hx443          rw zero at bound444          linarith445        have formula := dist.inv_inv with yNonzero, xNonzero446        have yAbs := abs.of_nonnegative with (realLess.implies_le with yPos)447        have xAbs := abs.of_nonnegative with (realLess.implies_le with xPos)448        rw [yAbs, xAbs] at formula449        have dNonneg := dist.nonnegative at g(y), g(x)450        have productLe : realInvValue(g(y)) * realInvValue(g(x)) ≤ (1:R)451          have step := realLe.mul_left_of_nonnegative with xLe, (realLess.implies_le with yPos)452          have one := realMulValue.one_right at realInvValue(g(y))453          rw one at step454          linarith455        have productNonneg : (0:R) ≤ realInvValue(g(y)) * realInvValue(g(x))456          have step := realLe.mul_left_of_nonnegative with (realLess.implies_le with xPos), (realLess.implies_le with yPos)457          have zero := realMulValue.zero_right at realInvValue(g(y))458          rwa zero at step459        have scaled := realLe.mul_left_of_nonnegative with productLe, dNonneg460        have one := realMulValue.one_right at dist(g(y), g(x))461        rw one at scaled462        rw formula463        linarith464465-- The larger of two reals, written so that it is built from sums, absolute466-- values, and a constant factor.467def realMax (A B : Real) : Real := half(realOne) * (A + B + abs(A + -B))468469theorem realMax.real (A B : Real)470  shows Real(realMax(A, B))471proof472  have product : Real(half(realOne) * (A + B + abs(A + -B))) by typecheck473  unfold realMax474  exact product475476theorem realMax.of_le (A B : Real)477  requires below : B ≤ A478  shows realMax(A, B) = A479proof480  have nonneg : (0:R) ≤ A + -B by linarith481  have value := abs.of_nonnegative with nonneg482  have halves := half.add_self at realOne483  have same : realMax(A, B) = half(realOne) * (A + B + abs(A + -B))484    unfold realMax485    rfl486  rw [same, value]487  have twoA : A + B + (A + -B) = A + A by ring488  have expand : half(realOne) * (A + A) = (half(realOne) + half(realOne)) * A by ring489  rw [twoA, expand, halves]490  exact realMulValue.one_left491492theorem realMax.of_ge (A B : Real)493  requires below : A ≤ B494  shows realMax(A, B) = B495proof496  have nonpos : A + -B ≤ (0:R) by linarith497  have value := abs.of_nonpositive with nonpos498  have halves := half.add_self at realOne499  have same : realMax(A, B) = half(realOne) * (A + B + abs(A + -B))500    unfold realMax501    rfl502  rw [same, value]503  have twoB : A + B + -(A + -B) = B + B by ring504  have expand : half(realOne) * (B + B) = (half(realOne) + half(realOne)) * B by ring505  rw [twoB, expand, halves]506  exact realMulValue.one_left507508theorem realMax.ge_left (A B : Real)509  shows A ≤ realMax(A, B)510proof511  have split := realLess.trichotomy at A, B512  cases split with less | rest513  . have value := realMax.of_ge with (realLess.implies_le with less)514    rw value515    linarith516  . cases rest with same | greater517    . have le : A ≤ B by linarith518      have value := realMax.of_ge with le519      rw value520      linarith521    . have value := realMax.of_le with (realLess.implies_le with greater)522      rw value523      linarith524525theorem realMax.ge_right (A B : Real)526  shows B ≤ realMax(A, B)527proof528  have split := realLess.trichotomy at A, B529  cases split with less | rest530  . have value := realMax.of_ge with (realLess.implies_le with less)531    rw value532    linarith533  . cases rest with same | greater534    . have le : A ≤ B by linarith535      have value := realMax.of_ge with le536      rw value537      linarith538    . have value := realMax.of_le with (realLess.implies_le with greater)539      rw value540      linarith541542def maxCube (n g h : Set) : Set :=543  mulCube(n, constantFunction(unitCube(n), ℝ, half(realOne)), addCube(n, addCube(n, g, h), absCube(n, addCube(n, g, negCube(n, h)))))544545theorem maxCube.value (n : Nat) (g h x : Set)546  requires gFunction : CubeFunction(g, n)547  requires hFunction : CubeFunction(h, n)548  requires hx : x ∈ unitCube(n)549  shows maxCube(n, g, h)(x) = realMax((g(x):R), (h(x):R))550proof551  have gx := CubeFunction.value with gFunction, hx552  have hx2 := CubeFunction.value with hFunction, hx553  have hReal := half.real at realOne554  have hIn : half(realOne) ∈ ℝ by typecheck555  have negFunction : CubeFunction(negCube(n, h), n) := negCube.function with hFunction556  have diffFunction : CubeFunction(addCube(n, g, negCube(n, h)), n) := addCube.function with557    gFunction, negFunction558  have absFunction : CubeFunction(absCube(n, addCube(n, g, negCube(n, h))), n) := absCube.function with559    diffFunction560  have sumFunction : CubeFunction(addCube(n, g, h), n) := addCube.function with gFunction, hFunction561  have totalFunction : CubeFunction(addCube(n, addCube(n, g, h), absCube(n, addCube(n, g, negCube(n, h)))), n) := addCube.function with562    sumFunction, absFunction563  have constantFunction2 : CubeFunction(constantFunction(unitCube(n), ℝ, half(realOne)), n) := constantFunction.function at unitCube(n), ℝ, half(1) with hIn564  have same : maxCube(n, g, h)(x) = mulCube(n, constantFunction(unitCube(n), ℝ, half(realOne)), addCube(n, addCube(n, g, h), absCube(n, addCube(n, g, negCube(n, h)))))(x)565    unfold maxCube566    rfl567  rw same568  have v1 := mulCube.value with constantFunction2, totalFunction, hx569  have v2 := constantFunction.apply at unitCube(n), ℝ, x, half(realOne) with hx570  have v3 := addCube.value with sumFunction, absFunction, hx571  have v4 := addCube.value with gFunction, hFunction, hx572  have v5 := absCube.value with diffFunction, hx573  have v6 := addCube.value with gFunction, negFunction, hx574  have v7 := negCube.value with hFunction, hx575  rw [v1, v2, v3, v4, v5, v6, v7]576  unfold realMax577  rfl578579theorem maxCube.continuous (n : Nat) (g h : Set)580  requires gContinuous : CubeFunctionContinuous(g, n)581  requires hContinuous : CubeFunctionContinuous(h, n)582  shows CubeFunctionContinuous(maxCube(n, g, h), n)583proof584  have hIn : half(realOne) ∈ ℝ by typecheck585  have constant := constantCube.continuous with hIn586  have neg := negCube.continuous with hContinuous587  have diff := addCube.continuous with gContinuous, neg588  have absolute := absCube.continuous with diff589  have sum := addCube.continuous with gContinuous, hContinuous590  have total := addCube.continuous with sum, absolute591  have product := mulCube.continuous with constant, total592  unfold maxCube593  exact product594