Grace/Cumulus/FixedPoint/BrouwerCube.g17

Open in Workbench Download source

Imports

BrouwerGrid

Declarations

Source

1-- Brouwer's fixed point theorem for the unit cube: every continuous self-map2-- of [0, 1]ⁿ has a fixed point, from Kuhn's lemma on finer and finer grids3-- 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.BrouwerCube9import BrouwerGrid1011-- At every grid level Kuhn's lemma gives a cell carrying, in each direction,12-- a point labelled 0 and a point labelled 1; one such cell is chosen.13defchoose kuhnCell (n f : Set, k : Nat) (base ∈ functionSpace(n, ℕ)) :=14  (∀ j ∈ n, base(j) < doubling(k)) ∧15  ∀ i ∈ n, ∃ u ∈ functionSpace(n, succ(doubling(k))), ∃ v ∈ functionSpace(n, succ(doubling(k))),16    (∀ j ∈ n, LessEqual(base(j), u(j)) ∧ LessEqual(u(j), add(base(j), (1:N)))) ∧ (∀ j ∈ n, LessEqual(base(j), v(j)) ∧ LessEqual(v(j), add(base(j), (1:N)))) ∧17    gridLabels(k, n, f)(u)(i) = (0:N) ∧ gridLabels(k, n, f)(v)(i) ≠ (0:N)18requires nNat : Nat(n)19proof20  obtain ⟨q, qNat, shape⟩ := doubling.successor at k21  have labFunction := gridLabels.function at k, n, f22  rw shape at labFunction23  have zeroWall := gridLabels.zero_wall at k, n, q, f with shape24  have fullWall := gridLabels.full_wall at k, n, q, f with shape25  obtain ⟨base, baseIn, bounds, pairs⟩ := kuhn.lemma at q, n, gridLabels(k, n, f), functionSpace(n, succ(succ(0))) with labFunction, zeroWall, fullWall26  witness base27  refine ⟨baseIn, ?_, ?_⟩28  . intros j hj29    have bound := bounds with hj30    rw ← shape at bound31    exact bound32  . intros i hi33    obtain ⟨u, hu, v, hv, uCell, vCell, uLabel, vLabel⟩ := pairs with hi34    rw ← shape at hu35    rw ← shape at hv36    witness u37    constructor38    . exact hu39    . witness v40      constructor41      . exact hv42      . exact ⟨uCell, vCell, uLabel, vLabel⟩4344theorem kuhnCell.grid (n : Nat) (f : Set) (k : Nat)45  shows kuhnCell(n, f, k) ∈ functionSpace(n, succ(doubling(k)))46proof47  obtain ⟨baseIn, bounds, pairs⟩ := kuhnCell.selected at n, f, k48  have baseFunction := functionSpace.mem_iff.forward with baseIn49  apply functionSpace.mem_iff.backward50  apply FunctionBetween.codomain_of_values with baseFunction51  intros j hj52  have bound := bounds with hj53  have valueIn := FunctionBetween.apply_closed with baseFunction, hj54  have valueNat := nat.omega.backward with valueIn55  have less : kuhnCell(n, f, k)(j) < succ(doubling(k)) by arith56  exact membership.of_Less with less5758defchoose lowPoint (n f : Set, k : Nat, i : Set) (u ∈ functionSpace(n, succ(doubling(k)))) :=59  (∀ j ∈ n, LessEqual(kuhnCell(n, f, k)(j), u(j)) ∧ LessEqual(u(j), add(kuhnCell(n, f, k)(j), (1:N)))) ∧ gridLabels(k, n, f)(u)(i) = (0:N)60requires nNat : Nat(n)61requires hi : i ∈ n62proof63  obtain ⟨baseIn, bounds, pairs⟩ := kuhnCell.selected at n, f, k64  obtain ⟨u, hu, v, hv, uCell, vCell, uLabel, vLabel⟩ := pairs with hi65  witness u66  refine ⟨hu, uCell, uLabel⟩6768defchoose highPoint (n f : Set, k : Nat, i : Set) (v ∈ functionSpace(n, succ(doubling(k)))) :=69  (∀ j ∈ n, LessEqual(kuhnCell(n, f, k)(j), v(j)) ∧ LessEqual(v(j), add(kuhnCell(n, f, k)(j), (1:N)))) ∧ gridLabels(k, n, f)(v)(i) ≠ (0:N)70requires nNat : Nat(n)71requires hi : i ∈ n72proof73  obtain ⟨baseIn, bounds, pairs⟩ := kuhnCell.selected at n, f, k74  obtain ⟨u, hu, v, hv, uCell, vCell, uLabel, vLabel⟩ := pairs with hi75  witness v76  refine ⟨hv, vCell, vLabel⟩7778-- The chosen cells, low points, and high points, scaled into the cube.79defgraph basePoints (n f : Set) (k ∈ ℕ) : functionSpace(n, ℝ) := gridPoint(k, n)(kuhnCell(n, f, k))80requires nNat : Nat(n)81proof82  have kNat := nat.omega.backward with member83  have gridFunction := gridPoint.function at k, n with *84  have pointIn := FunctionBetween.apply_closed with gridFunction, (kuhnCell.grid at n, f, k)85  have parts := unitCube.membership.forward with pointIn86  exact parts.left8788defgraph lowPoints (n f i : Set) (k ∈ ℕ) : functionSpace(n, ℝ) := gridPoint(k, n)(lowPoint(n, f, k, i))89requires nNat : Nat(n)90requires hi : i ∈ n91proof92  have kNat := nat.omega.backward with member93  have gridFunction := gridPoint.function at k, n with *94  have selected := lowPoint.selected at n, f, k, i with *95  have pointIn := FunctionBetween.apply_closed with gridFunction, selected.left96  have parts := unitCube.membership.forward with pointIn97  exact parts.left9899defgraph highPoints (n f i : Set) (k ∈ ℕ) : functionSpace(n, ℝ) := gridPoint(k, n)(highPoint(n, f, k, i))100requires nNat : Nat(n)101requires hi : i ∈ n102proof103  have kNat := nat.omega.backward with member104  have gridFunction := gridPoint.function at k, n with *105  have selected := highPoint.selected at n, f, k, i with *106  have pointIn := FunctionBetween.apply_closed with gridFunction, selected.left107  have parts := unitCube.membership.forward with pointIn108  exact parts.left109110theorem basePoints.sequence (n : Nat) (f : Set)111  shows PointSequence(basePoints(n, f), n)112proof113  exact basePoints.function at n, f with *114115theorem basePoints.in_cube (n : Nat) (f k : Set)116  requires hk : k ∈ ℕ117  shows basePoints(n, f)(k) ∈ unitCube(n)118proof119  have kNat := nat.omega.backward with hk120  have value := basePoints.value at n, f, k with *121  rw value122  have gridFunction := gridPoint.function at k, n with *123  exact FunctionBetween.apply_closed with gridFunction, (kuhnCell.grid at n, f, k)124125theorem lowPoints.sequence (n : Nat) (f i : Set)126  requires hi : i ∈ n127  shows PointSequence(lowPoints(n, f, i), n)128proof129  exact lowPoints.function at n, f, i with *130131theorem lowPoints.in_cube (n : Nat) (f i k : Set)132  requires hi : i ∈ n133  requires hk : k ∈ ℕ134  shows lowPoints(n, f, i)(k) ∈ unitCube(n)135proof136  have kNat := nat.omega.backward with hk137  have value := lowPoints.value at n, f, i, k with *138  rw value139  have gridFunction := gridPoint.function at k, n with *140  have selected := lowPoint.selected at n, f, k, i with *141  exact FunctionBetween.apply_closed with gridFunction, selected.left142143theorem highPoints.sequence (n : Nat) (f i : Set)144  requires hi : i ∈ n145  shows PointSequence(highPoints(n, f, i), n)146proof147  exact highPoints.function at n, f, i with *148149theorem highPoints.in_cube (n : Nat) (f i k : Set)150  requires hi : i ∈ n151  requires hk : k ∈ ℕ152  shows highPoints(n, f, i)(k) ∈ unitCube(n)153proof154  have kNat := nat.omega.backward with hk155  have value := highPoints.value at n, f, i, k with *156  rw value157  have gridFunction := gridPoint.function at k, n with *158  have selected := highPoint.selected at n, f, k, i with *159  exact FunctionBetween.apply_closed with gridFunction, selected.left160161-- The low and high points stay within one grid width of the cell's base162-- point in every coordinate.163theorem lowPoints.close (n : Nat) (f i k j : Set)164  requires hi : i ∈ n165  requires hk : k ∈ ℕ166  requires hj : j ∈ n167  shows dist(lowPoints(n, f, i)(k)(j), basePoints(n, f)(k)(j)) ≤ (dyadicRadius(k):R)168proof169  have kNat := nat.omega.backward with hk170  have lowValue := lowPoints.value at n, f, i, k with *171  have baseValue := basePoints.value at n, f, k with *172  rw [lowValue, baseValue]173  have selected := lowPoint.selected at n, f, k, i with *174  have uIn := selected.left175  have cell := selected.right.left with hj176  have baseIn := kuhnCell.grid at n, f, k177  have gridU := gridPoint.coordinate with uIn, hj178  have gridB := gridPoint.coordinate with baseIn, hj179  rw [gridU, gridB]180  have uFunction := functionSpace.mem_iff.forward with uIn181  have bFunction := functionSpace.mem_iff.forward with baseIn182  have close := scaledPoint.close with bFunction, uFunction, hj, cell.left, cell.right183  have uValue := scaledPoint.value at k, n, lowPoint(n, f, k, i), j with *184  have bValue := scaledPoint.value at k, n, kuhnCell(n, f, k), j with *185  rwa [uValue, bValue] at close186187theorem highPoints.close (n : Nat) (f i k j : Set)188  requires hi : i ∈ n189  requires hk : k ∈ ℕ190  requires hj : j ∈ n191  shows dist(highPoints(n, f, i)(k)(j), basePoints(n, f)(k)(j)) ≤ (dyadicRadius(k):R)192proof193  have kNat := nat.omega.backward with hk194  have highValue := highPoints.value at n, f, i, k with *195  have baseValue := basePoints.value at n, f, k with *196  rw [highValue, baseValue]197  have selected := highPoint.selected at n, f, k, i with *198  have vIn := selected.left199  have cell := selected.right.left with hj200  have baseIn := kuhnCell.grid at n, f, k201  have gridV := gridPoint.coordinate with vIn, hj202  have gridB := gridPoint.coordinate with baseIn, hj203  rw [gridV, gridB]204  have vFunction := functionSpace.mem_iff.forward with vIn205  have bFunction := functionSpace.mem_iff.forward with baseIn206  have close := scaledPoint.close with bFunction, vFunction, hj, cell.left, cell.right207  have vValue := scaledPoint.value at k, n, highPoint(n, f, k, i), j with *208  have bValue := scaledPoint.value at k, n, kuhnCell(n, f, k), j with *209  rwa [vValue, bValue] at close210211-- Along a subsequence on which the base points converge, so do the low and212-- high points, since the grid widths shrink to nothing.213theorem closePoints.converges (n : Nat) (Y X s L j : Set)214  requires ySequence : PointSequence(Y, n)215  requires xSequence : PointSequence(X, n)216  requires yCube : ∀ k ∈ ℕ, Y(k) ∈ unitCube(n)217  requires increasing : StrictlyIncreasingNat(s)218  requires hj : j ∈ n219  requires LReal : L ∈ ℝ220  requires close : ∀ k ∈ ℕ, dist(Y(k)(j), X(k)(j)) ≤ (dyadicRadius(k):R)221  requires converges : ConvergesTo(coordinateSequence(pointSubsequence(X, n, s), n, j), L)222  shows ConvergesTo(coordinateSequence(pointSubsequence(Y, n, s), n, j), L)223proof224  have xSub := pointSubsequence.sequence with xSequence, increasing225  have ySub := pointSubsequence.sequence with ySequence, increasing226  have u := coordinateSequence.sequence with xSub, hj227  have v := coordinateSequence.sequence with ySub, hj228  have sFunction := increasing.left229  apply ConvergesTo.of_asymptotically_close with converges230  unfold AsymptoticallyClose231  refine ⟨u, v, ?_⟩232  intros E EIn Epos233  obtain ⟨N, NIn, tail⟩ := dyadicRadii.eventually_below with Epos234  witness N235  constructor236  . exact NIn237  . intros m hm bound238    have mNat := nat.omega.backward with hm239    have NNat := nat.omega.backward with NIn240    have index := StrictlyIncreasingNat.index_le_value at s, m with increasing241    have sm := FunctionBetween.apply_closed with sFunction, hm242    have smNat := nat.omega.backward with sm243    have far : N ≤ s(m) by arith244    have small := tail with sm, far245    have vValue := coordinateSequence.value at pointSubsequence(Y, n, s), n, j, m with ySub, hj246    have uValue := coordinateSequence.value at pointSubsequence(X, n, s), n, j, m with xSub, hj247    have ySubValue := pointSubsequence.value with ySequence, increasing, hm248    have xSubValue := pointSubsequence.value with xSequence, increasing, hm249    rw [vValue, uValue, ySubValue, xSubValue]250    have near := close with sm251    have yIn := yCube with sm252    have yReal := unitCube.coordinate_real with yIn, hj253    have xPoint := PointSequence.point with xSequence, sm254    have xReal := FunctionBetween.apply_closed with xPoint, hj255    apply openBall.membership.backward256    constructor257    . exact yReal258    . linarith259260theorem lowPoints.coordinate (n : Nat) (f i s m j : Set)261  requires hi : i ∈ n262  requires increasing : StrictlyIncreasingNat(s)263  requires hm : m ∈ ℕ264  requires hj : j ∈ n265  shows coordinateSequence(pointSubsequence(lowPoints(n, f, i), n, s), n, j)(m) = scaledPoint(s(m), n, lowPoint(n, f, s(m), i))(j)266proof267  have lowSeq := lowPoints.sequence at n, f, i with hi268  have lowSub := pointSubsequence.sequence with lowSeq, increasing269  have sm := FunctionBetween.apply_closed with increasing.left, hm270  have smNat := nat.omega.backward with sm271  have value := coordinateSequence.value at pointSubsequence(lowPoints(n, f, i), n, s), n, j, m with lowSub, hj272  have subValue := pointSubsequence.value with lowSeq, increasing, hm273  have lowValue := lowPoints.value at n, f, i, s(m) with *274  rw [value, subValue, lowValue]275  have selected := lowPoint.selected at n, f, s(m), i with *276  have gridValue := gridPoint.value at s(m), n, lowPoint(n, f, s(m), i) with *277  rw gridValue278  rfl279280theorem highPoints.coordinate (n : Nat) (f i s m j : Set)281  requires hi : i ∈ n282  requires increasing : StrictlyIncreasingNat(s)283  requires hm : m ∈ ℕ284  requires hj : j ∈ n285  shows coordinateSequence(pointSubsequence(highPoints(n, f, i), n, s), n, j)(m) = scaledPoint(s(m), n, highPoint(n, f, s(m), i))(j)286proof287  have highSeq := highPoints.sequence at n, f, i with hi288  have highSub := pointSubsequence.sequence with highSeq, increasing289  have sm := FunctionBetween.apply_closed with increasing.left, hm290  have smNat := nat.omega.backward with sm291  have value := coordinateSequence.value at pointSubsequence(highPoints(n, f, i), n, s), n, j, m with highSub, hj292  have subValue := pointSubsequence.value with highSeq, increasing, hm293  have highValue := highPoints.value at n, f, i, s(m) with *294  rw [value, subValue, highValue]295  have selected := highPoint.selected at n, f, s(m), i with *296  have gridValue := gridPoint.value at s(m), n, highPoint(n, f, s(m), i) with *297  rw gridValue298  rfl299300theorem imageSequence.coordinate (n : Nat) (f Y s m j : Set)301  requires map : CubeMap(f, n)302  requires ySequence : PointSequence(Y, n)303  requires yCube : ∀ k ∈ ℕ, Y(k) ∈ unitCube(n)304  requires increasing : StrictlyIncreasingNat(s)305  requires hm : m ∈ ℕ306  requires hj : j ∈ n307  shows coordinateSequence(imageSequence(f, pointSubsequence(Y, n, s), n), n, j)(m) = f(Y(s(m)))(j)308proof309  have ySub := pointSubsequence.sequence with ySequence, increasing310  have subCube : ∀ k ∈ ℕ, pointSubsequence(Y, n, s)(k) ∈ unitCube(n)311    intros k hk312    have subValue := pointSubsequence.value with ySequence, increasing, hk313    rw subValue314    exact yCube with (FunctionBetween.apply_closed with increasing.left, hk)315  have imageSeq := imageSequence.sequence with map, ySub, subCube316  have value := coordinateSequence.value at imageSequence(f, pointSubsequence(Y, n, s), n), n, j, m with imageSeq, hj317  have imageValue := imageSequence.value with map, ySub, subCube, hm318  have subValue := pointSubsequence.value with ySequence, increasing, hm319  rw [value, imageValue, subValue]320  rfl321322-- Brouwer's fixed point theorem for the cube.323theorem brouwer.cube (n : Nat) (f : Set)324  requires continuous : CubeContinuous(f, n)325  shows ∃ x ∈ unitCube(n), f(x) = x326proof327  have map := continuous.left328  have fFunction := CubeMap.function with map329  have baseSeq := basePoints.sequence at n, f330  have baseCube : ∀ k ∈ ℕ, basePoints(n, f)(k) ∈ unitCube(n)331    intros k hk332    exact basePoints.in_cube with hk333  obtain ⟨s, increasing, x, xIn, limits⟩ := unitCube.bolzano_weierstrass with baseSeq, baseCube334  have xFunction := unitCube.point with xIn335  have fxIn := FunctionBetween.apply_closed with fFunction, xIn336  have fxFunction := unitCube.point with fxIn337  witness x338  constructor339  . exact xIn340  . apply FunctionBetween.ext with fxFunction, xFunction341    intros i hi342    have xiReal := FunctionBetween.apply_closed with xFunction, hi343    have fxiReal := FunctionBetween.apply_closed with fxFunction, hi344    have lowSeq := lowPoints.sequence at n, f, i with hi345    have lowCube : ∀ k ∈ ℕ, lowPoints(n, f, i)(k) ∈ unitCube(n)346      intros k hk347      exact lowPoints.in_cube with hi, hk348    have lowSub := pointSubsequence.sequence with lowSeq, increasing349    have lowSubCube : ∀ k ∈ ℕ, pointSubsequence(lowPoints(n, f, i), n, s)(k) ∈ unitCube(n)350      intros k hk351      have subValue := pointSubsequence.value with lowSeq, increasing, hk352      rw subValue353      exact lowCube with (FunctionBetween.apply_closed with increasing.left, hk)354    have lowConverges : ∀ j ∈ n, ConvergesTo(coordinateSequence(pointSubsequence(lowPoints(n, f, i), n, s), n, j), x(j))355      intros j hj356      have xjReal := FunctionBetween.apply_closed with xFunction, hj357      have close : ∀ k ∈ ℕ, dist(lowPoints(n, f, i)(k)(j), basePoints(n, f)(k)(j)) ≤ (dyadicRadius(k):R)358        intros k hk359        exact lowPoints.close with hi, hk, hj360      exact closePoints.converges with lowSeq, baseSeq, lowCube, increasing, hj, xjReal, close, (limits with hj)361    have imageLow := CubeContinuous.sequential with continuous, lowSub, lowSubCube, xIn, lowConverges362    have lowLimit := lowConverges with hi363    have imageLowLimit := imageLow with hi364    have lowOrdered : PointwiseLE(coordinateSequence(pointSubsequence(lowPoints(n, f, i), n, s), n, i), coordinateSequence(imageSequence(f, pointSubsequence(lowPoints(n, f, i), n, s), n), n, i))365      unfold PointwiseLE366      intros m hm367      have sm := FunctionBetween.apply_closed with increasing.left, hm368      have smNat := nat.omega.backward with sm369      have left := lowPoints.coordinate at n, f, i, s, m, i with hi, increasing, hm, hi370      have right := imageSequence.coordinate with map, lowSeq, lowCube, increasing, hm, hi371      have lowValue := lowPoints.value at n, f, i, s(m) with *372      rw [left, right, lowValue]373      have selected := lowPoint.selected at n, f, s(m), i with *374      have le := gridLabels.low_le with map, selected.left, hi, selected.right.right375      exact realLe.characterization.forward with le376    have lower := ConvergesTo.le_of_le_terms with lowLimit, imageLowLimit, lowOrdered377    have highSeq := highPoints.sequence at n, f, i with hi378    have highCube : ∀ k ∈ ℕ, highPoints(n, f, i)(k) ∈ unitCube(n)379      intros k hk380      exact highPoints.in_cube with hi, hk381    have highSub := pointSubsequence.sequence with highSeq, increasing382    have highSubCube : ∀ k ∈ ℕ, pointSubsequence(highPoints(n, f, i), n, s)(k) ∈ unitCube(n)383      intros k hk384      have subValue := pointSubsequence.value with highSeq, increasing, hk385      rw subValue386      exact highCube with (FunctionBetween.apply_closed with increasing.left, hk)387    have highConverges : ∀ j ∈ n, ConvergesTo(coordinateSequence(pointSubsequence(highPoints(n, f, i), n, s), n, j), x(j))388      intros j hj389      have xjReal := FunctionBetween.apply_closed with xFunction, hj390      have close : ∀ k ∈ ℕ, dist(highPoints(n, f, i)(k)(j), basePoints(n, f)(k)(j)) ≤ (dyadicRadius(k):R)391        intros k hk392        exact highPoints.close with hi, hk, hj393      exact closePoints.converges with highSeq, baseSeq, highCube, increasing, hj, xjReal, close, (limits with hj)394    have imageHigh := CubeContinuous.sequential with continuous, highSub, highSubCube, xIn, highConverges395    have highLimit := highConverges with hi396    have imageHighLimit := imageHigh with hi397    have highOrdered : PointwiseLE(coordinateSequence(imageSequence(f, pointSubsequence(highPoints(n, f, i), n, s), n), n, i), coordinateSequence(pointSubsequence(highPoints(n, f, i), n, s), n, i))398      unfold PointwiseLE399      intros m hm400      have sm := FunctionBetween.apply_closed with increasing.left, hm401      have smNat := nat.omega.backward with sm402      have left := highPoints.coordinate at n, f, i, s, m, i with hi, increasing, hm, hi403      have right := imageSequence.coordinate with map, highSeq, highCube, increasing, hm, hi404      have highValue := highPoints.value at n, f, i, s(m) with *405      rw [left, right, highValue]406      have selected := highPoint.selected at n, f, s(m), i with *407      have ge := gridLabels.high_ge with map, selected.left, hi, selected.right.right408      exact realLe.characterization.forward with ge409    have upper := ConvergesTo.le_of_le_terms with imageHighLimit, highLimit, highOrdered410    have upperLe := realLe.characterization.forward with upper411    have lowerLe := realLe.characterization.forward with lower412    exact RealLe.antisymmetric with upperLe, lowerLe413