Grace/Cumulus/Combinatorics/IntegerSum.g17

Open in Workbench Download source

Imports

Int · Algebra.Ring.WeightedRegrouping · Cardinal

Declarations

Source

1-- Integer-valued sums over finite sets: the canonical commutative ring sum2-- of ℤ over a finite index set, with closure, the singleton sum,3-- congruence, vanishing, restriction to a support, reindexing along a4-- bijection, and scaling by an integer5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Combinatorics.IntegerSum11import Int12import Algebra.Ring.WeightedRegrouping13import Cardinal1415-- The sum of an integer-valued weight over a finite set, as the canonical16-- commutative ring sum of the integers.17def integerSetSum (V w : Set) : Set :=18  finiteRingSum(V, ℤ, integerAdd, integerZero, integerNeg, integerMul,19    integerOne, restrict(w, V))2021theorem integerSetSum.integer (V Ω w : Set)22  requires finite : Finite(V)23  requires weights : w : Ω → ℤ24  requires subset : V ⊆ Ω25  shows Integer(integerSetSum(V, w))26proof27  have ring := integers.comm_ring28  have restricted := restrict.domain_function with weights, subset29  have closed := finiteRingSum.closed with ring, finite, restricted30  unfold integerSetSum31  exact closed3233theorem integerSetSum.singleton (Ω w a : Set)34  requires weights : w : Ω → ℤ35  requires member : a ∈ Ω36  shows integerSetSum({a}, w) = w(a)37proof38  have ring := integers.comm_ring39  have subset : {a} ⊆ Ω by simp40  have self : a ∈ {a} by simp41  have restricted := restrict.domain_function with weights, subset42  have sum := finiteRingSum.singleton with ring, restricted43  have value := restrict.domain_apply with weights, subset, self44  unfold integerSetSum45  cc4647theorem integerSetSum.congr (V Ω w v : Set)48  requires weightsW : w : Ω → ℤ49  requires weightsV : v : Ω → ℤ50  requires subset : V ⊆ Ω51  requires values : ∀ x ∈ V, w(x) = v(x)52  shows integerSetSum(V, w) = integerSetSum(V, v)53proof54  have restrictedW := restrict.domain_function with weightsW, subset55  have restrictedV := restrict.domain_function with weightsV, subset56  have same : ∀ x ∈ V, restrict(w, V)(x) = restrict(v, V)(x)57    intros x hx58    have left := restrict.domain_apply with weightsW, subset, hx59    have right := restrict.domain_apply with weightsV, subset, hx60    have equal := values with x, hx61    cc62  have equal := FunctionBetween.ext with restrictedW, restrictedV, same63  unfold integerSetSum64  cc6566theorem integerSetSum.zero (V Ω w : Set)67  requires finite : Finite(V)68  requires weights : w : Ω → ℤ69  requires subset : V ⊆ Ω70  requires values : ∀ x ∈ V, w(x) = integerZero71  shows integerSetSum(V, w) = integerZero72proof73  have ring := integers.comm_ring74  have restricted := restrict.domain_function with weights, subset75  have vanishing : ∀ x ∈ V, restrict(w, V)(x) = integerZero76    intros x hx77    have value := restrict.domain_apply with weights, subset, hx78    have zero := values with x, hx79    cc80  have sum := finiteRingSum.zero with ring, finite, restricted, vanishing81  unfold integerSetSum82  cc8384-- A sum shrinks to any subset outside of which its weight vanishes.85theorem integerSetSum.support (V S Ω w : Set)86  requires finite : Finite(V)87  requires weights : w : Ω → ℤ88  requires subset : V ⊆ Ω89  requires inner : S ⊆ V90  requires vanishes : ∀ x ∈ V, ¬(x ∈ S) → w(x) = integerZero91  shows integerSetSum(V, w) = integerSetSum(S, w)92proof93  have ring := integers.comm_ring94  have restricted := restrict.domain_function with weights, subset95  have vanishing : ∀ x ∈ V, ¬(x ∈ S) → restrict(w, V)(x) = integerZero96    intros x hx outside97    have value := restrict.domain_apply with weights, subset, hx98    have zero := vanishes with x, hx, outside99    cc100  have sum := finiteRingSum.restrict at V, S, ℤ, integerAdd, integerZero,101    integerNeg, integerMul, integerOne, restrict(w, V) with ring, finite,102      restricted, inner, vanishing103  have nested := restrict.nested at w, S, V with inner104  unfold integerSetSum105  cc106107-- A bijection between index sets carrying one weight to the other108-- identifies the two sums.109theorem integerSetSum.reindex (D E ΩD ΩE w v f : Set)110  requires finite : Finite(D)111  requires weightsW : w : ΩD → ℤ112  requires weightsV : v : ΩE → ℤ113  requires subsetD : D ⊆ ΩD114  requires subsetE : E ⊆ ΩE115  requires bijective : BijectiveBetween(f, D, E)116  requires values : ∀ d ∈ D, w(d) = v(f(d))117  shows integerSetSum(D, w) = integerSetSum(E, v)118proof119  have ring := integers.comm_ring120  have restrictedW := restrict.domain_function with weightsW, subsetD121  have restrictedV := restrict.domain_function with weightsV, subsetE122  have injective := Bijective.injective with bijective123  have function := Injective.function with injective124  have agree : ∀ d ∈ D, restrict(w, D)(d) = restrict(v, E)(f(d))125    intros d hd126    have image := FunctionBetween.apply_closed with function, hd127    have left := restrict.domain_apply with weightsW, subsetD, hd128    have right := restrict.domain_apply with weightsV, subsetE, image129    have equal := values with d, hd130    cc131  have sum := finiteRingSum.reindex with ring, finite, restrictedW,132    restrictedV, bijective, agree133  unfold integerSetSum134  cc135136theorem integerSetSum.scale (V Ω w v : Set) (a : Integer)137  requires finite : Finite(V)138  requires weightsW : w : Ω → ℤ139  requires weightsV : v : Ω → ℤ140  requires subset : V ⊆ Ω141  requires values : ∀ x ∈ V, v(x) = integerMulValue(a, w(x))142  shows integerSetSum(V, v) = integerMulValue(a, integerSetSum(V, w))143proof144  have ring := integers.comm_ring145  have scalar : a ∈ ℤ by simp [Integer]146  have restrictedW := restrict.domain_function with weightsW, subset147  have restrictedV := restrict.domain_function with weightsV, subset148  have entries : ∀ x ∈ V, restrict(v, V)(x) =149      call2(integerMul, a, restrict(w, V)(x))150    intros x hx151    have left := restrict.domain_apply with weightsV, subset, hx152    have right := restrict.domain_apply with weightsW, subset, hx153    have inDomain := subset with x, hx154    have valueW := FunctionBetween.apply_closed with weightsW, inDomain155    have equal := values with x, hx156    have bridge := integerMulValue.notation at a, w(x) with *157    cc158  have sum := finiteRingSum.scale_eq with ring, finite, restrictedW,159    restrictedV, scalar, entries160  have total := integerSetSum.integer with finite, weightsW, subset161  have bridge := integerMulValue.notation at a, integerSetSum(V, w) with *162  unfold integerSetSum at bridge163  unfold integerSetSum164  cc165