-- Real-valued functions on the unit cube that are continuous in the sup
-- metric, and the operations that preserve continuity: constants,
-- coordinates, sums, negatives, products, absolute values, reciprocals of
-- functions at least one, and maxima
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.FixedPoint.CubeFunctions
import CubeContinuity

predicate CubeFunction (g n : Set) := FunctionBetween(g, unitCube(n), ℝ)

predicate CubeFunctionContinuousAt (g n x : Set) :=
  ∀ E ∈ ℝ, (0:R) < E → ∃ D ∈ ℝ, (0:R) < D ∧
    (∀ y ∈ unitCube(n), ((∀ i ∈ n, dist(y(i), x(i)) < D) → dist(g(y), g(x)) < E))

predicate CubeFunctionContinuous (g n : Set) :=
  CubeFunction(g, n) ∧ ∀ x ∈ unitCube(n), CubeFunctionContinuousAt(g, n, x)

theorem CubeFunction.function (g n : Set)
  requires function : CubeFunction(g, n)
  shows g : unitCube(n) → ℝ
proof
  exact function

theorem CubeFunction.value (g n x : Set)
  requires function : CubeFunction(g, n)
  requires hx : x ∈ unitCube(n)
  shows g(x) ∈ ℝ
proof
  have between := CubeFunction.function with function
  exact FunctionBetween.apply_closed with between, hx

theorem CubeFunctionContinuous.function (g n : Set)
  requires continuous : CubeFunctionContinuous(g, n)
  shows CubeFunction(g, n)
proof
  exact continuous.left

theorem CubeFunctionContinuous.at (g n x : Set)
  requires continuous : CubeFunctionContinuous(g, n)
  requires hx : x ∈ unitCube(n)
  shows CubeFunctionContinuousAt(g, n, x)
proof
  exact continuous.right with hx

-- A smaller tolerance still works.
theorem CubeFunctionContinuousAt.shrink (g n x : Set) (E D C : Real)
  requires hx : x ∈ unitCube(n)
  requires close : ∀ y ∈ unitCube(n), ((∀ i ∈ n, dist(y(i), x(i)) < D) → dist(g(y), g(x)) < E)
  requires below : C ≤ D
  shows ∀ y ∈ unitCube(n), ((∀ i ∈ n, dist(y(i), x(i)) < C) → dist(g(y), g(x)) < E)
proof
  intros y hy near
  apply close with hy
  intros i hi
  have step := near with hi
  have yReal := unitCube.coordinate_real with hy, hi
  have xReal := unitCube.coordinate_real with hx, hi
  linarith

-- Two positive reals have a common positive lower bound.
theorem positive.below_both (E W : Real)
  requires positiveE : 0 < E
  requires positiveW : 0 < W
  shows ∃ H ∈ ℝ, (0:R) < H ∧ H < E ∧ H < W
proof
  have halfE := half.lt_self with positiveE
  have halfEPos := half.positive with positiveE
  have halfEReal := half.real at E
  have halfW := half.lt_self with positiveW
  have halfWPos := half.positive with positiveW
  have halfWReal := half.real at W
  have split := realLess.trichotomy at E, W
  cases split with below | rest
  . witness half(E)
    refine ⟨halfEReal, halfEPos, halfE, ?_⟩
    linarith
  . cases rest with same | above
    . witness half(E)
      refine ⟨halfEReal, halfEPos, halfE, ?_⟩
      rwa ← same
    . witness half(W)
      refine ⟨halfWReal, halfWPos, ?_, halfW⟩
      linarith

-- Two tolerances have a common positive lower bound.
theorem CubeFunctionContinuousAt.common (g h n x : Set) (E : Real)
  requires hx : x ∈ unitCube(n)
  requires gAt : CubeFunctionContinuousAt(g, n, x)
  requires hAt : CubeFunctionContinuousAt(h, n, x)
  requires positive : 0 < E
  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)))
proof
  have EReal : E ∈ ℝ by typecheck
  obtain ⟨D1, D1Real, D1Pos, gClose⟩ := gAt with EReal, positive
  obtain ⟨D2, D2Real, D2Pos, hClose⟩ := hAt with EReal, positive
  obtain ⟨D, DReal, DPos, DBelow1, DBelow2⟩ := positive.below_both with D1Pos, D2Pos
  have gShrunk := CubeFunctionContinuousAt.shrink with hx, gClose, (realLess.implies_le with DBelow1)
  have hShrunk := CubeFunctionContinuousAt.shrink with hx, hClose, (realLess.implies_le with DBelow2)
  witness D
  constructor
  . exact DReal
  . constructor
    . exact DPos
    . intros y hy near
      constructor
      . exact gShrunk with hy, near
      . exact hShrunk with hy, near

-- Constants and coordinates.
theorem constantCube.continuous (n : Nat) (c : Set)
  requires cReal : c ∈ ℝ
  shows CubeFunctionContinuous(constantFunction(unitCube(n), ℝ, c), n)
proof
  have function := constantFunction.function at unitCube(n), ℝ, c with cReal
  constructor
  . exact function
  . intros x hx E EReal Epos
    witness E
    constructor
    . exact EReal
    . constructor
      . exact Epos
      . intros y hy near
        have yValue := constantFunction.apply with hy, cReal
        have xValue := constantFunction.apply with hx, cReal
        rw [yValue, xValue]
        have self := dist.self at c
        rwa self

defgraph coordinateCube (n i : Set) (x ∈ unitCube(n)) : ℝ := x(i)
requires hi : i ∈ n
proof
  exact unitCube.coordinate_real with member, hi

theorem coordinateCube.continuous (n : Nat) (i : Set)
  requires hi : i ∈ n
  shows CubeFunctionContinuous(coordinateCube(n, i), n)
proof
  have function := coordinateCube.function with hi
  constructor
  . exact function
  . intros x hx E EReal Epos
    witness E
    constructor
    . exact EReal
    . constructor
      . exact Epos
      . intros y hy near
        have yValue := coordinateCube.value with hi, hy
        have xValue := coordinateCube.value with hi, hx
        rw [yValue, xValue]
        exact near with hi

-- Sums, negatives, and products of cube functions.
defgraph addCube (n g h : Set) (x ∈ unitCube(n)) : ℝ := (g(x):R) + (h(x):R)
requires gFunction : CubeFunction(g, n)
requires hFunction : CubeFunction(h, n)
proof
  have gValue := CubeFunction.value with gFunction, member
  have hValue := CubeFunction.value with hFunction, member
  exact realAddValue.real at g(x), h(x)

defgraph negCube (n g : Set) (x ∈ unitCube(n)) : ℝ := -(g(x):R)
requires gFunction : CubeFunction(g, n)
proof
  have gValue := CubeFunction.value with gFunction, member
  have neg : Real(-(g(x):R)) by typecheck
  exact neg

defgraph mulCube (n g h : Set) (x ∈ unitCube(n)) : ℝ := (g(x):R) * (h(x):R)
requires gFunction : CubeFunction(g, n)
requires hFunction : CubeFunction(h, n)
proof
  have gValue := CubeFunction.value with gFunction, member
  have hValue := CubeFunction.value with hFunction, member
  exact realMulValue.real at g(x), h(x)

theorem addCube.continuous (n : Nat) (g h : Set)
  requires gContinuous : CubeFunctionContinuous(g, n)
  requires hContinuous : CubeFunctionContinuous(h, n)
  shows CubeFunctionContinuous(addCube(n, g, h), n)
proof
  have gFunction := CubeFunctionContinuous.function with gContinuous
  have hFunction := CubeFunctionContinuous.function with hContinuous
  have function := addCube.function with gFunction, hFunction
  constructor
  . exact function
  . intros x hx E EReal Epos
    have halfPos := half.positive with Epos
    have gAt := CubeFunctionContinuous.at with gContinuous, hx
    have hAt := CubeFunctionContinuous.at with hContinuous, hx
    obtain ⟨D, DReal, DPos, close⟩ := CubeFunctionContinuousAt.common with hx, gAt, hAt, halfPos
    witness D
    constructor
    . exact DReal
    . constructor
      . exact DPos
      . intros y hy near
        obtain ⟨gNear, hNear⟩ := close with hy, near
        have yValue := addCube.value with gFunction, hFunction, hy
        have xValue := addCube.value with gFunction, hFunction, hx
        rw [yValue, xValue]
        have gy := CubeFunction.value with gFunction, hy
        have gx := CubeFunction.value with gFunction, hx
        have hy2 := CubeFunction.value with hFunction, hy
        have hx2 := CubeFunction.value with hFunction, hx
        have bound := dist.add_add at g(y), h(y), g(x), h(x)
        have halves := half.add_self at E
        linarith

theorem negCube.continuous (n : Nat) (g : Set)
  requires gContinuous : CubeFunctionContinuous(g, n)
  shows CubeFunctionContinuous(negCube(n, g), n)
proof
  have gFunction := CubeFunctionContinuous.function with gContinuous
  have function := negCube.function with gFunction
  constructor
  . exact function
  . intros x hx E EReal Epos
    have gAt := CubeFunctionContinuous.at with gContinuous, hx
    obtain ⟨D, DReal, DPos, close⟩ := gAt with EReal, Epos
    witness D
    constructor
    . exact DReal
    . constructor
      . exact DPos
      . intros y hy near
        have gNear := close with hy, near
        have yValue := negCube.value with gFunction, hy
        have xValue := negCube.value with gFunction, hx
        rw [yValue, xValue]
        have gy := CubeFunction.value with gFunction, hy
        have gx := CubeFunction.value with gFunction, hx
        have same := dist.neg at g(y), g(x)
        rwa same

theorem mulCube.continuous (n : Nat) (g h : Set)
  requires gContinuous : CubeFunctionContinuous(g, n)
  requires hContinuous : CubeFunctionContinuous(h, n)
  shows CubeFunctionContinuous(mulCube(n, g, h), n)
proof
  have gFunction := CubeFunctionContinuous.function with gContinuous
  have hFunction := CubeFunctionContinuous.function with hContinuous
  have function := mulCube.function with gFunction, hFunction
  constructor
  . exact function
  . intros x hx E EReal Epos
    have gx := CubeFunction.value with gFunction, hx
    have hx2 := CubeFunction.value with hFunction, hx
    have gAbs := abs.nonnegative at g(x)
    have hAbs := abs.nonnegative at h(x)
    have gAbsReal := abs.real at g(x)
    have hAbsReal := abs.real at h(x)
    have gScale : (0:R) < abs(g(x)) + 1 by linarith
    have hScale : (0:R) < abs(h(x)) + 1 by linarith
    have gScaleReal : Real(abs(g(x)) + 1) by typecheck
    have hScaleReal : Real(abs(h(x)) + 1) by typecheck
    -- g moves by less than E / (2(|h(x)| + 1)) and h by less than E / (2(|g(x)| + 1)).
    have gRadiusPos := scaledRadius.positive with Epos, hScale
    have hRadiusPos := scaledRadius.positive with Epos, gScale
    have gRadiusReal := scaledRadius.real at E, abs(h(x)) + 1
    have hRadiusReal := scaledRadius.real at E, abs(g(x)) + 1
    have gCancel := scaledRadius.cancel at E, abs(h(x)) + 1 with hScale
    have hCancel := scaledRadius.cancel at E, abs(g(x)) + 1 with gScale
    have onePos : (0:R) < (1:R) by linarith
    obtain ⟨R1, R1Real, R1Pos, R1Below, R1One⟩ := positive.below_both with gRadiusPos, onePos
    have gAt := CubeFunctionContinuous.at with gContinuous, hx
    have hAt := CubeFunctionContinuous.at with hContinuous, hx
    obtain ⟨D1, D1Real, D1Pos, gClose⟩ := gAt with R1Real, R1Pos
    have hRadiusIn : scaledRadius(E, abs(g(x)) + 1) ∈ ℝ by typecheck
    obtain ⟨D2, D2Real, D2Pos, hClose⟩ := hAt with hRadiusIn, hRadiusPos
    obtain ⟨D, DReal, DPos, DBelow1, DBelow2⟩ := positive.below_both with D1Pos, D2Pos
    have gShrunk := CubeFunctionContinuousAt.shrink with hx, gClose, (realLess.implies_le with DBelow1)
    have hShrunk := CubeFunctionContinuousAt.shrink with hx, hClose, (realLess.implies_le with DBelow2)
    witness D
    constructor
    . exact DReal
    . constructor
      . exact DPos
      . intros y hy near
        have gNear := gShrunk with hy, near
        have hNear := hShrunk with hy, near
        have yValue := mulCube.value with gFunction, hFunction, hy
        have xValue := mulCube.value with gFunction, hFunction, hx
        rw [yValue, xValue]
        have gy := CubeFunction.value with gFunction, hy
        have hy2 := CubeFunction.value with hFunction, hy
        have bound := dist.mul_mul at g(y), h(y), g(x), h(x)
        have gyAbs := abs.le_dist_add_abs at g(y), g(x)
        have gyAbsNonneg := abs.nonnegative at g(y)
        have d1Nonneg := dist.nonnegative at g(y), g(x)
        have d2Nonneg := dist.nonnegative at h(y), h(x)
        -- |g(y)| ≤ |g(x)| + 1, so |g(y)| · dist(h(y), h(x)) ≤ (|g(x)| + 1) · dist(h(y), h(x)) < half(E).
        have gyBound : abs(g(y)) ≤ abs(g(x)) + 1 by linarith
        have first := realLe.mul_right_of_nonnegative with gyBound, d2Nonneg
        have hRadiusLe := realLess.implies_le with hNear
        have second := realLe.mul_left_of_nonnegative with hRadiusLe, (realLess.implies_le with gScale)
        rw hCancel at second
        -- |h(x)| · dist(g(y), g(x)) ≤ (|h(x)| + 1) · dist(g(y), g(x)) < half(E).
        have hxBound : abs(h(x)) ≤ abs(h(x)) + 1 by linarith
        have third := realLe.mul_right_of_nonnegative with hxBound, d1Nonneg
        have gRadiusLe : dist(g(y), g(x)) ≤ scaledRadius(E, abs(h(x)) + 1) by linarith
        have fourth := realLe.mul_left_of_nonnegative with gRadiusLe, (realLess.implies_le with hScale)
        rw gCancel at fourth
        have halves := half.add_self at E
        have strict1 : (abs(g(x)) + 1) * dist(h(y), h(x)) < half(E)
          have step := realLess.mul_left_of_positive with hNear, gScale
          rwa hCancel at step
        have strict2 : (abs(h(x)) + 1) * dist(g(y), g(x)) < half(E)
          have gStrict : dist(g(y), g(x)) < scaledRadius(E, abs(h(x)) + 1) by linarith
          have step := realLess.mul_left_of_positive with gStrict, hScale
          rwa gCancel at step
        linarith

-- The absolute value does not increase distances.
theorem abs.le_of_bounds (A M : Real)
  requires upper : A ≤ M
  requires lower : -A ≤ M
  shows abs(A) ≤ M
proof
  have split := realLess.trichotomy at (0:R), A
  cases split with positive | rest
  . have value := abs.of_nonnegative with (realLess.implies_le with positive)
    rwa value
  . cases rest with zero | negative
    . have nonneg : (0:R) ≤ A by linarith
      have value := abs.of_nonnegative with nonneg
      rwa value
    . have value := abs.of_nonpositive with (realLess.implies_le with negative)
      rwa value

theorem dist.abs_le (A B : Real)
  shows dist(abs(A), abs(B)) ≤ dist(A, B)
proof
  have first := abs.le_dist_add_abs at A, B
  have second := abs.le_dist_add_abs at B, A
  have symmetric := dist.symmetric at B, A
  rw symmetric at second
  have same : dist(abs(A), abs(B)) = abs(abs(A) - abs(B))
    unfold dist
    rfl
  rw same
  apply abs.le_of_bounds
  . linarith
  . linarith

defgraph absCube (n g : Set) (x ∈ unitCube(n)) : ℝ := abs((g(x):R))
requires gFunction : CubeFunction(g, n)
proof
  have gValue := CubeFunction.value with gFunction, member
  exact abs.real at g(x)

theorem absCube.continuous (n : Nat) (g : Set)
  requires gContinuous : CubeFunctionContinuous(g, n)
  shows CubeFunctionContinuous(absCube(n, g), n)
proof
  have gFunction := CubeFunctionContinuous.function with gContinuous
  have function := absCube.function with gFunction
  constructor
  . exact function
  . intros x hx E EReal Epos
    have gAt := CubeFunctionContinuous.at with gContinuous, hx
    obtain ⟨D, DReal, DPos, close⟩ := gAt with EReal, Epos
    witness D
    constructor
    . exact DReal
    . constructor
      . exact DPos
      . intros y hy near
        have gNear := close with hy, near
        have yValue := absCube.value with gFunction, hy
        have xValue := absCube.value with gFunction, hx
        rw [yValue, xValue]
        have gy := CubeFunction.value with gFunction, hy
        have gx := CubeFunction.value with gFunction, hx
        have bound := dist.abs_le at g(y), g(x)
        linarith

-- Reciprocals of functions that stay at least one.
theorem realInvValue.le_one (A : Real)
  requires atLeastOne : (1:R) ≤ A
  shows (0:R) < realInvValue(A) ∧ realInvValue(A) ≤ (1:R)
proof
  have positive : (0:R) < A by linarith
  have nonzero : A ≠ (0:R)
    intro zero
    rw zero at positive
    linarith
  have cut := realInvValue.of_positive with positive
  have cutPositive := positiveRealInvCut.positive with positive
  have invPositive : (0:R) < realInvValue(A) by rwa cut
  have cancel := realInvValue.mul_right with nonzero
  have step := realLe.mul_left_of_nonnegative with atLeastOne, (realLess.implies_le with invPositive)
  have one := realMulValue.one_right at realInvValue(A)
  have commute := realMulValue.commutative at realInvValue(A), A
  rw [one, commute, cancel] at step
  exact ⟨invPositive, step⟩

defgraph invCube (n g : Set) (x ∈ unitCube(n)) : ℝ := realInvValue((g(x):R))
requires gFunction : CubeFunction(g, n)
proof
  have gValue := CubeFunction.value with gFunction, member
  exact realInvValue.real at g(x)

theorem invCube.continuous (n : Nat) (g : Set)
  requires gContinuous : CubeFunctionContinuous(g, n)
  requires atLeastOne : ∀ x ∈ unitCube(n), (1:R) ≤ (g(x):R)
  shows CubeFunctionContinuous(invCube(n, g), n)
proof
  have gFunction := CubeFunctionContinuous.function with gContinuous
  have function := invCube.function with gFunction
  constructor
  . exact function
  . intros x hx E EReal Epos
    have gAt := CubeFunctionContinuous.at with gContinuous, hx
    obtain ⟨D, DReal, DPos, close⟩ := gAt with EReal, Epos
    witness D
    constructor
    . exact DReal
    . constructor
      . exact DPos
      . intros y hy near
        have gNear := close with hy, near
        have yValue := invCube.value with gFunction, hy
        have xValue := invCube.value with gFunction, hx
        rw [yValue, xValue]
        have gy := CubeFunction.value with gFunction, hy
        have gx := CubeFunction.value with gFunction, hx
        obtain ⟨yPos, yLe⟩ := realInvValue.le_one with (atLeastOne with hy)
        obtain ⟨xPos, xLe⟩ := realInvValue.le_one with (atLeastOne with hx)
        have yNonzero : (g(y):R) ≠ (0:R)
          intro zero
          have bound := atLeastOne with hy
          rw zero at bound
          linarith
        have xNonzero : (g(x):R) ≠ (0:R)
          intro zero
          have bound := atLeastOne with hx
          rw zero at bound
          linarith
        have formula := dist.inv_inv with yNonzero, xNonzero
        have yAbs := abs.of_nonnegative with (realLess.implies_le with yPos)
        have xAbs := abs.of_nonnegative with (realLess.implies_le with xPos)
        rw [yAbs, xAbs] at formula
        have dNonneg := dist.nonnegative at g(y), g(x)
        have productLe : realInvValue(g(y)) * realInvValue(g(x)) ≤ (1:R)
          have step := realLe.mul_left_of_nonnegative with xLe, (realLess.implies_le with yPos)
          have one := realMulValue.one_right at realInvValue(g(y))
          rw one at step
          linarith
        have productNonneg : (0:R) ≤ realInvValue(g(y)) * realInvValue(g(x))
          have step := realLe.mul_left_of_nonnegative with (realLess.implies_le with xPos), (realLess.implies_le with yPos)
          have zero := realMulValue.zero_right at realInvValue(g(y))
          rwa zero at step
        have scaled := realLe.mul_left_of_nonnegative with productLe, dNonneg
        have one := realMulValue.one_right at dist(g(y), g(x))
        rw one at scaled
        rw formula
        linarith

-- The larger of two reals, written so that it is built from sums, absolute
-- values, and a constant factor.
def realMax (A B : Real) : Real := half(realOne) * (A + B + abs(A + -B))

theorem realMax.real (A B : Real)
  shows Real(realMax(A, B))
proof
  have product : Real(half(realOne) * (A + B + abs(A + -B))) by typecheck
  unfold realMax
  exact product

theorem realMax.of_le (A B : Real)
  requires below : B ≤ A
  shows realMax(A, B) = A
proof
  have nonneg : (0:R) ≤ A + -B by linarith
  have value := abs.of_nonnegative with nonneg
  have halves := half.add_self at realOne
  have same : realMax(A, B) = half(realOne) * (A + B + abs(A + -B))
    unfold realMax
    rfl
  rw [same, value]
  have twoA : A + B + (A + -B) = A + A by ring
  have expand : half(realOne) * (A + A) = (half(realOne) + half(realOne)) * A by ring
  rw [twoA, expand, halves]
  exact realMulValue.one_left

theorem realMax.of_ge (A B : Real)
  requires below : A ≤ B
  shows realMax(A, B) = B
proof
  have nonpos : A + -B ≤ (0:R) by linarith
  have value := abs.of_nonpositive with nonpos
  have halves := half.add_self at realOne
  have same : realMax(A, B) = half(realOne) * (A + B + abs(A + -B))
    unfold realMax
    rfl
  rw [same, value]
  have twoB : A + B + -(A + -B) = B + B by ring
  have expand : half(realOne) * (B + B) = (half(realOne) + half(realOne)) * B by ring
  rw [twoB, expand, halves]
  exact realMulValue.one_left

theorem realMax.ge_left (A B : Real)
  shows A ≤ realMax(A, B)
proof
  have split := realLess.trichotomy at A, B
  cases split with less | rest
  . have value := realMax.of_ge with (realLess.implies_le with less)
    rw value
    linarith
  . cases rest with same | greater
    . have le : A ≤ B by linarith
      have value := realMax.of_ge with le
      rw value
      linarith
    . have value := realMax.of_le with (realLess.implies_le with greater)
      rw value
      linarith

theorem realMax.ge_right (A B : Real)
  shows B ≤ realMax(A, B)
proof
  have split := realLess.trichotomy at A, B
  cases split with less | rest
  . have value := realMax.of_ge with (realLess.implies_le with less)
    rw value
    linarith
  . cases rest with same | greater
    . have le : A ≤ B by linarith
      have value := realMax.of_ge with le
      rw value
      linarith
    . have value := realMax.of_le with (realLess.implies_le with greater)
      rw value
      linarith

def maxCube (n g h : Set) : Set :=
  mulCube(n, constantFunction(unitCube(n), ℝ, half(realOne)), addCube(n, addCube(n, g, h), absCube(n, addCube(n, g, negCube(n, h)))))

theorem maxCube.value (n : Nat) (g h x : Set)
  requires gFunction : CubeFunction(g, n)
  requires hFunction : CubeFunction(h, n)
  requires hx : x ∈ unitCube(n)
  shows maxCube(n, g, h)(x) = realMax((g(x):R), (h(x):R))
proof
  have gx := CubeFunction.value with gFunction, hx
  have hx2 := CubeFunction.value with hFunction, hx
  have hReal := half.real at realOne
  have hIn : half(realOne) ∈ ℝ by typecheck
  have negFunction : CubeFunction(negCube(n, h), n) := negCube.function with hFunction
  have diffFunction : CubeFunction(addCube(n, g, negCube(n, h)), n) := addCube.function with
    gFunction, negFunction
  have absFunction : CubeFunction(absCube(n, addCube(n, g, negCube(n, h))), n) := absCube.function with
    diffFunction
  have sumFunction : CubeFunction(addCube(n, g, h), n) := addCube.function with gFunction, hFunction
  have totalFunction : CubeFunction(addCube(n, addCube(n, g, h), absCube(n, addCube(n, g, negCube(n, h)))), n) := addCube.function with
    sumFunction, absFunction
  have constantFunction2 : CubeFunction(constantFunction(unitCube(n), ℝ, half(realOne)), n) := constantFunction.function at unitCube(n), ℝ, half(1) with hIn
  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)
    unfold maxCube
    rfl
  rw same
  have v1 := mulCube.value with constantFunction2, totalFunction, hx
  have v2 := constantFunction.apply at unitCube(n), ℝ, x, half(realOne) with hx
  have v3 := addCube.value with sumFunction, absFunction, hx
  have v4 := addCube.value with gFunction, hFunction, hx
  have v5 := absCube.value with diffFunction, hx
  have v6 := addCube.value with gFunction, negFunction, hx
  have v7 := negCube.value with hFunction, hx
  rw [v1, v2, v3, v4, v5, v6, v7]
  unfold realMax
  rfl

theorem maxCube.continuous (n : Nat) (g h : Set)
  requires gContinuous : CubeFunctionContinuous(g, n)
  requires hContinuous : CubeFunctionContinuous(h, n)
  shows CubeFunctionContinuous(maxCube(n, g, h), n)
proof
  have hIn : half(realOne) ∈ ℝ by typecheck
  have constant := constantCube.continuous with hIn
  have neg := negCube.continuous with hContinuous
  have diff := addCube.continuous with gContinuous, neg
  have absolute := absCube.continuous with diff
  have sum := addCube.continuous with gContinuous, hContinuous
  have total := addCube.continuous with sum, absolute
  have product := mulCube.continuous with constant, total
  unfold maxCube
  exact product