Grace/Cumulus/FixedPoint/BlockSums.g17

Open in Workbench Download source

Imports

CubeAssembly

Declarations

Source

1-- Block sums of a point of the cube: each term is the coordinate or zero,2-- the sum is nonnegative and at least any selected coordinate, and it3-- transforms linearly under a common affine change of the selected coordinates4-- 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.BlockSums10import CubeAssembly1112-- A masked term is the coordinate on the block and zero off it.13theorem maskedPoint.on_block (n : Nat) (S x i : Set)14  requires xFunction : x : n → ℝ15  requires hi : i ∈ n16  requires inBlock : i ∈ S17  shows maskedPoint(n, S, x)(i) = x(i)18proof19  have value := maskedPoint.coordinate at n, S, x, i with xFunction, hi20  have one := indicator.member with inBlock21  have xi := FunctionBetween.apply_closed with xFunction, hi22  rw [value, one, realNat.one]23  exact realMulValue.one_left2425theorem maskedPoint.off_block (n : Nat) (S x i : Set)26  requires xFunction : x : n → ℝ27  requires hi : i ∈ n28  requires outside : ¬i ∈ S29  shows maskedPoint(n, S, x)(i) = (0:R)30proof31  have value := maskedPoint.coordinate at n, S, x, i with xFunction, hi32  have zero := indicator.absent with outside33  have xi := FunctionBetween.apply_closed with xFunction, hi34  rw [value, zero, realNat.zero]35  exact realMulValue.zero_left3637theorem maskedPoint.nonnegative (n : Nat) (S x i : Set)38  requires hx : x ∈ unitCube(n)39  requires hi : i ∈ n40  shows (0:R) ≤ (maskedPoint(n, S, x)(i):R)41proof42  have xFunction := unitCube.point with hx43  have alternatives : i ∈ S ∨ ¬i ∈ S by tauto44  cases alternatives with inBlock | outside45  . have same := maskedPoint.on_block with xFunction, hi, inBlock46    have interval := unitCube.coordinate with hx, hi47    obtain ⟨xReal, lower, upper⟩ := closedInterval.membership.forward with interval48    rwa same49  . have same := maskedPoint.off_block with xFunction, hi, outside50    rw same51    linarith5253-- Partial sums of nonnegative terms are nonnegative and bound every term.54theorem realPartialSum.nonnegative_prefix (u : Set) (m : Nat)55  requires sequence : RealSequence(u)56  shows (∀ k ∈ m, (0:R) ≤ (u(k):R)) → (0:R) ≤ (realPartialSum(u, m):R)57proof58  induction m59  | zero =>60    intro terms61    have zero := realPartialSum.zero at u62    rw zero63    linarith64  | succ(j) using ih =>65    intro terms66    have jNat : Nat(j) by typecheck67    have last := terms with (bootstrap.succ.self at j)68    have smaller : ∀ k ∈ j, (0:R) ≤ (u(k):R)69      intros k hk70      have kNat := natural.member at j with hk71      have less := Less.of_membership with hk72      have below : k < succ(j) by arith73      have inSucc : k ∈ succ(j)74        exact membership.of_Less with below75      exact terms with inSucc76    have previous := ih with smaller77    have step := realPartialSum.succ at u, j78    have lastReal := RealSequence.value at u, j with sequence79    rw step80    linarith8182theorem realPartialSum.term_le_prefix (u : Set) (m : Nat)83  requires sequence : RealSequence(u)84  shows (∀ k ∈ m, (0:R) ≤ (u(k):R)) → ∀ j ∈ m, (u(j):R) ≤ (realPartialSum(u, m):R)85proof86  induction m87  | zero =>88    intros terms j hj89    exfalso90    rw nat.zero at hj91    simpa using hj92  | succ(i) using ih =>93    intros terms j hj94    have iNat : Nat(i) by typecheck95    have smaller : ∀ k ∈ i, (0:R) ≤ (u(k):R)96      intros k hk97      have kNat := natural.member at i with hk98      have less := Less.of_membership with hk99      have below : k < succ(i) by arith100      have inSucc : k ∈ succ(i)101        exact membership.of_Less with below102      exact terms with inSucc103    have nonnegative := realPartialSum.nonnegative_prefix at u, i with sequence104    have prefixNonneg := nonnegative with smaller105    have step := realPartialSum.succ at u, i106    have lastReal := RealSequence.value at u, i with sequence107    have last := terms with (bootstrap.succ.self at i)108    have split := bootstrap.succ.membership.forward with hj109    rw step110    cases split with below | same111    . have bounds := ih with smaller112      have bound := bounds with below113      have jNat := natural.member at i with below114      have jReal := RealSequence.value at u, j with sequence115      linarith116    . rw same117      linarith118119-- Block sums are nonnegative and at least any selected coordinate.120theorem sumCube.terms_nonnegative (n : Nat) (S x : Set)121  requires hx : x ∈ unitCube(n)122  shows ∀ k ∈ n, (0:R) ≤ (maskedPoint(n, S, x)(k):R)123proof124  intros k hk125  exact maskedPoint.nonnegative with hx, hk126127theorem sumCube.nonnegative (n : Nat) (S x : Set)128  requires hx : x ∈ unitCube(n)129  shows (0:R) ≤ (sumCube(n, S)(x):R)130proof131  have xFunction := unitCube.point with hx132  have sequence := maskedPoint.sequence at n, S, x with xFunction133  have value := sumCube.value at n, S, x with hx134  have terms := sumCube.terms_nonnegative at n, S, x with hx135  have bound := realPartialSum.nonnegative_prefix with sequence136  rw value137  exact bound with terms138139theorem sumCube.ge_coordinate (n : Nat) (S x j : Set)140  requires hx : x ∈ unitCube(n)141  requires hj : j ∈ n142  requires inBlock : j ∈ S143  shows (x(j):R) ≤ (sumCube(n, S)(x):R)144proof145  have xFunction := unitCube.point with hx146  have sequence := maskedPoint.sequence at n, S, x with xFunction147  have value := sumCube.value at n, S, x with hx148  have terms := sumCube.terms_nonnegative at n, S, x with hx149  have bounds := realPartialSum.term_le_prefix with sequence150  have forAll := bounds with terms151  have bound := forAll with hj152  have same := maskedPoint.on_block with xFunction, hj, inBlock153  rw value154  rwa same at bound155156-- When the selected coordinates of z are an affine image of those of x and a,157-- the block sum of z is the same affine image of the block sums of x and a.158theorem sumCube.affine (n : Nat) (S x a z : Set) (E C : Real)159  requires hx : x ∈ unitCube(n)160  requires ha : a ∈ unitCube(n)161  requires hz : z ∈ unitCube(n)162  requires shifted : ∀ j ∈ n, j ∈ S → z(j) = ((x(j):R) + E * (a(j):R)) * C163  shows sumCube(n, S)(z) = ((sumCube(n, S)(x):R) + E * (sumCube(n, S)(a):R)) * C164proof165  have xFunction := unitCube.point with hx166  have aFunction := unitCube.point with ha167  have zFunction := unitCube.point with hz168  have maskedX := maskedPoint.sequence at n, S, x with xFunction169  have maskedA := maskedPoint.sequence at n, S, a with aFunction170  have maskedZ := maskedPoint.sequence at n, S, z with zFunction171  have constantE := constantSequence.sequence at E172  have constantC := constantSequence.sequence at C173  have scaledA := mulSequence.sequence with constantE, maskedA174  have inner := addSequence.sequence with maskedX, scaledA175  have agree : ∀ k ∈ ℕ, k < n → maskedPoint(n, S, z)(k) = mulSequence(constantSequence(C), addSequence(maskedPoint(n, S, x), mulSequence(constantSequence(E), maskedPoint(n, S, a))))(k)176    intros k hk hkn177    have kNat : Nat(k) by typecheck178    have hkIn : k ∈ n by exact membership.of_Less with hkn179    have xReal := RealSequence.value at maskedPoint(n, S, x), k with maskedX180    have aReal := RealSequence.value at maskedPoint(n, S, a), k with maskedA181    have eReal := RealSequence.value at constantSequence(E), k with constantE182    have cReal := RealSequence.value at constantSequence(C), k with constantC183    have eValue := constantSequence.value at E, k184    have cValue := constantSequence.value at C, k185    have scaledValue := mulSequence.value with constantE, maskedA, eReal, aReal186    have scaledReal := RealSequence.value at mulSequence(constantSequence(E), maskedPoint(n, S, a)), k with scaledA187    have innerValue := addSequence.value with maskedX, scaledA, xReal, scaledReal188    have innerReal := RealSequence.value at addSequence(maskedPoint(n, S, x), mulSequence(constantSequence(E), maskedPoint(n, S, a))), k with inner189    have outerValue := mulSequence.value with constantC, inner, cReal, innerReal190    rw [outerValue, innerValue, scaledValue, eValue, cValue]191    have alternatives : k ∈ S ∨ ¬k ∈ S by tauto192    cases alternatives with inBlock | outside193    . have zSame := maskedPoint.on_block with zFunction, hkIn, inBlock194      have xSame := maskedPoint.on_block with xFunction, hkIn, inBlock195      have aSame := maskedPoint.on_block with aFunction, hkIn, inBlock196      have zValue := shifted with hkIn, inBlock197      have xk := unitCube.coordinate_real with hx, hkIn198      have ak := unitCube.coordinate_real with ha, hkIn199      rw [zSame, xSame, aSame, zValue]200      ring201    . have zSame := maskedPoint.off_block with zFunction, hkIn, outside202      have xSame := maskedPoint.off_block with xFunction, hkIn, outside203      have aSame := maskedPoint.off_block with aFunction, hkIn, outside204      rw [zSame, xSame, aSame]205      ring206  have outer := mulSequence.sequence with constantC, inner207  have equal := realPartialSum.eq_prefix with maskedZ, outer, agree208  have scaleC := realPartialSum.scale at addSequence(maskedPoint(n, S, x), mulSequence(constantSequence(E), maskedPoint(n, S, a))), n, C with inner209  have addXA := realPartialSum.add with maskedX, scaledA210  have scaleE := realPartialSum.scale at maskedPoint(n, S, a), n, E with maskedA211  have zValue := sumCube.value at n, S, z with hz212  have xValue := sumCube.value at n, S, x with hx213  have aValue := sumCube.value at n, S, a with ha214  rw [zValue, xValue, aValue, equal, scaleC, addXA, scaleE]215  ring216