Grace/Cumulus/FixedPoint/BlockSimplex.g17

Open in Workbench Download source

Imports

BlockSums

Declarations

• blockSet def
• blockSet.own theorem derivation
• blockSum def
• blockSum.definition theorem derivation
• blockSum.continuous theorem derivation
• blockSum.function theorem derivation
• blockSum.real theorem derivation
• blockSum.nonnegative theorem derivation
• blockSum.ge_coordinate theorem derivation
• simplexProduct def
• simplexProduct.cube theorem derivation
• simplexProduct.block_sum theorem derivation
• excessCube def
• scaleCube def
• excessCube.definition theorem derivation
• scaleCube.definition theorem derivation
• excessCube.continuous theorem derivation
• scaleCube.continuous theorem derivation
• excessCube.value theorem derivation
• scaleCube.value theorem derivation
• realMax.excess theorem derivation
• excessCube.nonnegative theorem derivation
• scaleCube.at_least_one theorem derivation
• scaleCube.ge_sum theorem derivation
• scaleCube.sum_excess theorem derivation
• scaleCube.real theorem derivation
• excessCube.real theorem derivation

Source

1-- Blocks of coordinates, their sums, the product of simplices cut out of the2-- cube by asking every block sum to be one, and the two continuous3-- corrections, max(0, 1 − s) and max(1, s), applied to a block sum s4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.FixedPoint.BlockSimplex10import BlockSums1112-- The coordinates that the block map blk sends to p.13def blockSet (n blk p : Set) : Set := { i ∈ n | blk(i) = p }1415theorem blockSet.own (n blk j : Set)16  requires hj : j ∈ n17  shows j ∈ blockSet(n, blk, blk(j))18proof19  apply blockSet.membership.backward20  exact ⟨hj, rfl⟩2122-- The sum of the coordinates in block p, as a cube function.23def blockSum (n blk p : Set) : Set := sumCube(n, blockSet(n, blk, p))2425theorem blockSum.definition (n blk p : Set)26  shows sumCube(n, blockSet(n, blk, p)) = blockSum(n, blk, p)27proof28  unfold blockSum29  rfl3031theorem blockSum.continuous (n : Nat) (blk p : Set)32  shows CubeFunctionContinuous(blockSum(n, blk, p), n)33proof34  have same := blockSum.definition at n, blk, p35  have continuous := sumCube.continuous at n, blockSet(n, blk, p)36  rwa same at continuous3738theorem blockSum.function (n : Nat) (blk p : Set)39  shows CubeFunction(blockSum(n, blk, p), n)40proof41  exact CubeFunctionContinuous.function with (blockSum.continuous at n, blk, p)4243theorem blockSum.real (n : Nat) (blk p x : Set)44  requires hx : x ∈ unitCube(n)45  shows blockSum(n, blk, p)(x) ∈ ℝ46proof47  exact CubeFunction.value with (blockSum.function at n, blk, p), hx4849theorem blockSum.nonnegative (n : Nat) (blk p x : Set)50  requires hx : x ∈ unitCube(n)51  shows (0:R) ≤ (blockSum(n, blk, p)(x):R)52proof53  have same := blockSum.definition at n, blk, p54  have bound := sumCube.nonnegative at n, blockSet(n, blk, p), x with hx55  rwa same at bound5657theorem blockSum.ge_coordinate (n : Nat) (blk x j : Set)58  requires hx : x ∈ unitCube(n)59  requires hj : j ∈ n60  shows (x(j):R) ≤ (blockSum(n, blk, blk(j))(x):R)61proof62  have same := blockSum.definition at n, blk, blk(j)63  have inBlock := blockSet.own at n, blk, j with hj64  have bound := sumCube.ge_coordinate with hx, hj, inBlock65  rwa same at bound6667-- The product of simplices: the points of the cube whose block sums are one.68def simplexProduct (n m blk : Set) : Set :=69  { x ∈ unitCube(n) | ∀ p ∈ m, blockSum(n, blk, p)(x) = (1:R) }7071theorem simplexProduct.cube (n m blk x : Set)72  requires hx : x ∈ simplexProduct(n, m, blk)73  shows x ∈ unitCube(n)74proof75  have parts := simplexProduct.membership.forward with hx76  exact parts.left7778theorem simplexProduct.block_sum (n m blk x p : Set)79  requires hx : x ∈ simplexProduct(n, m, blk)80  requires hp : p ∈ m81  shows blockSum(n, blk, p)(x) = (1:R)82proof83  have parts := simplexProduct.membership.forward with hx84  exact parts.right with hp8586-- The shortfall of a block sum below one, and the block sum capped below by one.87def excessCube (n blk p : Set) : Set :=88  maxCube(n, constantFunction(unitCube(n), ℝ, (0:R)), addCube(n, constantFunction(unitCube(n), ℝ, (1:R)), negCube(n, blockSum(n, blk, p))))8990def scaleCube (n blk p : Set) : Set :=91  maxCube(n, constantFunction(unitCube(n), ℝ, (1:R)), blockSum(n, blk, p))9293theorem excessCube.definition (n blk p : Set)94  shows excessCube(n, blk, p) = maxCube(n, constantFunction(unitCube(n), ℝ, (0:R)), addCube(n, constantFunction(unitCube(n), ℝ, (1:R)), negCube(n, blockSum(n, blk, p))))95proof96  unfold excessCube97  rfl9899theorem scaleCube.definition (n blk p : Set)100  shows scaleCube(n, blk, p) = maxCube(n, constantFunction(unitCube(n), ℝ, (1:R)), blockSum(n, blk, p))101proof102  unfold scaleCube103  rfl104105theorem excessCube.continuous (n : Nat) (blk p : Set)106  shows CubeFunctionContinuous(excessCube(n, blk, p), n)107proof108  have zeroIn : (0:R) ∈ ℝ by typecheck109  have oneIn : (1:R) ∈ ℝ by typecheck110  have zero := constantCube.continuous with zeroIn111  have one := constantCube.continuous with oneIn112  have sum := blockSum.continuous at n, blk, p113  have negative := negCube.continuous with sum114  have shifted := addCube.continuous with one, negative115  have same := excessCube.definition at n, blk, p116  rw same117  exact maxCube.continuous with zero, shifted118119theorem scaleCube.continuous (n : Nat) (blk p : Set)120  shows CubeFunctionContinuous(scaleCube(n, blk, p), n)121proof122  have oneIn : (1:R) ∈ ℝ by typecheck123  have one := constantCube.continuous with oneIn124  have sum := blockSum.continuous at n, blk, p125  have same := scaleCube.definition at n, blk, p126  rw same127  exact maxCube.continuous with one, sum128129theorem excessCube.value (n : Nat) (blk p x : Set)130  requires hx : x ∈ unitCube(n)131  shows excessCube(n, blk, p)(x) = realMax((0:R), (1:R) + -(blockSum(n, blk, p)(x):R))132proof133  have zeroIn : (0:R) ∈ ℝ by typecheck134  have oneIn : (1:R) ∈ ℝ by typecheck135  have zero := constantCube.continuous with zeroIn136  have one := constantCube.continuous with oneIn137  have sum := blockSum.continuous at n, blk, p138  have negative := negCube.continuous with sum139  have shifted := addCube.continuous with one, negative140  have zeroFunction := CubeFunctionContinuous.function with zero141  have oneFunction := CubeFunctionContinuous.function with one142  have sumFunction := CubeFunctionContinuous.function with sum143  have negativeFunction := CubeFunctionContinuous.function with negative144  have shiftedFunction := CubeFunctionContinuous.function with shifted145  have same := excessCube.definition at n, blk, p146  have maxValue := maxCube.value with zeroFunction, shiftedFunction, hx147  have zeroValue := constantFunction.apply at unitCube(n), ℝ, x, (0:R) with hx148  have oneValue := constantFunction.apply at unitCube(n), ℝ, x, (1:R) with hx149  have shiftedValue := addCube.value with oneFunction, negativeFunction, hx150  have negativeValue := negCube.value with sumFunction, hx151  rw [same, maxValue, zeroValue, shiftedValue, oneValue, negativeValue]152  rfl153154theorem scaleCube.value (n : Nat) (blk p x : Set)155  requires hx : x ∈ unitCube(n)156  shows scaleCube(n, blk, p)(x) = realMax((1:R), (blockSum(n, blk, p)(x):R))157proof158  have oneIn : (1:R) ∈ ℝ by typecheck159  have one := constantCube.continuous with oneIn160  have oneFunction := CubeFunctionContinuous.function with one161  have sumFunction := blockSum.function at n, blk, p162  have same := scaleCube.definition at n, blk, p163  have maxValue := maxCube.value with oneFunction, sumFunction, hx164  have oneValue := constantFunction.apply at unitCube(n), ℝ, x, (1:R) with hx165  rw [same, maxValue, oneValue]166  rfl167168-- The two corrections are nonnegative, the scale is at least one, and a block169-- sum plus its shortfall is exactly the scale.170theorem realMax.excess (S : Real)171  shows S + realMax((0:R), (1:R) + -S) = realMax((1:R), S)172proof173  have alternatives : (1:R) ≤ S ∨ ¬(1:R) ≤ S by tauto174  cases alternatives with atLeastOne | below175  . have shortfall : (1:R) + -S ≤ (0:R) by linarith176    have excessZero := realMax.of_le with shortfall177    have scaleS := realMax.of_ge with atLeastOne178    rw [excessZero, scaleS]179    linarith180  . have notLess : ¬((1:R) < S)181      intro less182      apply below183      exact realLess.implies_le with less184    have atMostOne := realLe.of_not_less with notLess185    have shortfall : (0:R) ≤ (1:R) + -S by linarith186    have excessShortfall := realMax.of_ge with shortfall187    have scaleOne := realMax.of_le with atMostOne188    rw [excessShortfall, scaleOne]189    linarith190191theorem excessCube.nonnegative (n : Nat) (blk p x : Set)192  requires hx : x ∈ unitCube(n)193  shows (0:R) ≤ (excessCube(n, blk, p)(x):R)194proof195  have value := excessCube.value at n, blk, p, x with hx196  rw value197  exact realMax.ge_left198199theorem scaleCube.at_least_one (n : Nat) (blk p x : Set)200  requires hx : x ∈ unitCube(n)201  shows (1:R) ≤ (scaleCube(n, blk, p)(x):R)202proof203  have value := scaleCube.value at n, blk, p, x with hx204  rw value205  exact realMax.ge_left206207theorem scaleCube.ge_sum (n : Nat) (blk p x : Set)208  requires hx : x ∈ unitCube(n)209  shows (blockSum(n, blk, p)(x):R) ≤ (scaleCube(n, blk, p)(x):R)210proof211  have value := scaleCube.value at n, blk, p, x with hx212  rw value213  exact realMax.ge_right214215theorem scaleCube.sum_excess (n : Nat) (blk p x : Set)216  requires hx : x ∈ unitCube(n)217  shows (blockSum(n, blk, p)(x):R) + (excessCube(n, blk, p)(x):R) = scaleCube(n, blk, p)(x)218proof219  have excessValue := excessCube.value at n, blk, p, x with hx220  have scaleValue := scaleCube.value at n, blk, p, x with hx221  rw [excessValue, scaleValue]222  exact realMax.excess223224theorem scaleCube.real (n : Nat) (blk p x : Set)225  requires hx : x ∈ unitCube(n)226  shows scaleCube(n, blk, p)(x) ∈ ℝ227proof228  exact CubeFunction.value with (CubeFunctionContinuous.function with (scaleCube.continuous at n, blk, p)), hx229230theorem excessCube.real (n : Nat) (blk p x : Set)231  requires hx : x ∈ unitCube(n)232  shows excessCube(n, blk, p)(x) ∈ ℝ233proof234  exact CubeFunction.value with (CubeFunctionContinuous.function with (excessCube.continuous at n, blk, p)), hx235