Grace/Cumulus/FixedPoint/SimplexRetraction.g17

Open in Workbench Download source

Imports

BlockSimplex

Declarations

• retractCoordinate def
• retractCoordinate.definition theorem derivation
• retractCoordinate.continuous theorem derivation
• retractCoordinate.value theorem derivation
• retractCoordinate.bounds theorem derivation
• retractFamily defgraph
• retractFamily.coordinate theorem derivation
• retractFamily.continuous theorem derivation
• retractFamily.functions theorem derivation
• retractFamily.bounds theorem derivation
• retraction def
• retraction.definition theorem derivation
• retraction.continuous theorem derivation
• retraction.map theorem derivation
• retraction.in_cube theorem derivation
• retraction.coordinate theorem derivation
• retraction.block_sum theorem derivation
• retraction.in_product theorem derivation
• retraction.fixed theorem derivation

Source

1-- A continuous retraction of the cube onto a product of simplices: each2-- coordinate is shifted toward an anchor point by the shortfall of its block3-- sum and then divided by the scale, so that every block sums to one4-- 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.SimplexRetraction10import BlockSimplex1112-- Coordinate j of the retraction toward the anchor a.13def retractCoordinate (n blk a j : Set) : Set :=14  mulCube(n, addCube(n, coordinateCube(n, j), mulCube(n, excessCube(n, blk, blk(j)), constantFunction(unitCube(n), ℝ, a(j)))), invCube(n, scaleCube(n, blk, blk(j))))1516theorem retractCoordinate.definition (n blk a j : Set)17  shows retractCoordinate(n, blk, a, j) = mulCube(n, addCube(n, coordinateCube(n, j), mulCube(n, excessCube(n, blk, blk(j)), constantFunction(unitCube(n), ℝ, a(j)))), invCube(n, scaleCube(n, blk, blk(j))))18proof19  unfold retractCoordinate20  rfl2122theorem retractCoordinate.continuous (n : Nat) (blk a j : Set)23  requires ha : a ∈ unitCube(n)24  requires hj : j ∈ n25  shows CubeFunctionContinuous(retractCoordinate(n, blk, a, j), n)26proof27  have aj := unitCube.coordinate_real with ha, hj28  have coordinate := coordinateCube.continuous with hj29  have excess := excessCube.continuous at n, blk, blk(j)30  have anchor := constantCube.continuous with aj31  have shift := mulCube.continuous with excess, anchor32  have numerator := addCube.continuous with coordinate, shift33  have scale := scaleCube.continuous at n, blk, blk(j)34  have atLeastOne : ∀ x ∈ unitCube(n), (1:R) ≤ (scaleCube(n, blk, blk(j))(x):R)35    intros x hx36    exact scaleCube.at_least_one with hx37  have inverse := invCube.continuous with scale, atLeastOne38  have same := retractCoordinate.definition at n, blk, a, j39  rw same40  exact mulCube.continuous with numerator, inverse4142theorem retractCoordinate.value (n : Nat) (blk a j x : Set)43  requires ha : a ∈ unitCube(n)44  requires hj : j ∈ n45  requires hx : x ∈ unitCube(n)46  shows retractCoordinate(n, blk, a, j)(x) = ((x(j):R) + (excessCube(n, blk, blk(j))(x):R) * (a(j):R)) * realInvValue((scaleCube(n, blk, blk(j))(x):R))47proof48  have aj := unitCube.coordinate_real with ha, hj49  have coordinate := coordinateCube.continuous with hj50  have excess := excessCube.continuous at n, blk, blk(j)51  have anchor := constantCube.continuous with aj52  have shift := mulCube.continuous with excess, anchor53  have numerator := addCube.continuous with coordinate, shift54  have scale := scaleCube.continuous at n, blk, blk(j)55  have atLeastOne : ∀ y ∈ unitCube(n), (1:R) ≤ (scaleCube(n, blk, blk(j))(y):R)56    intros y hy57    exact scaleCube.at_least_one with hy58  have inverse := invCube.continuous with scale, atLeastOne59  have coordinateFunction := CubeFunctionContinuous.function with coordinate60  have excessFunction := CubeFunctionContinuous.function with excess61  have anchorFunction := CubeFunctionContinuous.function with anchor62  have shiftFunction := CubeFunctionContinuous.function with shift63  have numeratorFunction := CubeFunctionContinuous.function with numerator64  have scaleFunction := CubeFunctionContinuous.function with scale65  have inverseFunction := CubeFunctionContinuous.function with inverse66  have same := retractCoordinate.definition at n, blk, a, j67  have product := mulCube.value with numeratorFunction, inverseFunction, hx68  have sum := addCube.value with coordinateFunction, shiftFunction, hx69  have shiftValue := mulCube.value with excessFunction, anchorFunction, hx70  have coordinateValue := coordinateCube.value with hj, hx71  have anchorValue := constantFunction.apply with hx, aj72  have inverseValue := invCube.value with scaleFunction, hx73  rw [same, product, sum, shiftValue, coordinateValue, anchorValue, inverseValue]74  rfl7576-- Every retracted coordinate lies in [0, 1].77theorem retractCoordinate.bounds (n : Nat) (blk a j x : Set)78  requires ha : a ∈ unitCube(n)79  requires hj : j ∈ n80  requires hx : x ∈ unitCube(n)81  shows (0:R) ≤ (retractCoordinate(n, blk, a, j)(x):R) ∧ (retractCoordinate(n, blk, a, j)(x):R) ≤ (1:R)82proof83  have value := retractCoordinate.value at n, blk, a, j, x with ha, hj, hx84  have xInterval := unitCube.coordinate with hx, hj85  obtain ⟨xReal, xLower, xUpper⟩ := closedInterval.membership.forward with xInterval86  have aInterval := unitCube.coordinate with ha, hj87  obtain ⟨aReal, aLower, aUpper⟩ := closedInterval.membership.forward with aInterval88  have sumReal := blockSum.real at n, blk, blk(j), x with hx89  have excessReal := excessCube.real at n, blk, blk(j), x with hx90  have scaleReal := scaleCube.real at n, blk, blk(j), x with hx91  have excessNonneg := excessCube.nonnegative at n, blk, blk(j), x with hx92  have scaleAtLeastOne := scaleCube.at_least_one at n, blk, blk(j), x with hx93  have sumExcess := scaleCube.sum_excess at n, blk, blk(j), x with hx94  have termBound := blockSum.ge_coordinate at n, blk, x, j with hx, hj95  obtain ⟨inversePositive, inverseLe⟩ := realInvValue.le_one with scaleAtLeastOne96  have inverseNonneg := realLess.implies_le with inversePositive97  have shiftNonneg := realMulValue.nonnegative with excessNonneg, aLower98  have numeratorNonneg : (0:R) ≤ (x(j):R) + (excessCube(n, blk, blk(j))(x):R) * (a(j):R) by linarith99  have scaleNonzero : (scaleCube(n, blk, blk(j))(x):R) ≠ (0:R)100    intro zero101    rw zero at scaleAtLeastOne102    linarith103  have cancel := realInvValue.mul_right with scaleNonzero104  have shiftLe : (excessCube(n, blk, blk(j))(x):R) * (a(j):R) ≤ (excessCube(n, blk, blk(j))(x):R)105    have step := realLe.mul_left_of_nonnegative with aUpper, excessNonneg106    have one := realMulValue.one_right at excessCube(n, blk, blk(j))(x)107    rwa one at step108  have numeratorLe : (x(j):R) + (excessCube(n, blk, blk(j))(x):R) * (a(j):R) ≤ (scaleCube(n, blk, blk(j))(x):R) by linarith109  have scaled := realLe.mul_right_of_nonnegative with numeratorLe, inverseNonneg110  rw cancel at scaled111  rw value112  constructor113  . exact realMulValue.nonnegative with numeratorNonneg, inverseNonneg114  . exact scaled115116-- The family of retracted coordinates and the assembled retraction.117defgraph retractFamily (n blk a : Set) (j ∈ n) : functionSpace(unitCube(n), ℝ) := retractCoordinate(n, blk, a, j)118requires nNat : Nat(n)119requires ha : a ∈ unitCube(n)120proof121  have continuous := retractCoordinate.continuous at n, blk, a, j with ha, member122  have function := CubeFunctionContinuous.function with continuous123  have between : retractCoordinate(n, blk, a, j) : unitCube(n) → ℝ124    exact CubeFunction.function with function125  exact functionSpace.mem_iff.backward with between126127theorem retractFamily.coordinate (n : Nat) (blk a j : Set)128  requires ha : a ∈ unitCube(n)129  requires hj : j ∈ n130  shows retractFamily(n, blk, a)(j) = retractCoordinate(n, blk, a, j)131proof132  exact retractFamily.value at n, blk, a, j with *133134theorem retractFamily.continuous (n : Nat) (blk a : Set)135  requires ha : a ∈ unitCube(n)136  shows ∀ j ∈ n, CubeFunctionContinuous(retractFamily(n, blk, a)(j), n)137proof138  intros j hj139  have same := retractFamily.coordinate at n, blk, a, j with ha, hj140  rw same141  exact retractCoordinate.continuous with ha, hj142143theorem retractFamily.functions (n : Nat) (blk a : Set)144  requires ha : a ∈ unitCube(n)145  shows ∀ j ∈ n, CubeFunction(retractFamily(n, blk, a)(j), n)146proof147  intros j hj148  have continuous := retractFamily.continuous at n, blk, a with ha149  exact CubeFunctionContinuous.function with (continuous with hj)150151theorem retractFamily.bounds (n : Nat) (blk a : Set)152  requires ha : a ∈ unitCube(n)153  shows ∀ j ∈ n, ∀ x ∈ unitCube(n), (0:R) ≤ (retractFamily(n, blk, a)(j)(x):R) ∧ (retractFamily(n, blk, a)(j)(x):R) ≤ (1:R)154proof155  intros j hj x hx156  have same := retractFamily.coordinate at n, blk, a, j with ha, hj157  rw same158  exact retractCoordinate.bounds with ha, hj, hx159160def retraction (n blk a : Set) : Set := assembledMap(n, retractFamily(n, blk, a))161162theorem retraction.definition (n blk a : Set)163  shows retraction(n, blk, a) = assembledMap(n, retractFamily(n, blk, a))164proof165  unfold retraction166  rfl167168theorem retraction.continuous (n : Nat) (blk a : Set)169  requires ha : a ∈ unitCube(n)170  shows CubeContinuous(retraction(n, blk, a), n)171proof172  have family := retractFamily.continuous at n, blk, a with ha173  have bounds := retractFamily.bounds at n, blk, a with ha174  have same := retraction.definition at n, blk, a175  rw same176  exact assembledMap.continuous with family, bounds177178theorem retraction.map (n : Nat) (blk a : Set)179  requires ha : a ∈ unitCube(n)180  shows CubeMap(retraction(n, blk, a), n)181proof182  have continuous := retraction.continuous at n, blk, a with ha183  exact continuous.left184185theorem retraction.in_cube (n : Nat) (blk a x : Set)186  requires ha : a ∈ unitCube(n)187  requires hx : x ∈ unitCube(n)188  shows retraction(n, blk, a)(x) ∈ unitCube(n)189proof190  have map := retraction.map at n, blk, a with ha191  have function := CubeMap.function with map192  exact FunctionBetween.apply_closed with function, hx193194theorem retraction.coordinate (n : Nat) (blk a x j : Set)195  requires ha : a ∈ unitCube(n)196  requires hx : x ∈ unitCube(n)197  requires hj : j ∈ n198  shows retraction(n, blk, a)(x)(j) = ((x(j):R) + (excessCube(n, blk, blk(j))(x):R) * (a(j):R)) * realInvValue((scaleCube(n, blk, blk(j))(x):R))199proof200  have functions := retractFamily.functions at n, blk, a with ha201  have bounds := retractFamily.bounds at n, blk, a with ha202  have same := retraction.definition at n, blk, a203  have assembled := assembledMap.coordinate with functions, bounds, hx, hj204  have family := retractFamily.coordinate at n, blk, a, j with ha, hj205  rw [same, assembled, family]206  exact retractCoordinate.value with ha, hj, hx207208-- Every block of the retracted point sums to one, so the retraction lands in209-- the product of simplices, and it fixes every point of the product.210theorem retraction.block_sum (n : Nat) (m blk a x p : Set)211  requires blkFunction : blk : n → m212  requires ha : a ∈ simplexProduct(n, m, blk)213  requires hx : x ∈ unitCube(n)214  requires hp : p ∈ m215  shows blockSum(n, blk, p)(retraction(n, blk, a)(x)) = (1:R)216proof217  have aCube := simplexProduct.cube with ha218  have anchor := simplexProduct.block_sum with ha, hp219  have image := retraction.in_cube at n, blk, a, x with aCube, hx220  have shifted : ∀ j ∈ n, j ∈ blockSet(n, blk, p) → retraction(n, blk, a)(x)(j) = ((x(j):R) + (excessCube(n, blk, p)(x):R) * (a(j):R)) * realInvValue((scaleCube(n, blk, p)(x):R))221    intros j hj inBlock222    have parts := blockSet.membership.forward with inBlock223    have block := parts.right224    have value := retraction.coordinate at n, blk, a, x, j with aCube, hx, hj225    rwa block at value226  have sumSame := blockSum.definition at n, blk, p227  have affine := sumCube.affine with hx, aCube, image, shifted228  rw sumSame at affine229  have sumExcess := scaleCube.sum_excess at n, blk, p, x with hx230  have scaleAtLeastOne := scaleCube.at_least_one at n, blk, p, x with hx231  have scaleNonzero : (scaleCube(n, blk, p)(x):R) ≠ (0:R)232    intro zero233    rw zero at scaleAtLeastOne234    linarith235  have cancel := realInvValue.mul_right with scaleNonzero236  have one := realMulValue.one_right at excessCube(n, blk, p)(x)237  rwa [affine, anchor, one, sumExcess]238239theorem retraction.in_product (n : Nat) (m blk a x : Set)240  requires blkFunction : blk : n → m241  requires ha : a ∈ simplexProduct(n, m, blk)242  requires hx : x ∈ unitCube(n)243  shows retraction(n, blk, a)(x) ∈ simplexProduct(n, m, blk)244proof245  have aCube := simplexProduct.cube with ha246  apply simplexProduct.membership.backward247  constructor248  . exact retraction.in_cube with aCube, hx249  . intros p hp250    exact retraction.block_sum with blkFunction, ha, hx, hp251252theorem retraction.fixed (n : Nat) (m blk a x : Set)253  requires blkFunction : blk : n → m254  requires ha : a ∈ simplexProduct(n, m, blk)255  requires hx : x ∈ simplexProduct(n, m, blk)256  shows retraction(n, blk, a)(x) = x257proof258  have aCube := simplexProduct.cube with ha259  have xCube := simplexProduct.cube with hx260  have image := retraction.in_cube at n, blk, a, x with aCube, xCube261  have imageFunction := unitCube.point with image262  have xFunction := unitCube.point with xCube263  apply FunctionBetween.ext with imageFunction, xFunction264  intros j hj265  have value := retraction.coordinate at n, blk, a, x, j with aCube, xCube, hj266  have block := FunctionBetween.apply_closed with blkFunction, hj267  have sumOne := simplexProduct.block_sum with hx, block268  have excessValue := excessCube.value at n, blk, blk(j), x with xCube269  have scaleValue := scaleCube.value at n, blk, blk(j), x with xCube270  rw sumOne at excessValue271  rw sumOne at scaleValue272  have shift : (1:R) + -(1:R) = (0:R) by linarith273  rw shift at excessValue274  have excessZero := realMax.of_le with (realLe.reflexive at (0:R))275  have scaleOne := realMax.of_le with (realLe.reflexive at (1:R))276  rw excessZero at excessValue277  rw scaleOne at scaleValue278  have oneNonzero : (1:R) ≠ (0:R)279    intro equal280    linarith281  have inverseOne : realInvValue((1:R)) = (1:R)282    have cancel := realInvValue.mul_right with oneNonzero283    have one := realMulValue.one_left at realInvValue((1:R))284    rwa one at cancel285  have xj := unitCube.coordinate_real with xCube, hj286  have aj := unitCube.coordinate_real with aCube, hj287  rw [value, excessValue, scaleValue, inverseOne]288  ring289