Grace/Cumulus/FixedPoint/BrouwerSimplex.g17

Open in Workbench Download source

Imports

SimplexRetraction · BrouwerCube

Declarations

Source

1-- Brouwer's fixed point theorem for a product of simplices: a continuous2-- self-map of the product is composed with the retraction of the cube onto3-- it, the cube theorem gives a fixed point, and that point lies in the product4-- 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.BrouwerSimplex10import SimplexRetraction11import BrouwerCube1213-- Self-maps of the product of simplices, continuous in the sup metric.14predicate ProductMap (f n m blk : Set) :=15  FunctionBetween(f, simplexProduct(n, m, blk), simplexProduct(n, m, blk))1617predicate ProductContinuousAt (f n m blk x : Set) :=18  ∀ E ∈ ℝ, (0:R) < E → ∃ D ∈ ℝ, (0:R) < D ∧19    (∀ y ∈ simplexProduct(n, m, blk), ((∀ i ∈ n, dist(y(i), x(i)) < D) → (∀ i ∈ n, dist(f(y)(i), f(x)(i)) < E)))2021predicate ProductContinuous (f n m blk : Set) :=22  ProductMap(f, n, m, blk) ∧ ∀ x ∈ simplexProduct(n, m, blk), ProductContinuousAt(f, n, m, blk, x)2324theorem ProductMap.function (f n m blk : Set)25  requires map : ProductMap(f, n, m, blk)26  shows f : simplexProduct(n, m, blk) → simplexProduct(n, m, blk)27proof28  exact map2930theorem ProductMap.apply (f n m blk x : Set)31  requires map : ProductMap(f, n, m, blk)32  requires hx : x ∈ simplexProduct(n, m, blk)33  shows f(x) ∈ simplexProduct(n, m, blk)34proof35  have function := ProductMap.function with map36  exact FunctionBetween.apply_closed with function, hx3738-- The self-map of the cube obtained by retracting first.39defgraph composedMap (n m blk a f : Set) (x ∈ unitCube(n)) : unitCube(n) := f(retraction(n, blk, a)(x))40requires nNat : Nat(n)41requires blkFunction : blk : n → m42requires ha : a ∈ simplexProduct(n, m, blk)43requires map : ProductMap(f, n, m, blk)44proof45  have image := retraction.in_product with blkFunction, ha, member46  have value := ProductMap.apply with map, image47  exact simplexProduct.cube with value4849theorem composedMap.continuous (n : Nat) (m blk a f : Set)50  requires blkFunction : blk : n → m51  requires ha : a ∈ simplexProduct(n, m, blk)52  requires continuous : ProductContinuous(f, n, m, blk)53  shows CubeContinuous(composedMap(n, m, blk, a, f), n)54proof55  have map := continuous.left56  have aCube := simplexProduct.cube with ha57  have function := composedMap.function at n, m, blk, a, f with *58  have cubeMap : CubeMap(composedMap(n, m, blk, a, f), n) by exact function59  constructor60  . exact cubeMap61  . intros x hx E EReal Epos62    have rx := retraction.in_product with blkFunction, ha, hx63    have fAt := continuous.right with rx64    obtain ⟨D1, D1Real, D1Pos, fClose⟩ := fAt with EReal, Epos65    have rContinuous := retraction.continuous at n, blk, a with aCube66    have rAt := rContinuous.right with hx67    obtain ⟨D, DReal, DPos, rClose⟩ := rAt with D1Real, D1Pos68    witness D69    constructor70    . exact DReal71    . constructor72      . exact DPos73      . intros y hy near74        have ry := retraction.in_product with blkFunction, ha, hy75        have rNear := rClose with hy, near76        have fNear := fClose with ry, rNear77        have yValue := composedMap.value at n, m, blk, a, f, y with *78        have xValue := composedMap.value at n, m, blk, a, f, x with *79        intros i hi80        rw [yValue, xValue]81        exact fNear with hi8283-- Brouwer's theorem for the product of simplices.84theorem brouwer.simplexProduct (n : Nat) (m a f : Set) (blk : n → m)85  requires ha : a ∈ simplexProduct(n, m, blk)86  requires continuous : ProductContinuous(f, n, m, blk)87  shows ∃ x ∈ simplexProduct(n, m, blk), f(x) = x88proof89  have blkFunction : blk : n → m by assumption90  have map := continuous.left91  have composed := composedMap.continuous with blkFunction, ha, continuous92  obtain ⟨x, hx, fixed⟩ := brouwer.cube with composed93  have value := composedMap.value at n, m, blk, a, f, x with *94  rw value at fixed95  have rx := retraction.in_product with blkFunction, ha, hx96  have inProduct := ProductMap.apply with map, rx97  rw fixed at inProduct98  have same := retraction.fixed with blkFunction, ha, inProduct99  rw same at fixed100  witness x101  exact ⟨inProduct, fixed⟩102103-- A continuous self-map of the whole cube that keeps the product of104-- simplices also has a fixed point inside the product.105defgraph composeCube (n f g : Set) (x ∈ unitCube(n)) : unitCube(n) := f(g(x))106requires fMap : CubeMap(f, n)107requires gMap : CubeMap(g, n)108proof109  have gx := FunctionBetween.apply_closed with (CubeMap.function with gMap), member110  exact FunctionBetween.apply_closed with (CubeMap.function with fMap), gx111112theorem composeCube.continuous (n : Nat) (f g : Set)113  requires fContinuous : CubeContinuous(f, n)114  requires gContinuous : CubeContinuous(g, n)115  shows CubeContinuous(composeCube(n, f, g), n)116proof117  have fMap := fContinuous.left118  have gMap := gContinuous.left119  have function := composeCube.function with fMap, gMap120  have map : CubeMap(composeCube(n, f, g), n) by exact function121  constructor122  . exact map123  . intros x hx E EReal Epos124    have gx := FunctionBetween.apply_closed with (CubeMap.function with gMap), hx125    have fAt := fContinuous.right with gx126    obtain ⟨D1, D1Real, D1Pos, fClose⟩ := fAt with EReal, Epos127    have gAt := gContinuous.right with hx128    obtain ⟨D, DReal, DPos, gClose⟩ := gAt with D1Real, D1Pos129    witness D130    constructor131    . exact DReal132    . constructor133      . exact DPos134      . intros y hy near135        have gy := FunctionBetween.apply_closed with (CubeMap.function with gMap), hy136        have gNear := gClose with hy, near137        have fNear := fClose with gy, gNear138        have yValue := composeCube.value with fMap, gMap, hy139        have xValue := composeCube.value with fMap, gMap, hx140        intros i hi141        rw [yValue, xValue]142        exact fNear with hi143144theorem brouwer.simplexProduct_of_cube (n : Nat) (m blk a f : Set)145  requires blkFunction : blk : n → m146  requires ha : a ∈ simplexProduct(n, m, blk)147  requires continuous : CubeContinuous(f, n)148  requires preserves : ∀ x ∈ simplexProduct(n, m, blk), f(x) ∈ simplexProduct(n, m, blk)149  shows ∃ x ∈ simplexProduct(n, m, blk), f(x) = x150proof151  have aCube := simplexProduct.cube with ha152  have fMap := continuous.left153  have rContinuous := retraction.continuous at n, blk, a with aCube154  have rMap := rContinuous.left155  have composed := composeCube.continuous with continuous, rContinuous156  obtain ⟨x, hx, fixed⟩ := brouwer.cube with composed157  have value := composeCube.value with fMap, rMap, hx158  rw value at fixed159  have rx := retraction.in_product with blkFunction, ha, hx160  have inProduct := preserves with rx161  rw fixed at inProduct162  have same := retraction.fixed with blkFunction, ha, inProduct163  rw same at fixed164  witness x165  exact ⟨inProduct, fixed⟩166