-- Grouping weighted finite sums by their index map (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Ring.WeightedRegrouping
import Regrouping
import FiniteLinearity

section Rings
variable (D C A add zero neg mul one h w t a v : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis ring : IsCommRing(R)
hypothesis finiteD : Finite(D)
hypothesis finiteC : Finite(C)
hypothesis indexMap : h : D → C
hypothesis weights : w : D → A
hypothesis terms : t : D → A
hypothesis scalars : a : C → A
hypothesis outputs : v : C → A
hypothesis factors : ∀ d ∈ D, t(d) = a(h(d)) * w(d)
hypothesis values : ∀ c ∈ C, v(c) = a(c) * finitePushforward(D, C, A, add, zero, neg, mul, one, h, w)(c)

theorem finitePushforward.weighted_sum
  shows finiteRingSum(D, R, t) = finiteRingSum(C, R, v)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have grouped := finitePushforward.function at D, C, A, add, zero, neg, mul, one, h, t with *
  have equations : ∀ c ∈ C, finitePushforward(D, C, A, add, zero, neg, mul, one, h, t)(c) = v(c)
    intros c hc
    have scalar := FunctionBetween.apply_closed at a, C, A, c with *
    have selectedW := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, w, c with *
    have selectedT := pushforwardWeights.function at D, A, add, zero, neg, mul, one, h, t, c with *
    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)
      intros d hd
      have wIn := FunctionBetween.apply_closed at w, D, A, d with *
      have tIn := FunctionBetween.apply_closed at t, D, A, d with *
      have left := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, t, c, d with *
      have right := pushforwardWeights.value at D, A, add, zero, neg, mul, one, h, w, c, d with *
      have alternatives : c = h(d) ∨ c ≠ h(d) by tauto
      cases alternatives with same | different
      . have selectedLeft := singleValue.same at A, zero, t(d), h(d), c with *
        have selectedRight := singleValue.same at A, zero, w(d), h(d), c with *
        have factor := factors with d, hd
        cc
      . have selectedLeft := singleValue.other at A, zero, t(d), h(d), c with *
        have selectedRight := singleValue.other at A, zero, w(d), h(d), c with *
        rw [left, right, selectedLeft, selectedRight]
        ring
    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 *
    have left := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, t, c with *
    have right := finitePushforward.value at D, C, A, add, zero, neg, mul, one, h, w, c with *
    have output := values with c, hc
    cc
  have groupedSum := finitePushforward.sum at D, C, A, add, zero, neg, mul, one, h, t with *
  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 *
  cc

end Rings