Grace/Cumulus/FixedPoint/BrouwerGrid.g17

Open in Workbench Download source

Imports

CubeContinuity · KuhnInduction · Real.RootTwo

Declarations

Source

1-- Dyadic grids on the unit cube: grid points scaled into the cube, the2-- labelling of a grid point by comparing it with its image under a self-map3-- of the cube, and the closeness of the points of one cell4-- 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.BrouwerGrid10import CubeContinuity11import KuhnInduction12import Real.RootTwo1314-- Grid sizes 1, 2, 4, …, matched to the dyadic widths 1, 1/2, 1/4, ….15def doubling (k : Nat) → Nat16  | zero => succ(0)17  | succ(k) => add(doubling(k), doubling(k))1819theorem doubling.zero20  shows doubling(0) = succ(0)21proof22  simp [doubling]2324theorem doubling.step (k : Nat)25  shows doubling(succ(k)) = add(doubling(k), doubling(k))26proof27  simp [doubling]2829theorem doubling.successor (k : Nat)30  shows ∃ q, Nat(q) ∧ doubling(k) = succ(q)31proof32  induction k33  | zero =>34    witness 035    exact doubling.zero36  | succ(j) using ih =>37    obtain ⟨q, qNat, shape⟩ := ih38    have sumNat : Nat(add(succ(q), q)) by typecheck39    witness add(succ(q), q)40    have step := doubling.step at j41    rw [step, shape]42    exact add.succ_right at q, succ(q)4344theorem doubling.real_scale (k : Nat)45  shows (realNat(doubling(k)):R) * (dyadicRadius(k):R) = (1:R)46proof47  induction k48  | zero =>49    have d : dyadicRadius(0) = (1:R)50      simp [dyadicRadius]51    rw [doubling.zero, d, realNat.one]52    exact realMulValue.one_right at (1:R)53  | succ(j) using ih =>54    have s := doubling.step at j55    have d : dyadicRadius(succ(j)) = half(dyadicRadius(j))56      simp [dyadicRadius]57    have dReal := dyadicRadius.real at j58    have aReal := realNat.real at doubling(j)59    have hReal := half.real at dyadicRadius(j)60    have halves := half.add_self at dyadicRadius(j)61    rw [s, d, realNat.add]62    have expand : ((realNat(doubling(j)):R) + (realNat(doubling(j)):R)) * (half(dyadicRadius(j)):R) = (realNat(doubling(j)):R) * ((half(dyadicRadius(j)):R) + (half(dyadicRadius(j)):R))63      ring64    rw [expand, halves]65    exact ih6667-- Scaling a grid point into the unit cube.68defgraph scaledPoint (k n x : Set) (i ∈ n) : ℝ := (realNat(x(i)):R) * (dyadicRadius(k):R)69requires kNat : Nat(k)70requires xFunction : x : n → succ(doubling(k))71proof72  have xi := FunctionBetween.apply_closed with xFunction, member73  have xiNat := natural.member at succ(doubling(k)) with xi74  exact realMulValue.real at realNat(x(i)), dyadicRadius(k)7576theorem realNat.le_of_le (m n : Nat)77  requires bound : m ≤ n78  shows realNat(m) ≤ realNat(n)79proof80  have less : m < succ(n) by arith81  have inSucc := membership.of_Less with less82  have split := bootstrap.succ.membership.forward with inSucc83  cases split with below | same84  . have strict := realNat.lt_of_lt with (Less.of_membership with below)85    exact realLess.implies_le with strict86  . rw same87    linarith8889theorem scaledPoint.nonnegative (k n : Nat) (x i : Set)90  requires xFunction : x : n → succ(doubling(k))91  requires hi : i ∈ n92  shows (0:R) ≤ scaledPoint(k, n, x)(i)93proof94  have value := scaledPoint.value at k, n, x, i with *95  rw value96  have xi := FunctionBetween.apply_closed with xFunction, hi97  have xiNat := natural.member at succ(doubling(k)) with xi98  have nonneg := realNat.nonnegative at x(i)99  have positive := dyadicRadius.positive at k100  have dNonneg := realLess.implies_le with positive101  have step := realLe.mul_right_of_nonnegative with nonneg, dNonneg102  have zero := realMulValue.zero_left at dyadicRadius(k)103  rwa zero at step104105theorem scaledPoint.le_one (k n : Nat) (x i : Set)106  requires xFunction : x : n → succ(doubling(k))107  requires hi : i ∈ n108  shows scaledPoint(k, n, x)(i) ≤ (1:R)109proof110  have value := scaledPoint.value at k, n, x, i with *111  rw value112  have xi := FunctionBetween.apply_closed with xFunction, hi113  have xiNat := natural.member at succ(doubling(k)) with xi114  have xiLess := Less.of_membership with xi115  have xiLe : x(i) ≤ doubling(k) by arith116  have bound := realNat.le_of_le with xiLe117  have positive := dyadicRadius.positive at k118  have dNonneg := realLess.implies_le with positive119  have step := realLe.mul_right_of_nonnegative with bound, dNonneg120  have scale := doubling.real_scale at k121  rwa scale at step122123defgraph gridPoint (k n : Set) (x ∈ functionSpace(n, succ(doubling(k)))) : unitCube(n) := scaledPoint(k, n, x)124requires kNat : Nat(k)125requires nNat : Nat(n)126proof127  have xFunction := functionSpace.mem_iff.forward with member128  have function := scaledPoint.function with kNat, xFunction129  apply unitCube.membership.backward130  constructor131  . exact functionSpace.mem_iff.backward with function132  . intros i hi133    apply closedInterval.membership.backward134    constructor135    . exact FunctionBetween.apply_closed with function, hi136    . constructor137      . exact scaledPoint.nonnegative with xFunction, hi138      . exact scaledPoint.le_one with xFunction, hi139140theorem gridPoint.coordinate (k n : Nat) (x i : Set)141  requires hx : x ∈ functionSpace(n, succ(doubling(k)))142  requires hi : i ∈ n143  shows gridPoint(k, n)(x)(i) = (realNat(x(i)):R) * (dyadicRadius(k):R)144proof145  have xFunction := functionSpace.mem_iff.forward with hx146  have value := gridPoint.value at k, n, x with *147  have scaled := scaledPoint.value at k, n, x, i with *148  rw [value, scaled]149  rfl150151-- The label of a grid point in direction i is 0 when the point lies on the152-- near wall or below its image there, and 1 otherwise.153predicate LowLabel (k n f x i : Set) :=154  x(i) = (0:N) ∨ (x(i) ≠ doubling(k) ∧ (scaledPoint(k, n, x)(i):R) ≤ (f(gridPoint(k, n)(x))(i):R))155156theorem two.member (b : Set)157  requires hb : b ∈ succ(succ(0))158  shows b = (0:N) ∨ b = succ(0)159proof160  have split := bootstrap.succ.membership.forward with hb161  cases split with below | same162  . left163    exact successor.zero_member with below164  . right165    exact same166167defunique labelBit (k n f x i : Set) (b ∈ succ(succ(0))) := (b = (0:N) ↔ LowLabel(k, n, f, x, i))168proof169  have alternatives : LowLabel(k, n, f, x, i) ∨ ¬LowLabel(k, n, f, x, i) by tauto170  have zeroIn : (0:N) ∈ succ(succ(0))171    have less : (0:N) < succ(succ(0)) by arith172    exact membership.of_Less with less173  have oneIn := bootstrap.succ.self at succ(0)174  cases alternatives with low | high175  . refine ⟨(0:N), zeroIn, ?_⟩176    constructor177    . intro h178      exact low179    . intro h180      rfl181  . refine ⟨succ(0), oneIn, ?_⟩182    constructor183    . intro h184      arith185    . intro h186      exfalso187      exact high with h188uniqueness189  intros a ha first b hb second190  have alternatives : LowLabel(k, n, f, x, i) ∨ ¬LowLabel(k, n, f, x, i) by tauto191  cases alternatives with low | high192  . have aZero := first.backward with low193    have bZero := second.backward with low194    rw [aZero, bZero]195    rfl196  . have aSplit := two.member with ha197    have bSplit := two.member with hb198    cases aSplit with aZero | aOne199    . exfalso200      exact high with (first.forward with aZero)201    . cases bSplit with bZero | bOne202      . exfalso203        exact high with (second.forward with bZero)204      . rw [aOne, bOne]205        rfl206207defgraph labelVector (k n f x : Set) (i ∈ n) : succ(succ(0)) := labelBit(k, n, f, x, i)208proof209  have selected := labelBit.selected at k, n, f, x, i210  exact selected.left211212defgraph gridLabels (k n f : Set) (x ∈ functionSpace(n, succ(doubling(k)))) : functionSpace(n, succ(succ(0))) := labelVector(k, n, f, x)213proof214  exact functionSpace.mem_iff.backward with (labelVector.function at k, n, f, x)215216theorem gridLabels.bit (k n f x i : Set)217  requires hx : x ∈ functionSpace(n, succ(doubling(k)))218  requires hi : i ∈ n219  shows gridLabels(k, n, f)(x)(i) = (0:N) ↔ LowLabel(k, n, f, x, i)220proof221  have value := gridLabels.value at k, n, f, x with hx222  have vector := labelVector.value at k, n, f, x, i with hi223  rw [value, vector]224  have selected := labelBit.selected at k, n, f, x, i225  exact selected.right226227theorem gridLabels.in_two (k n f x i : Set)228  requires hx : x ∈ functionSpace(n, succ(doubling(k)))229  requires hi : i ∈ n230  shows gridLabels(k, n, f)(x)(i) ∈ succ(succ(0))231proof232  have value := gridLabels.value at k, n, f, x with hx233  have vector := labelVector.value at k, n, f, x, i with hi234  rw [value, vector]235  have selected := labelBit.selected at k, n, f, x, i236  exact selected.left237238theorem gridLabels.zero_wall (k n q : Nat) (f : Set)239  requires shape : doubling(k) = succ(q)240  shows ∀ x ∈ functionSpace(n, succ(succ(q))), ∀ j ∈ n, x(j) = (0:N) → gridLabels(k, n, f)(x)(j) = (0:N)241proof242  intros x hx j hj zero243  rw ← shape at hx244  have bit := gridLabels.bit at k, n, f, x, j with hx, hj245  apply bit.backward246  left247  exact zero248249theorem gridLabels.full_wall (k n q : Nat) (f : Set)250  requires shape : doubling(k) = succ(q)251  shows ∀ x ∈ functionSpace(n, succ(succ(q))), ∀ j ∈ n, x(j) = succ(q) → gridLabels(k, n, f)(x)(j) = (1:N)252proof253  intros x hx j hj full254  rw ← shape at hx255  rw ← shape at full256  have bit := gridLabels.bit at k, n, f, x, j with hx, hj257  have inTwo := gridLabels.in_two at k, n, f, x, j with hx, hj258  have split := two.member with inTwo259  cases split with zero | one260  . exfalso261    have low := bit.forward with zero262    cases low with isZero | isLow263    . rw [full, shape] at isZero264      arith265    . exact isLow.left with full266  . exact one267268-- The inequalities behind the two labels.269theorem gridLabels.low_le (k n : Nat) (f x i : Set)270  requires map : CubeMap(f, n)271  requires hx : x ∈ functionSpace(n, succ(doubling(k)))272  requires hi : i ∈ n273  requires zero : gridLabels(k, n, f)(x)(i) = (0:N)274  shows (scaledPoint(k, n, x)(i):R) ≤ (f(gridPoint(k, n)(x))(i):R)275proof276  have bit := gridLabels.bit at k, n, f, x, i with hx, hi277  have low := bit.forward with zero278  have fFunction := CubeMap.function with map279  have gridFunction := gridPoint.function at k, n with *280  have gridIn := FunctionBetween.apply_closed with gridFunction, hx281  have imageIn := FunctionBetween.apply_closed with fFunction, gridIn282  have coordinate := unitCube.coordinate with imageIn, hi283  have parts := closedInterval.membership.forward with coordinate284  cases low with isZero | isLow285  . have xFunction := functionSpace.mem_iff.forward with hx286    have value := scaledPoint.value at k, n, x, i with *287    rw [value, isZero, realNat.zero, realMulValue.zero_left]288    exact parts.right.left289  . exact isLow.right290291theorem gridLabels.high_ge (k n : Nat) (f x i : Set)292  requires map : CubeMap(f, n)293  requires hx : x ∈ functionSpace(n, succ(doubling(k)))294  requires hi : i ∈ n295  requires nonzero : gridLabels(k, n, f)(x)(i) ≠ (0:N)296  shows (f(gridPoint(k, n)(x))(i):R) ≤ (scaledPoint(k, n, x)(i):R)297proof298  have bit := gridLabels.bit at k, n, f, x, i with hx, hi299  have notLow : ¬LowLabel(k, n, f, x, i)300    intro low301    exact nonzero with (bit.backward with low)302  have fFunction := CubeMap.function with map303  have gridFunction := gridPoint.function at k, n with *304  have gridIn := FunctionBetween.apply_closed with gridFunction, hx305  have imageIn := FunctionBetween.apply_closed with fFunction, gridIn306  have coordinate := unitCube.coordinate with imageIn, hi307  have parts := closedInterval.membership.forward with coordinate308  have xFunction := functionSpace.mem_iff.forward with hx309  have scaledFunction := scaledPoint.function at k, n, x with *310  have scaledReal := FunctionBetween.apply_closed with scaledFunction, hi311  have alternatives : x(i) = doubling(k) ∨ x(i) ≠ doubling(k) by tauto312  cases alternatives with top | notTop313  . have value := scaledPoint.value at k, n, x, i with *314    have scale := doubling.real_scale at k315    rw [value, top, scale]316    exact parts.right.right317  . have alternatives2 : (scaledPoint(k, n, x)(i):R) ≤ (f(gridPoint(k, n)(x))(i):R) ∨ ¬((scaledPoint(k, n, x)(i):R) ≤ (f(gridPoint(k, n)(x))(i):R))318      tauto319    cases alternatives2 with le | notLe320    . exfalso321      apply notLow322      right323      exact ⟨notTop, le⟩324    . have less := realLess.of_not_le with notLe325      exact realLess.implies_le with less326327-- Two grid points of one cell are within one grid width in every coordinate.328theorem scaledPoint.close (k n : Nat) (base u i : Set)329  requires baseFunction : base : n → succ(doubling(k))330  requires uFunction : u : n → succ(doubling(k))331  requires hi : i ∈ n332  requires lower : LessEqual(base(i), u(i))333  requires upper : LessEqual(u(i), add(base(i), (1:N)))334  shows dist(scaledPoint(k, n, u)(i), scaledPoint(k, n, base)(i)) ≤ (dyadicRadius(k):R)335proof336  have uValue := scaledPoint.value at k, n, u, i with *337  have bValue := scaledPoint.value at k, n, base, i with *338  rw [uValue, bValue]339  have bi := FunctionBetween.apply_closed with baseFunction, hi340  have biNat := natural.member at succ(doubling(k)) with bi341  have ui := FunctionBetween.apply_closed with uFunction, hi342  have uiNat := natural.member at succ(doubling(k)) with ui343  have positive := dyadicRadius.positive at k344  have dNonneg := realLess.implies_le with positive345  have below := realNat.le_of_le with lower346  have succBound : LessEqual(u(i), succ(base(i))) by arith347  have aboveSucc := realNat.le_of_le with succBound348  have succValue := realNat.succ at base(i)349  rw succValue at aboveSucc350  have same : dist((realNat(u(i)):R) * (dyadicRadius(k):R), (realNat(base(i)):R) * (dyadicRadius(k):R)) = abs((realNat(u(i)):R) * (dyadicRadius(k):R) - (realNat(base(i)):R) * (dyadicRadius(k):R))351    unfold dist352    rfl353  rw same354  have expand : (realNat(u(i)):R) * (dyadicRadius(k):R) - (realNat(base(i)):R) * (dyadicRadius(k):R) = (dyadicRadius(k):R) * ((realNat(u(i)):R) - (realNat(base(i)):R))355    ring356  rw expand357  have gapNonneg : (0:R) ≤ (realNat(u(i)):R) - (realNat(base(i)):R) by linarith358  have gapLe : (realNat(u(i)):R) - (realNat(base(i)):R) ≤ (1:R) by linarith359  have productNonneg : (0:R) ≤ (dyadicRadius(k):R) * ((realNat(u(i)):R) - (realNat(base(i)):R))360    have step := realLe.mul_left_of_nonnegative with gapNonneg, dNonneg361    have zero := realMulValue.zero_right at dyadicRadius(k)362    rwa zero at step363  have absValue := abs.of_nonnegative with productNonneg364  rw absValue365  have step := realLe.mul_left_of_nonnegative with gapLe, dNonneg366  have one := realMulValue.one_right at dyadicRadius(k)367  rwa one at step368