Grace/Cumulus/Algebra/Ring/WeightedRegrouping.g17

Open in Workbench Download source

Imports

Regrouping · FiniteLinearity

Declarations

• finitePushforward.weighted_sum theorem derivation

Source

1-- Grouping weighted finite sums by their index map (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Ring.WeightedRegrouping8import Regrouping9import FiniteLinearity1011section Rings12variable (D C A add zero neg mul one h w t a v : Set)13notation ring R := (A, add, zero, neg, mul, one)14hypothesis ring : IsCommRing(R)15hypothesis finiteD : Finite(D)16hypothesis finiteC : Finite(C)17hypothesis indexMap : h : D → C18hypothesis weights : w : D → A19hypothesis terms : t : D → A20hypothesis scalars : a : C → A21hypothesis outputs : v : C → A22hypothesis factors : ∀ d ∈ D, t(d) = a(h(d)) * w(d)23hypothesis values : ∀ c ∈ C, v(c) = a(c) * finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)(c)2425theorem finitePushforward.weighted_sum26  shows finiteRingSum(D, R, t) = finiteRingSum(C, R, v)27proof28  have ordinary := IsCommRing.ring with ring29  have zeroIn := IsRing.zero_in_carrier with ordinary30  have grouped := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, t with *31  have equations : ∀ c ∈ C, finitePushforward(D, C, A, add, zero, neg, mul, one, h, t)(c) = v(c)32    intros c hc33    have scalar := FunctionBetween.apply_closed at a, C, A, c with *34    have selectedW := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *35    have selectedT := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, t, c with *36    have pointwise : ∀ d ∈ D, pushforwardWeights(D, A, add, zero, neg, mul, one, h, t, c)(d) = a(c) * pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c)(d)37      intros d hd38      have wIn := FunctionBetween.apply_closed at w, D, A, d with *39      have tIn := FunctionBetween.apply_closed at t, D, A, d with *40      have left := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, t, c, d with *41      have right := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *42      have alternatives : c = h(d) ∨ c ≠ h(d) by tauto43      cases alternatives with same | different44      . have selectedLeft := singleValue.same at A, zero, t(d), h(d), c with *45        have selectedRight := singleValue.same at A, zero, w(d), h(d), c with *46        have factor := factors with d, hd47        cc48      . have selectedLeft := singleValue.other at A, zero, t(d), h(d), c with *49        have selectedRight := singleValue.other at A, zero, w(d), h(d), c with *50        rw [left, right, selectedLeft, selectedRight]51        ring52    have scale := finiteRingSum.scale_eq at D, A, add, zero, neg, mul, one, pushforwardWeights(D, A, add, zero, neg, mul, one, h, w, c), pushforwardWeights(D, A, add, zero, neg, mul, one, h, t, c), a(c) with *53    have left := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, t, c with *54    have right := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *55    have output := values with c, hc56    cc57  have groupedSum := finitePushforward.sum at D, C, A, add, zero, neg, mul, one, h, t with *58  have equal := finiteRingSum.congr at C, A, add, zero, neg, mul, one, finitePushforward(D, C, A, add, zero, neg, mul, one, h, t), v with *59  cc6061end Rings62