Grace/Cumulus/FixedPoint/WeightedSums.g17

Open in Workbench Download source

Imports

BlockSums

Declarations

Source

1-- Block sums of a family of cube functions: continuity, nonnegativity, the2-- bound of a sum by any of its terms, sums of vanishing terms, and how the3-- block sum of a point changes when a common real shift is scaled4-- 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.WeightedSums10import BlockSums1112-- Sums over the first m coordinates of S of the values W(i)(x).13defgraph prefixWeighted (n S W m : Set) (x ∈ unitCube(n)) : ℝ := realPartialSum(maskedPoint(n, S, assembledPoint(n, W, x)), m)14requires nNat : Nat(n)15requires mNat : Nat(m)16requires functions : ∀ i ∈ n, CubeFunction(W(i), n)17proof18  have values := assembledPoint.function at n, W, x with functions, member19  have sequence := maskedPoint.sequence at n, S, assembledPoint(n, W, x) with values20  exact realPartialSum.real at maskedPoint(n, S, assembledPoint(n, W, x)), m with sequence2122theorem prefixWeighted.continuous (n : Nat) (S W : Set) (m : Nat)23  requires family : ∀ i ∈ n, CubeFunctionContinuous(W(i), n)24  shows m ∈ succ(n) → CubeFunctionContinuous(prefixWeighted(n, S, W, m), n)25proof26  induction m27  | zero =>28    intro hm29    have functions : ∀ i ∈ n, CubeFunction(W(i), n)30      intros i hi31      exact CubeFunctionContinuous.function with (family with hi)32    have zeroIn : (0:R) ∈ ℝ by typecheck33    have constant := constantCube.continuous at n, (0:R) with zeroIn34    have function : CubeFunction(prefixWeighted(n, S, W, 0), n)35      exact prefixWeighted.function at n, S, W, 0 with *36    apply CubeFunctionContinuous.congr with function, constant37    intros x hx38    have value := prefixWeighted.value at n, S, W, 0, x with *39    have constantValue := constantFunction.apply at unitCube(n), ℝ, x, (0:R) with hx, zeroIn40    rw [value, constantValue]41    exact realPartialSum.zero at maskedPoint(n, S, assembledPoint(n, W, x))42  | succ(j) using ih =>43    intro hm44    have functions : ∀ i ∈ n, CubeFunction(W(i), n)45      intros i hi46      exact CubeFunctionContinuous.function with (family with hi)47    have jNat : Nat(j) by typecheck48    have jIn : j ∈ succ(n)49      have less := Less.of_membership with hm50      have below : j < succ(n) by arith51      exact membership.of_Less with below52    have jInN : j ∈ n53      have less := Less.of_membership with hm54      have below : j < n by arith55      exact membership.of_Less with below56    have previous := ih with jIn57    have weightNat := indicator.natural at S, j58    have weightReal := realNat.real at indicator(S, j)59    have weightIn : (realNat(indicator(S, j)):R) ∈ ℝ by typecheck60    have constant := constantCube.continuous at n, (realNat(indicator(S, j)):R) with weightIn61    have component := family with jInN62    have term := mulCube.continuous with constant, component63    have total := addCube.continuous with previous, term64    have function : CubeFunction(prefixWeighted(n, S, W, succ(j)), n)65      exact prefixWeighted.function at n, S, W, succ(j) with *66    apply CubeFunctionContinuous.congr with function, total67    intros x hx68    have values := assembledPoint.function at n, W, x with functions, hx69    have previousFunction := CubeFunctionContinuous.function with previous70    have termFunction := CubeFunctionContinuous.function with term71    have constantFunction2 := CubeFunctionContinuous.function with constant72    have componentFunction := CubeFunctionContinuous.function with component73    have value := prefixWeighted.value at n, S, W, succ(j), x with *74    have previousValue := prefixWeighted.value at n, S, W, j, x with *75    have sumValue := addCube.value at n, prefixWeighted(n, S, W, j), mulCube(n, constantFunction(unitCube(n), ℝ, (realNat(indicator(S, j)):R)), W(j)), x with previousFunction, termFunction, hx76    have termValue := mulCube.value at n, constantFunction(unitCube(n), ℝ, (realNat(indicator(S, j)):R)), W(j), x with constantFunction2, componentFunction, hx77    have constantValue := constantFunction.apply at unitCube(n), ℝ, x, (realNat(indicator(S, j)):R) with hx, weightIn78    have componentValue := assembledPoint.value at n, W, x, j with functions, hx, jInN79    have step := realPartialSum.succ at maskedPoint(n, S, assembledPoint(n, W, x)), j80    have masked := maskedPoint.coordinate at n, S, assembledPoint(n, W, x), j with values, jInN81    have sequence := maskedPoint.sequence at n, S, assembledPoint(n, W, x) with values82    have componentReal := CubeFunction.value with componentFunction, hx83    rw [value, sumValue, previousValue, termValue, constantValue, step, masked, componentValue]84    linarith8586-- The block sum of the family over S.87def weightedSum (n S W : Set) : Set := prefixWeighted(n, S, W, n)8889theorem weightedSum.definition (n S W : Set)90  shows weightedSum(n, S, W) = prefixWeighted(n, S, W, n)91proof92  unfold weightedSum93  rfl9495theorem weightedSum.continuous (n : Nat) (S W : Set)96  requires family : ∀ i ∈ n, CubeFunctionContinuous(W(i), n)97  shows CubeFunctionContinuous(weightedSum(n, S, W), n)98proof99  have all := prefixWeighted.continuous at n, S, W, n with family100  have same := weightedSum.definition at n, S, W101  rw same102  exact all with (bootstrap.succ.self at n)103104theorem weightedSum.function (n : Nat) (S W : Set)105  requires functions : ∀ i ∈ n, CubeFunction(W(i), n)106  shows CubeFunction(weightedSum(n, S, W), n)107proof108  have same := weightedSum.definition at n, S, W109  rw same110  exact prefixWeighted.function at n, S, W, n with *111112theorem weightedSum.value (n : Nat) (S W x : Set)113  requires functions : ∀ i ∈ n, CubeFunction(W(i), n)114  requires hx : x ∈ unitCube(n)115  shows weightedSum(n, S, W)(x) = realPartialSum(maskedPoint(n, S, assembledPoint(n, W, x)), n)116proof117  have same := weightedSum.definition at n, S, W118  rw same119  exact prefixWeighted.value at n, S, W, n, x with *120121theorem weightedSum.real (n : Nat) (S W x : Set)122  requires functions : ∀ i ∈ n, CubeFunction(W(i), n)123  requires hx : x ∈ unitCube(n)124  shows weightedSum(n, S, W)(x) ∈ ℝ125proof126  exact CubeFunction.value with (weightedSum.function at n, S, W with functions), hx127128-- Masked terms of a nonnegative family are nonnegative.129theorem maskedPoint.nonnegative_of (n : Nat) (S w k : Set)130  requires wFunction : w : n → ℝ131  requires hk : k ∈ n132  requires nonnegative : (0:R) ≤ (w(k):R)133  shows (0:R) ≤ (maskedPoint(n, S, w)(k):R)134proof135  have alternatives : k ∈ S ∨ ¬k ∈ S by tauto136  cases alternatives with inBlock | outside137  . have same := maskedPoint.on_block with wFunction, hk, inBlock138    rwa same139  . have same := maskedPoint.off_block with wFunction, hk, outside140    rw same141    linarith142143theorem weightedSum.terms_nonnegative (n : Nat) (S W x : Set)144  requires functions : ∀ i ∈ n, CubeFunction(W(i), n)145  requires hx : x ∈ unitCube(n)146  requires nonnegative : ∀ i ∈ n, (0:R) ≤ (W(i)(x):R)147  shows ∀ k ∈ n, (0:R) ≤ (maskedPoint(n, S, assembledPoint(n, W, x))(k):R)148proof149  intros k hk150  have values := assembledPoint.function with functions, hx151  have value := assembledPoint.value with functions, hx, hk152  have bound := nonnegative with hk153  have termNonneg : (0:R) ≤ (assembledPoint(n, W, x)(k):R) by rwa value154  exact maskedPoint.nonnegative_of with values, hk, termNonneg155156theorem weightedSum.nonnegative (n : Nat) (S W x : Set)157  requires functions : ∀ i ∈ n, CubeFunction(W(i), n)158  requires hx : x ∈ unitCube(n)159  requires nonnegative : ∀ i ∈ n, (0:R) ≤ (W(i)(x):R)160  shows (0:R) ≤ (weightedSum(n, S, W)(x):R)161proof162  have values := assembledPoint.function with functions, hx163  have sequence := maskedPoint.sequence at n, S, assembledPoint(n, W, x) with values164  have value := weightedSum.value at n, S, W, x with functions, hx165  have terms := weightedSum.terms_nonnegative at n, S, W, x with functions, hx, nonnegative166  have bound := realPartialSum.nonnegative_prefix with sequence167  rw value168  exact bound with terms169170theorem weightedSum.ge_term (n : Nat) (S W x j : Set)171  requires functions : ∀ i ∈ n, CubeFunction(W(i), n)172  requires hx : x ∈ unitCube(n)173  requires nonnegative : ∀ i ∈ n, (0:R) ≤ (W(i)(x):R)174  requires hj : j ∈ n175  requires inBlock : j ∈ S176  shows (W(j)(x):R) ≤ (weightedSum(n, S, W)(x):R)177proof178  have values := assembledPoint.function with functions, hx179  have sequence := maskedPoint.sequence at n, S, assembledPoint(n, W, x) with values180  have value := weightedSum.value at n, S, W, x with functions, hx181  have terms := weightedSum.terms_nonnegative at n, S, W, x with functions, hx, nonnegative182  have bounds := realPartialSum.term_le_prefix with sequence183  have forAll := bounds with terms184  have bound := forAll with hj185  have same := maskedPoint.on_block with values, hj, inBlock186  have component := assembledPoint.value with functions, hx, hj187  rw value188  rwa [same, component] at bound189190-- A partial sum of vanishing terms vanishes.191theorem realPartialSum.zero_terms (u : Set) (m : Nat)192  requires sequence : RealSequence(u)193  shows (∀ k ∈ m, u(k) = (0:R)) → realPartialSum(u, m) = (0:R)194proof195  induction m196  | zero =>197    intro terms198    exact realPartialSum.zero at u199  | succ(j) using ih =>200    intro terms201    have jNat : Nat(j) by typecheck202    have last := terms with (bootstrap.succ.self at j)203    have smaller : ∀ k ∈ j, u(k) = (0:R)204      intros k hk205      have kNat := natural.member at j with hk206      have less := Less.of_membership with hk207      have below : k < succ(j) by arith208      have inSucc : k ∈ succ(j)209        exact membership.of_Less with below210      exact terms with inSucc211    have previous := ih with smaller212    have step := realPartialSum.succ at u, j213    have lastReal := RealSequence.value at u, j with sequence214    rw step215    linarith216217-- When the selected coordinates of z are those of x shifted by a real218-- function w and scaled by C, so is the block sum.219theorem sumCube.scaled_sum (n : Nat) (S x z w : Set) (C : Real)220  requires hx : x ∈ unitCube(n)221  requires hz : z ∈ unitCube(n)222  requires wFunction : w : n → ℝ223  requires shifted : ∀ j ∈ n, j ∈ S → z(j) = ((x(j):R) + (w(j):R)) * C224  shows sumCube(n, S)(z) = ((sumCube(n, S)(x):R) + (realPartialSum(maskedPoint(n, S, w), n):R)) * C225proof226  have xFunction := unitCube.point with hx227  have zFunction := unitCube.point with hz228  have maskedX := maskedPoint.sequence at n, S, x with xFunction229  have maskedW := maskedPoint.sequence at n, S, w with wFunction230  have maskedZ := maskedPoint.sequence at n, S, z with zFunction231  have constantC := constantSequence.sequence at C232  have inner := addSequence.sequence with maskedX, maskedW233  have agree : ∀ k ∈ ℕ, k < n → maskedPoint(n, S, z)(k) = mulSequence(constantSequence(C), addSequence(maskedPoint(n, S, x), maskedPoint(n, S, w)))(k)234    intros k hk hkn235    have kNat : Nat(k) by typecheck236    have hkIn : k ∈ n by exact membership.of_Less with hkn237    have xReal := RealSequence.value at maskedPoint(n, S, x), k with maskedX238    have wReal := RealSequence.value at maskedPoint(n, S, w), k with maskedW239    have cReal := RealSequence.value at constantSequence(C), k with constantC240    have cValue := constantSequence.value at C, k241    have innerValue := addSequence.value with maskedX, maskedW, xReal, wReal242    have innerReal := RealSequence.value at addSequence(maskedPoint(n, S, x), maskedPoint(n, S, w)), k with inner243    have outerValue := mulSequence.value with constantC, inner, cReal, innerReal244    rw [outerValue, innerValue, cValue]245    have alternatives : k ∈ S ∨ ¬k ∈ S by tauto246    cases alternatives with inBlock | outside247    . have zSame := maskedPoint.on_block with zFunction, hkIn, inBlock248      have xSame := maskedPoint.on_block with xFunction, hkIn, inBlock249      have wSame := maskedPoint.on_block with wFunction, hkIn, inBlock250      have zValue := shifted with hkIn, inBlock251      have xk := unitCube.coordinate_real with hx, hkIn252      have wk := FunctionBetween.apply_closed with wFunction, hkIn253      rw [zSame, xSame, wSame, zValue]254      ring255    . have zSame := maskedPoint.off_block with zFunction, hkIn, outside256      have xSame := maskedPoint.off_block with xFunction, hkIn, outside257      have wSame := maskedPoint.off_block with wFunction, hkIn, outside258      rw [zSame, xSame, wSame]259      ring260  have outer := mulSequence.sequence with constantC, inner261  have equal := realPartialSum.eq_prefix with maskedZ, outer, agree262  have scaleC := realPartialSum.scale with inner263  have addXW := realPartialSum.add with maskedX, maskedW264  have zValue := sumCube.value at n, S, z with hz265  have xValue := sumCube.value at n, S, x with hx266  rw [zValue, xValue, equal, scaleC, addXW]267  ring268