Grace/Cumulus/Cardinal/IndicatorSum.g17

Open in Workbench Download source

Imports

NaturalSum · Set.Indicator

Declarations

Source

1-- The sum of an indicator over a finite set counts the members it marks2-- 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.Cardinal.IndicatorSum8import NaturalSum9import Set.Indicator1011defgraph indicatorMap (A V : Set) (v ∈ V) : ℕ := indicator(A, v)12proof13  have natural := indicator.natural at A, v14  exact nat.omega.forward with natural1516theorem indicatorMap.natural (A V : Set)17  shows ∀ v ∈ V, indicatorMap(A, V)(v) ∈ ℕ18proof19  intros v hv20  rw indicatorMap.value with hv21  exact nat.omega.forward with (indicator.natural at A, v)2223-- Meeting a point counts it exactly when the point is a member.24theorem cardinality.intersection_singleton (X a : Set)25  shows cardinality(X ∩ {a}) = indicator(X, a)26proof27  by_cases member : a ∈ X28  . have same : X ∩ {a} = {a}29      ext y30      simp31    have one := indicator.member at X, a with member32    rw [same, cardinality.singleton, one]33    rfl34  . have same : X ∩ {a} = ∅35      ext y36      simp37    have zero := indicator.absent at X, a with member38    rw [same, zero]39    exact cardinality.empty4041theorem natSum.indicator_of_size (A : Set, n : Nat)42  shows ∀ V, Finite(V) → cardinality(V) = n → natSum(V, indicatorMap(A, V)) = cardinality(V ∩ A)43proof44  induction n45  | zero =>46    intros V finite size47    have has := cardinality.correct with finite48    rw size at has49    have empty := HasCardinality.empty_of_zero at V with has50    rw [empty, natSum.empty, intersection.left_empty]51    rw ← nat.zero52    rw cardinality.natural53    rfl54  | succ(k) using ih =>55    intros V finite size56    have has := cardinality.correct with finite57    rw size at has58    obtain ⟨a, ha⟩ := HasCardinality.exists_member with has59    have removed := cardinality.remove with finite, ha60    rw size at removed61    have smaller := Naturals.injective.succ with removed62    have restSize : cardinality(V ∖ {a}) = k63      symm64      exact smaller65    have restInside := difference.subset_left at V, {a}66    have restFinite := Finite.subset with finite, restInside67    have rest := ih with V ∖ {a}, restFinite, restSize68    have fresh : ¬a ∈ V ∖ {a}69      intro inside70      have parts := difference.singleton_membership.forward with inside71      apply parts.right72      rfl73    have restore := insert.restore with ha74    have graph := indicatorMap.function at A, V75    have restGraph := indicatorMap.function at A, V ∖ {a}76    have weights : ∀ v ∈ V ∖ {a}, indicatorMap(A, V)(v) ∈ ℕ77      intros v hv78      exact FunctionBetween.apply_closed with graph, (restInside with v, hv)79    have weightA := FunctionBetween.apply_closed with graph, ha80    have agree : ∀ v ∈ V ∖ {a}, indicatorMap(A, V ∖ {a})(v) = indicatorMap(A, V)(v)81      intros v hv82      have valueRest := indicatorMap.value at A, V ∖ {a}, v with hv83      have value := indicatorMap.value at A, V, v with (restInside with v, hv)84      rw [valueRest, value]85      rfl86    have sameSum := natSum.congr with agree87    have inserted := natSum.insert with restFinite, weights, weightA, fresh88    rw restore at inserted89    have valueA := indicatorMap.value at A, V, a with ha90    have restIntersection := Finite.subset with restFinite, (intersection.subset_left at V ∖ {a}, A)91    have split : a ∈ A ∨ ¬a ∈ A by tauto92    cases split with inA | outA93    . have one := indicator.member with inA94      have decomposition : V ∩ A = insert(a, (V ∖ {a}) ∩ A)95        ext x96        constructor97        . intro hx98          have both := intersection.membership.forward with hx99          have split2 : x = a ∨ x ≠ a by tauto100          apply insert.membership.backward101          cases split2 with same | different102          . left103            exact same104          . right105            have inRest : x ∈ V ∖ {a} := difference.singleton_membership.backward with ⟨both.left, different⟩106            exact intersection.membership.backward with ⟨inRest, both.right⟩107        . intro hx108          have split2 := insert.membership.forward with hx109          apply intersection.membership.backward110          cases split2 with same | inRest111          . rw same112            exact ⟨ha, inA⟩113          . have both := intersection.membership.forward with inRest114            have parts := difference.singleton_membership.forward with both.left115            exact ⟨parts.left, both.right⟩116      have freshIntersection : ¬a ∈ (V ∖ {a}) ∩ A117        intro inside118        have both := intersection.membership.forward with inside119        exact fresh with both.left120      have counted := cardinality.insert with restIntersection, freshIntersection121      rw [inserted, ← sameSum, rest, valueA, one, decomposition, counted]122      have correct := cardinality.correct with restIntersection123      have cardNat := correct.left124      rw add.right_one125      rfl126    . have zero := indicator.absent with outA127      have decomposition : V ∩ A = (V ∖ {a}) ∩ A128        ext x129        constructor130        . intro hx131          have both := intersection.membership.forward with hx132          have different : x ≠ a133            intro same134            rw same at both135            exact outA with both.right136          have inRest : x ∈ V ∖ {a} := difference.singleton_membership.backward with ⟨both.left, different⟩137          exact intersection.membership.backward with ⟨inRest, both.right⟩138        . intro hx139          have both := intersection.membership.forward with hx140          have parts := difference.singleton_membership.forward with both.left141          exact intersection.membership.backward with ⟨parts.left, both.right⟩142      rw [inserted, ← sameSum, rest, valueA, zero, decomposition]143      have correct := cardinality.correct with restIntersection144      have cardNat := correct.left145      rw add.right_unit146      rfl147148149-- The same for a finite set, with no size parameter.150theorem natSum.indicator (V A : Set)151  requires finite : Finite(V)152  shows natSum(V, indicatorMap(A, V)) = cardinality(V ∩ A)153proof154  have correct := cardinality.correct with finite155  have natural := correct.left156  have size : cardinality(V) = cardinality(V) by rfl157  exact natSum.indicator_of_size at A, cardinality(V)158    with natural, V, finite, size159160