Grace/Cumulus/FixedPoint/CubeAssembly.g17

Open in Workbench Download source

Imports

CubeMask · Real.FiniteSum

Declarations

Source

1-- Sums of selected coordinates as continuous cube functions, and maps of the2-- cube assembled coordinate by coordinate from continuous cube functions3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.FixedPoint.CubeAssembly9import CubeMask10import Real.FiniteSum1112-- Sums of the first m selected coordinates, as cube functions.13defgraph prefixSumCube (n S m : Set) (x ∈ unitCube(n)) : ℝ := realPartialSum(maskedPoint(n, S, x), m)14requires nNat : Nat(n)15requires mNat : Nat(m)16proof17  have xFunction := unitCube.point with member18  have sequence := maskedPoint.sequence at n, S, x with xFunction19  exact realPartialSum.real at maskedPoint(n, S, x), m with sequence2021theorem prefixSumCube.continuous (n : Nat) (S : Set) (m : Nat)22  shows m ∈ succ(n) → CubeFunctionContinuous(prefixSumCube(n, S, m), n)23proof24  induction m25  | zero =>26    intro hm27    have zeroIn : (0:R) ∈ ℝ by typecheck28    have constant := constantCube.continuous at n, (0:R) with zeroIn29    have function : CubeFunction(prefixSumCube(n, S, 0), n)30      exact prefixSumCube.function at n, S, 0 with *31    apply CubeFunctionContinuous.congr with function, constant32    intros x hx33    have value := prefixSumCube.value at n, S, 0, x with *34    have constantValue := constantFunction.apply at unitCube(n), ℝ, x, (0:R) with hx, zeroIn35    rw [value, constantValue]36    exact realPartialSum.zero at maskedPoint(n, S, x)37  | succ(j) using ih =>38    intro hm39    have jNat : Nat(j) by typecheck40    have jIn : j ∈ succ(n)41      have less := Less.of_membership with hm42      have below : j < succ(n) by arith43      exact membership.of_Less with below44    have jInN : j ∈ n45      have less := Less.of_membership with hm46      have below : j < n by arith47      exact membership.of_Less with below48    have previous := ih with jIn49    have weightNat := indicator.natural at S, j50    have weightReal := realNat.real at indicator(S, j)51    have weightIn : (realNat(indicator(S, j)):R) ∈ ℝ by typecheck52    have constant := constantCube.continuous at n, (realNat(indicator(S, j)):R) with weightIn53    have coordinate := coordinateCube.continuous at n, j with jInN54    have term := mulCube.continuous with constant, coordinate55    have total := addCube.continuous with previous, term56    have function : CubeFunction(prefixSumCube(n, S, succ(j)), n)57      exact prefixSumCube.function at n, S, succ(j) with *58    apply CubeFunctionContinuous.congr with function, total59    intros x hx60    have xFunction := unitCube.point with hx61    have previousFunction := CubeFunctionContinuous.function with previous62    have termFunction := CubeFunctionContinuous.function with term63    have constantFunction2 := CubeFunctionContinuous.function with constant64    have coordinateFunction := CubeFunctionContinuous.function with coordinate65    have value := prefixSumCube.value at n, S, succ(j), x with *66    have previousValue := prefixSumCube.value at n, S, j, x with *67    have sumValue := addCube.value at n, prefixSumCube(n, S, j), mulCube(n, constantFunction(unitCube(n), ℝ, (realNat(indicator(S, j)):R)), coordinateCube(n, j)), x with previousFunction, termFunction, hx68    have termValue := mulCube.value at n, constantFunction(unitCube(n), ℝ, (realNat(indicator(S, j)):R)), coordinateCube(n, j), x with constantFunction2, coordinateFunction, hx69    have constantValue := constantFunction.apply at unitCube(n), ℝ, x, (realNat(indicator(S, j)):R) with hx, weightIn70    have coordinateValue := coordinateCube.value at n, j, x with jInN, hx71    have step := realPartialSum.succ at maskedPoint(n, S, x), j72    have masked := maskedPoint.coordinate at n, S, x, j with xFunction, jInN73    have sequence := maskedPoint.sequence at n, S, x with xFunction74    have xReal := unitCube.coordinate_real with hx, jInN75    rw [value, sumValue, previousValue, termValue, constantValue, coordinateValue, step, masked]76    linarith7778def sumCube (n S : Set) : Set := prefixSumCube(n, S, n)7980theorem sumCube.continuous (n : Nat) (S : Set)81  shows CubeFunctionContinuous(sumCube(n, S), n)82proof83  have all := prefixSumCube.continuous at n, S, n84  have same : sumCube(n, S) = prefixSumCube(n, S, n)85    unfold sumCube86    rfl87  rw same88  exact all with (bootstrap.succ.self at n)8990theorem sumCube.value (n : Nat) (S x : Set)91  requires hx : x ∈ unitCube(n)92  shows sumCube(n, S)(x) = realPartialSum(maskedPoint(n, S, x), n)93proof94  have same : sumCube(n, S) = prefixSumCube(n, S, n)95    unfold sumCube96    rfl97  rw same98  exact prefixSumCube.value at n, S, n, x with *99100-- A map of the cube assembled from one cube function per coordinate.101defgraph assembledPoint (n G x : Set) (i ∈ n) : ℝ := G(i)(x)102requires family : ∀ i ∈ n, CubeFunction(G(i), n)103requires hx : x ∈ unitCube(n)104proof105  exact CubeFunction.value with (family with member), hx106107defgraph assembledMap (n G : Set) (x ∈ unitCube(n)) : unitCube(n) := assembledPoint(n, G, x)108requires family : ∀ i ∈ n, CubeFunction(G(i), n)109requires bounds : ∀ i ∈ n, ∀ x ∈ unitCube(n), (0:R) ≤ (G(i)(x):R) ∧ (G(i)(x):R) ≤ (1:R)110proof111  have function := assembledPoint.function with family, member112  apply unitCube.membership.backward113  constructor114  . exact functionSpace.mem_iff.backward with function115  . intros i hi116    have value := assembledPoint.value with family, member, hi117    have forI := bounds with hi118    obtain ⟨lower, upper⟩ := forI with member119    apply closedInterval.membership.backward120    rw value121    constructor122    . exact CubeFunction.value with (family with hi), member123    . exact ⟨lower, upper⟩124125theorem assembledMap.coordinate (n : Nat) (G x i : Set)126  requires family : ∀ i ∈ n, CubeFunction(G(i), n)127  requires bounds : ∀ i ∈ n, ∀ x ∈ unitCube(n), (0:R) ≤ (G(i)(x):R) ∧ (G(i)(x):R) ≤ (1:R)128  requires hx : x ∈ unitCube(n)129  requires hi : i ∈ n130  shows assembledMap(n, G)(x)(i) = G(i)(x)131proof132  have value := assembledMap.value with family, bounds, hx133  have point := assembledPoint.value with family, hx, hi134  rw [value, point]135  rfl136137-- Finitely many coordinate functions have a common tolerance at a point.138theorem assembledMap.common_tolerance (n : Nat) (G x : Set) (E : Real) (m : Nat)139  requires family : ∀ i ∈ n, CubeFunctionContinuous(G(i), n)140  requires hx : x ∈ unitCube(n)141  requires positive : 0 < E142  shows m ∈ succ(n) → ∃ D ∈ ℝ, (0:R) < D ∧ (∀ y ∈ unitCube(n), ((∀ j ∈ n, dist(y(j), x(j)) < D) → (∀ i ∈ m, dist(G(i)(y), G(i)(x)) < E)))143proof144  induction m145  | zero =>146    intro hm147    have oneIn : (1:R) ∈ ℝ by typecheck148    have onePos : (0:R) < (1:R) by linarith149    witness (1:R)150    constructor151    . exact oneIn152    . constructor153      . exact onePos154      . intros y hy near i hi155        exfalso156        rw nat.zero at hi157        simpa using hi158  | succ(j) using ih =>159    intro hm160    have jNat : Nat(j) by typecheck161    have jIn : j ∈ succ(n)162      have less := Less.of_membership with hm163      have below : j < succ(n) by arith164      exact membership.of_Less with below165    have jInN : j ∈ n166      have less := Less.of_membership with hm167      have below : j < n by arith168      exact membership.of_Less with below169    obtain ⟨D1, D1Real, D1Pos, previous⟩ := ih with jIn170    have jAt := CubeFunctionContinuous.at with (family with jInN), hx171    have EReal : E ∈ ℝ by typecheck172    obtain ⟨D2, D2Real, D2Pos, close⟩ := jAt with EReal, positive173    obtain ⟨D, DReal, DPos, DBelow1, DBelow2⟩ := positive.below_both with D1Pos, D2Pos174    have shrunk := CubeFunctionContinuousAt.shrink at G(j), n, x, E, D2, D with hx, close, (realLess.implies_le with DBelow2)175    witness D176    constructor177    . exact DReal178    . constructor179      . exact DPos180      . intros y hy near i hi181        have nearD1 : ∀ k ∈ n, dist(y(k), x(k)) < D1182          intros k hk183          have step := near with hk184          have yReal := unitCube.coordinate_real with hy, hk185          have xReal := unitCube.coordinate_real with hx, hk186          have distReal := dist.real at y(k), x(k)187          linarith188        have split := bootstrap.succ.membership.forward with hi189        cases split with below | same190        . have forY := previous with hy, nearD1191          exact forY with below192        . rw same193          exact shrunk with hy, near194195theorem assembledMap.continuous (n : Nat) (G : Set)196  requires family : ∀ i ∈ n, CubeFunctionContinuous(G(i), n)197  requires bounds : ∀ i ∈ n, ∀ x ∈ unitCube(n), (0:R) ≤ (G(i)(x):R) ∧ (G(i)(x):R) ≤ (1:R)198  shows CubeContinuous(assembledMap(n, G), n)199proof200  have functions : ∀ i ∈ n, CubeFunction(G(i), n)201    intros i hi202    exact CubeFunctionContinuous.function with (family with hi)203  have function := assembledMap.function with functions, bounds204  constructor205  . exact function206  . intros x hx E EReal Epos207    have all := assembledMap.common_tolerance with family, hx, Epos208    obtain ⟨D, DReal, DPos, close⟩ := all with (bootstrap.succ.self at n)209    witness D210    constructor211    . exact DReal212    . constructor213      . exact DPos214      . intros y hy near i hi215        have yValue := assembledMap.coordinate with functions, bounds, hy, hi216        have xValue := assembledMap.coordinate with functions, bounds, hx, hi217        rw [yValue, xValue]218        have forY := close with hy, near219        exact forY with hi220