Grace/Cumulus/Probability/SetSum.g17

Open in Workbench Download source

Imports

Algebra.Ring.SumSupport · Real.Natural · Cardinal

Declarations

Source

1-- Real-valued sums over finite sets2-- 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.Probability.SetSum8import Algebra.Ring.SumSupport9import Real.Natural10import Cardinal1112-- The sum of a real-valued weight over a finite set, as the canonical13-- commutative ring sum of the reals.14def realSetSum (V w : Set) : Set :=15  finiteRingSum(V, ℝ, realAdd, realZero, realNeg, realMul, realOne, restrict(w,16    V))1718theorem realSetSum.real (V Ω w : Set)19  requires finite : Finite(V)20  requires weights : w : Ω → ℝ21  requires subset : V ⊆ Ω22  shows Real(realSetSum(V, w))23proof24  have ring := reals.comm_ring25  have restricted := restrict.domain_function with weights, subset26  have closed := finiteRingSum.closed with ring, finite, restricted27  unfold realSetSum28  exact closed2930theorem realSetSum.empty (w : Set)31  shows realSetSum(∅, w) = (0:R)32proof33  have ring := reals.comm_ring34  have restricted : restrict(w, ∅) : ∅ → ℝ35    have same := restrict.empty at w36    rw same37    exact FunctionBetween.empty at ℝ38  have sum := finiteRingSum.empty with ring, restricted39  unfold realSetSum40  cc4142-- An enumeration of the index set turns the sum into an indexed sum of the43-- original weight.44theorem realSetSum.enumeration (V Ω w f : Set, n : Nat)45  requires weights : w : Ω → ℝ46  requires subset : V ⊆ Ω47  requires enumeration : BijectiveBetween(f, n, V)48  shows realSetSum(V, w) = indexedRingSum(w, f, realAdd, realZero, n)49proof50  have ring := reals.comm_ring51  have restricted := restrict.domain_function with weights, subset52  have sum := finiteRingSum.enumeration at V, ℝ, realAdd, realZero, realNeg,53    realMul, realOne, restrict(w, V), f, n with ring, restricted, enumeration54  have injective := Bijective.injective with enumeration55  have function := Injective.function with injective56  have values : ∀ i ∈ n, restrict(w, V)(f(i)) = w(f(i))57    intros i hi58    have member := FunctionBetween.apply_closed with function, hi59    exact restrict.domain_apply with weights, subset, member60  have congr := indexedRingSum.congr at restrict(w, V), w, f, f, realAdd,61      realZero, n62  have same := congr with values63  unfold realSetSum64  cc6566theorem realSetSum.weighted_values (V Ω w f : Set, n : Nat)67  requires weights : w : Ω → ℝ68  requires subset : V ⊆ Ω69  requires function : f : n → V70  shows WeightedValues(w, f, ℝ, n)71proof72  intros i hi73  have inV := FunctionBetween.apply_closed with function, hi74  have inDomain := subset with f(i), inV75  exact FunctionBetween.apply_closed with weights, inDomain7677theorem realSetSum.insert (V Ω w a : Set)78  requires finite : Finite(V)79  requires weights : w : Ω → ℝ80  requires subset : V ⊆ Ω81  requires member : a ∈ Ω82  requires fresh : ¬(a ∈ V)83  shows realSetSum(insert(a, V), w) = (realSetSum(V, w):R) + (w(a):R)84proof85  have ring := reals.comm_ring86  have bigger : insert(a, V) ⊆ Ω by simp87  have inner : V ⊆ insert(a, V) by simp88  have selfMember : a ∈ insert(a, V) by simp89  have restricted := restrict.domain_function with weights, bigger90  have inserted := finiteRingSum.insert with ring, finite, restricted, fresh91  have nested := restrict.nested at w, V, insert(a, V) with inner92  have value := restrict.domain_apply with weights, bigger, selfMember93  unfold realSetSum94  cc9596theorem realSetSum.singleton (Ω w a : Set)97  requires weights : w : Ω → ℝ98  requires member : a ∈ Ω99  shows realSetSum({a}, w) = w(a)100proof101  have same : insert(a, ∅) = {a}102    ext y103    simp104  have finite := Finite.empty105  have subset := empty.subset at Ω106  have fresh := set.empty at a107  have inserted := realSetSum.insert with finite, weights, subset, member, fresh108  have emptySum := realSetSum.empty at w109  have value := FunctionBetween.apply_closed with weights, member110  rw same at inserted111  rw [inserted, emptySum]112  ring113114theorem realSetSum.congr (V Ω w v : Set)115  requires weightsW : w : Ω → ℝ116  requires weightsV : v : Ω → ℝ117  requires subset : V ⊆ Ω118  requires values : ∀ x ∈ V, w(x) = v(x)119  shows realSetSum(V, w) = realSetSum(V, v)120proof121  have restrictedW := restrict.domain_function with weightsW, subset122  have restrictedV := restrict.domain_function with weightsV, subset123  have same : ∀ x ∈ V, restrict(w, V)(x) = restrict(v, V)(x)124    intros x hx125    have left := restrict.domain_apply with weightsW, subset, hx126    have right := restrict.domain_apply with weightsV, subset, hx127    have equal := values with x, hx128    cc129  have equal := FunctionBetween.ext with restrictedW, restrictedV, same130  unfold realSetSum131  cc132133theorem realSetSum.zero (V Ω w : Set)134  requires finite : Finite(V)135  requires weights : w : Ω → ℝ136  requires subset : V ⊆ Ω137  requires values : ∀ x ∈ V, w(x) = (0:R)138  shows realSetSum(V, w) = (0:R)139proof140  have ring := reals.comm_ring141  have restricted := restrict.domain_function with weights, subset142  have vanishing : ∀ x ∈ V, restrict(w, V)(x) = realZero143    intros x hx144    have value := restrict.domain_apply with weights, subset, hx145    have zero := values with x, hx146    cc147  have sum := finiteRingSum.zero with ring, finite, restricted, vanishing148  unfold realSetSum149  cc150151-- Indexed real sums of nonnegative terms are nonnegative.152theorem indexedRingSum.real_nonnegative (w f : Set, n : Nat)153  shows WeightedValues(w, f, ℝ, n) → (∀ i ∈ n, (0:R) ≤ (w(f(i)):R)) →154    (0:R) ≤ (indexedRingSum(w, f, realAdd, realZero, n):R)155proof156  induction n157  | zero =>158    intros values bounds159    rw indexedRingSum160    exact realLe.reflexive with realZero.real161  | succ(k) using ih =>162    intros values bounds163    have ring := reals.comm_ring164    have prefix := WeightedValues.prefix at w, f, ℝ, k with values165    have last := WeightedValues.last at w, f, ℝ, k with values166    have prefixBounds : ∀ i ∈ k, (0:R) ≤ (w(f(i)):R)167      intros i hi168      have next := membership.into_successor at i, k with *169      exact bounds with i, next170    have lastBound := bounds with k, membership.self_successor at k with *171    have previous := ih with prefix, prefixBounds172    have closure := indexedRingSum.closed at ℝ, realAdd, realZero, realNeg,173      realMul, realOne, w, f, k with ring174    have sumReal := closure with prefix175    rw indexedRingSum176    linarith177178theorem realSetSum.nonnegative (V Ω w : Set)179  requires finite : Finite(V)180  requires weights : w : Ω → ℝ181  requires subset : V ⊆ Ω182  requires bounds : ∀ x ∈ V, (0:R) ≤ (w(x):R)183  shows (0:R) ≤ (realSetSum(V, w):R)184proof185  obtain ⟨n, natural, f, enumeration⟩ := Finite.enumeration with finite186  have injective := Bijective.injective with enumeration187  have function := Injective.function with injective188  have sum := realSetSum.enumeration with weights, subset, enumeration189  have values := realSetSum.weighted_values with weights, subset, function190  have indexBounds : ∀ i ∈ n, (0:R) ≤ (w(f(i)):R)191    intros i hi192    have member := FunctionBetween.apply_closed with function, hi193    exact bounds with f(i), member194  have nonnegative := indexedRingSum.real_nonnegative at w, f, n195  rw sum196  exact nonnegative with values, indexBounds197198theorem indexedRingSum.real_monotone (w v f : Set, n : Nat)199  shows WeightedValues(w, f, ℝ, n) → WeightedValues(v, f, ℝ, n) →200    (∀ i ∈ n, (w(f(i)):R) ≤ (v(f(i)):R)) →201    (indexedRingSum(w, f, realAdd, realZero, n):R) ≤202      (indexedRingSum(v, f, realAdd, realZero, n):R)203proof204  induction n205  | zero =>206    intros valuesW valuesV bounds207    rw [indexedRingSum, indexedRingSum]208    exact realLe.reflexive with realZero.real209  | succ(k) using ih =>210    intros valuesW valuesV bounds211    have ring := reals.comm_ring212    have prefixW := WeightedValues.prefix at w, f, ℝ, k with valuesW213    have prefixV := WeightedValues.prefix at v, f, ℝ, k with valuesV214    have lastW := WeightedValues.last at w, f, ℝ, k with valuesW215    have lastV := WeightedValues.last at v, f, ℝ, k with valuesV216    have prefixBounds : ∀ i ∈ k, (w(f(i)):R) ≤ (v(f(i)):R)217      intros i hi218      have next := membership.into_successor at i, k with *219      exact bounds with i, next220    have lastBound := bounds with k, membership.self_successor at k with *221    have previous := ih with prefixW, prefixV, prefixBounds222    have closureW := indexedRingSum.closed at ℝ, realAdd, realZero, realNeg,223      realMul, realOne, w, f, k with ring224    have closureV := indexedRingSum.closed at ℝ, realAdd, realZero, realNeg,225      realMul, realOne, v, f, k with ring226    have sumW := closureW with prefixW227    have sumV := closureV with prefixV228    rw [indexedRingSum, indexedRingSum]229    linarith230231theorem realSetSum.monotone (V Ω w v : Set)232  requires finite : Finite(V)233  requires weightsW : w : Ω → ℝ234  requires weightsV : v : Ω → ℝ235  requires subset : V ⊆ Ω236  requires bounds : ∀ x ∈ V, (w(x):R) ≤ (v(x):R)237  shows (realSetSum(V, w):R) ≤ (realSetSum(V, v):R)238proof239  obtain ⟨n, natural, f, enumeration⟩ := Finite.enumeration with finite240  have injective := Bijective.injective with enumeration241  have function := Injective.function with injective242  have sumW := realSetSum.enumeration with weightsW, subset, enumeration243  have sumV := realSetSum.enumeration with weightsV, subset, enumeration244  have valuesW := realSetSum.weighted_values with weightsW, subset, function245  have valuesV := realSetSum.weighted_values with weightsV, subset, function246  have indexBounds : ∀ i ∈ n, (w(f(i)):R) ≤ (v(f(i)):R)247    intros i hi248    have member := FunctionBetween.apply_closed with function, hi249    exact bounds with f(i), member250  have monotone := indexedRingSum.real_monotone at w, v, f, n251  rw [sumW, sumV]252  exact monotone with valuesW, valuesV, indexBounds253254-- Pointwise sum of two real-valued functions on the same domain.255defgraph weightAdd (Ω w v : Set) (x ∈ Ω) : ℝ := call2(realAdd, w(x), v(x))256requires weightsW : w : Ω → ℝ257requires weightsV : v : Ω → ℝ258proof259  have left := FunctionBetween.apply_closed with weightsW, member260  have right := FunctionBetween.apply_closed with weightsV, member261  exact realAddValue.real at w(x), v(x)262263theorem realSetSum.add (V Ω w v : Set)264  requires finite : Finite(V)265  requires weightsW : w : Ω → ℝ266  requires weightsV : v : Ω → ℝ267  requires subset : V ⊆ Ω268  shows realSetSum(V, weightAdd(Ω, w, v)) =269    (realSetSum(V, w):R) + (realSetSum(V, v):R)270proof271  have ring := reals.comm_ring272  obtain ⟨n, natural, f, enumeration⟩ := Finite.enumeration with finite273  have injective := Bijective.injective with enumeration274  have function := Injective.function with injective275  have combined := weightAdd.function with weightsW, weightsV276  have sumW := realSetSum.enumeration with weightsW, subset, enumeration277  have sumV := realSetSum.enumeration with weightsV, subset, enumeration278  have sumBoth := realSetSum.enumeration with combined, subset, enumeration279  have valuesW := realSetSum.weighted_values with weightsW, subset, function280  have valuesV := realSetSum.weighted_values with weightsV, subset, function281  have equations : ∀ i ∈ n, weightAdd(Ω, w, v)(f(i)) = (w(f(i)):R) + (v(f(i)):R)282    intros i hi283    have inV := FunctionBetween.apply_closed with function, hi284    have inDomain := subset with f(i), inV285    exact weightAdd.value with weightsW, weightsV, inDomain286  have distribute := indexedRingSum.add at ℝ, realAdd, realZero, realNeg,287      realMul,288    realOne, w, v, weightAdd(Ω, w, v), f, n with ring289  rw [sumBoth, sumW, sumV]290  exact distribute with valuesW, valuesV, equations291292-- Pointwise scaling of a real-valued function by a constant.293defgraph weightScale (Ω : Set) (c : Real) (w : Set) (x ∈ Ω) : ℝ :=294  call2(realMul, c, w(x))295requires weights : w : Ω → ℝ296proof297  have value := FunctionBetween.apply_closed with weights, member298  exact realMulValue.real at c, w(x)299300theorem realSetSum.scale (V Ω w : Set) (c : Real)301  requires finite : Finite(V)302  requires weights : w : Ω → ℝ303  requires subset : V ⊆ Ω304  shows realSetSum(V, weightScale(Ω, c, w)) = c * (realSetSum(V, w):R)305proof306  have ring := reals.comm_ring307  have scalar : c ∈ ℝ by simp [Real]308  obtain ⟨n, natural, f, enumeration⟩ := Finite.enumeration with finite309  have injective := Bijective.injective with enumeration310  have function := Injective.function with injective311  have scaled := weightScale.function at Ω, c, w with weights312  have sumW := realSetSum.enumeration with weights, subset, enumeration313  have sumScaled := realSetSum.enumeration with scaled, subset, enumeration314  have valuesW := realSetSum.weighted_values with weights, subset, function315  have equations : ∀ i ∈ n, weightScale(Ω, c, w)(f(i)) = c * (w(f(i)):R)316    intros i hi317    have inV := FunctionBetween.apply_closed with function, hi318    have inDomain := subset with f(i), inV319    exact weightScale.value at Ω, c, w, f(i) with weights, inDomain320  have distribute := indexedRingSum.scale at ℝ, realAdd, realZero, realNeg,321      realMul,322    realOne, w, c, weightScale(Ω, c, w), f, n with ring, scalar323  rw [sumScaled, sumW]324  exact distribute with valuesW, equations325326theorem indexedRingSum.real_constant (Ω f : Set) (c : Real) (n : Nat)327  shows (∀ i ∈ n, f(i) ∈ Ω) →328    indexedRingSum(constantFunction(Ω, ℝ, c), f, realAdd, realZero, n) =329      (realNat(n):R) * c330proof331  induction n332  | zero =>333    intro values334    rw [indexedRingSum, realNat.zero]335    ring336  | succ(k) using ih =>337    intro values338    have scalar : c ∈ ℝ by simp [Real]339    have prefix : ∀ i ∈ k, f(i) ∈ Ω340      intros i hi341      have next := membership.into_successor at i, k with *342      exact values with i, next343    have last := values with k, membership.self_successor at k with *344    have previous := ih with prefix345    have value := constantFunction.apply with last, scalar346    have natural := realNat.real at k347    rw [indexedRingSum, previous, value, realNat.succ]348    ring349350theorem realSetSum.constant (V Ω : Set) (c : Real)351  requires finite : Finite(V)352  requires subset : V ⊆ Ω353  shows realSetSum(V, constantFunction(Ω, ℝ,354      c)) = (realNat(cardinality(V)):R) * c355proof356  have scalar : c ∈ ℝ by simp [Real]357  have weights := constantFunction.function at Ω, ℝ, c with scalar358  obtain ⟨natural, g, bijective⟩ := cardinality.correct with finite359  have enumeration := converse.bijective with bijective360  have injective := Bijective.injective with enumeration361  have function := Injective.function with injective362  have sum := realSetSum.enumeration with weights, subset, enumeration363  have values : ∀ i ∈ cardinality(V), converse(g, V, cardinality(V))(i) ∈ Ω364    intros i hi365    have inV := FunctionBetween.apply_closed with function, hi366    exact subset with converse(g, V, cardinality(V))(i), inV367  have constant := indexedRingSum.real_constant at Ω, converse(g, V,368      cardinality(V)),369    c, cardinality(V)370  rw sum371  exact constant with values372373-- A real sum restricted to the support of its weight.374theorem realSetSum.restrict (V S Ω w : Set)375  requires finite : Finite(V)376  requires weights : w : Ω → ℝ377  requires subset : V ⊆ Ω378  requires inner : S ⊆ V379  requires vanishes : ∀ x ∈ V, ¬(x ∈ S) → w(x) = (0:R)380  shows realSetSum(V, w) = realSetSum(S, w)381proof382  have ring := reals.comm_ring383  have restricted := restrict.domain_function with weights, subset384  have vanishing : ∀ x ∈ V, ¬(x ∈ S) → restrict(w, V)(x) = realZero385    intros x hx outside386    have value := restrict.domain_apply with weights, subset, hx387    have zero := vanishes with x, hx, outside388    cc389  have sum := finiteRingSum.restrict at V, S, ℝ, realAdd, realZero, realNeg,390    realMul, realOne, restrict(w, V) with ring, finite, restricted, inner,391      vanishing392  have nested := restrict.nested at w, S, V with inner393  unfold realSetSum394  cc395396-- The weight w cut down to S: w on S and zero elsewhere.397defgraph maskedWeight (Ω S w : Set) (x ∈ Ω) : ℝ :=398  call2(realMul, realNat(indicator(S, x)), w(x))399requires weights : w : Ω → ℝ400proof401  have natural := indicator.natural at S, x402  have mask := realNat.real at indicator(S, x)403  have value := FunctionBetween.apply_closed with weights, member404  exact realMulValue.real at realNat(indicator(S, x)), w(x)405406theorem maskedWeight.inside (Ω S w x : Set)407  requires weights : w : Ω → ℝ408  requires member : x ∈ Ω409  requires inside : x ∈ S410  shows maskedWeight(Ω, S, w)(x) = w(x)411proof412  have value := maskedWeight.value at Ω, S, w, x with weights, member413  have one := indicator.member with inside414  have valueReal := FunctionBetween.apply_closed with weights, member415  rw [value, one, realNat.one]416  ring417418theorem maskedWeight.outside (Ω S w x : Set)419  requires weights : w : Ω → ℝ420  requires member : x ∈ Ω421  requires outside : ¬(x ∈ S)422  shows maskedWeight(Ω, S, w)(x) = (0:R)423proof424  have value := maskedWeight.value at Ω, S, w, x with weights, member425  have zero := indicator.absent with outside426  have valueReal := FunctionBetween.apply_closed with weights, member427  rw [value, zero, realNat.zero]428  ring429430-- The masked weight sums over V to the original weight summed over S.431theorem realSetSum.masked (V S Ω w : Set)432  requires finite : Finite(V)433  requires weights : w : Ω → ℝ434  requires subset : V ⊆ Ω435  requires inner : S ⊆ V436  shows realSetSum(V, maskedWeight(Ω, S, w)) = realSetSum(S, w)437proof438  have masked := maskedWeight.function at Ω, S, w with weights439  have finiteS := Finite.subset with finite, inner440  have subsetS := Subset.transitive with inner, subset441  have vanishes : ∀ x ∈ V, ¬(x ∈ S) → maskedWeight(Ω, S, w)(x) = (0:R)442    intros x hx outside443    have member := subset with x, hx444    exact maskedWeight.outside with weights, member, outside445  have restricted := realSetSum.restrict with finite, masked, subset, inner,446      vanishes447  have agree : ∀ x ∈ S, maskedWeight(Ω, S, w)(x) = w(x)448    intros x hx449    have member := subsetS with x, hx450    exact maskedWeight.inside with weights, member, hx451  have same := realSetSum.congr with masked, weights, subsetS, agree452  rw [restricted, same]453  rfl454455theorem realSetSum.union_disjoint (V W Ω w : Set)456  requires finiteV : Finite(V)457  requires finiteW : Finite(W)458  requires weights : w : Ω → ℝ459  requires subsetV : V ⊆ Ω460  requires subsetW : W ⊆ Ω461  requires disjoint : Disjoint(V, W)462  shows realSetSum(V ∪ W, w) = (realSetSum(V, w):R) + (realSetSum(W, w):R)463proof464  have finite := Finite.union with finiteV, finiteW465  have subset : V ∪ W ⊆ Ω by simp466  have innerV := union2.subset_left at V, W467  have innerW := union2.subset_right at V, W468  have maskV := maskedWeight.function at Ω, V, w with weights469  have maskW := maskedWeight.function at Ω, W, w with weights470  have combined := weightAdd.function with maskV, maskW471  have absent := Disjoint.iff.forward with disjoint472  have split : ∀ y ∈ V ∪ W, w(y) = weightAdd(Ω, maskedWeight(Ω, V, w),473      maskedWeight(Ω, W, w))(y)474    intros y hy475    have member := subset with y, hy476    have valueReal := FunctionBetween.apply_closed with weights, member477    have added := weightAdd.value with maskV, maskW, member478    have alternatives := union2.membership.forward with hy479    cases alternatives with inV | inW480    . have notW := absent with y, inV481      have left := maskedWeight.inside at Ω, V, w, y with weights, member, inV482      have right := maskedWeight.outside at Ω, W, w, y with weights, member,483          notW484      rw [added, left, right]485      ring486    . have notV : ¬(y ∈ V)487        intro inV488        exact absent with y, inV, inW489      have left := maskedWeight.outside at Ω, V, w, y with weights, member, notV490      have right := maskedWeight.inside at Ω, W, w, y with weights, member, inW491      rw [added, left, right]492      ring493  have same := realSetSum.congr with weights, combined, subset, split494  have sumAdd := realSetSum.add with finite, maskV, maskW, subset495  have sumV := realSetSum.masked with finite, weights, subset, innerV496  have sumW := realSetSum.masked with finite, weights, subset, innerW497  rw [same, sumAdd, sumV, sumW]498  rfl499500theorem realSetSum.difference (V S Ω w : Set)501  requires finite : Finite(V)502  requires weights : w : Ω → ℝ503  requires subset : V ⊆ Ω504  requires inner : S ⊆ V505  shows realSetSum(V, w) = (realSetSum(S, w):R) + (realSetSum(V ∖ S, w):R)506proof507  have rest := difference.subset_left at V, S508  have finiteS := Finite.subset with finite, inner509  have finiteRest := Finite.subset with finite, rest510  have subsetS := Subset.transitive with inner, subset511  have subsetRest := Subset.transitive with rest, subset512  have disjoint := Disjoint.difference_right at V, S513  have union := difference.union2_of_subset with inner514  have sum := realSetSum.union_disjoint with finiteS, finiteRest, weights,515    subsetS, subsetRest, disjoint516  rw union at sum517  exact sum518519theorem realSetSum.subset_le (V S Ω w : Set)520  requires finite : Finite(V)521  requires weights : w : Ω → ℝ522  requires subset : V ⊆ Ω523  requires inner : S ⊆ V524  requires bounds : ∀ x ∈ V, (0:R) ≤ (w(x):R)525  shows (realSetSum(S, w):R) ≤ (realSetSum(V, w):R)526proof527  have rest := difference.subset_left at V, S528  have finiteS := Finite.subset with finite, inner529  have finiteRest := Finite.subset with finite, rest530  have subsetS := Subset.transitive with inner, subset531  have subsetRest := Subset.transitive with rest, subset532  have split := realSetSum.difference with finite, weights, subset, inner533  have restBounds : ∀ x ∈ V ∖ S, (0:R) ≤ (w(x):R)534    intros x hx535    have inV := rest with x, hx536    exact bounds with x, inV537  have restNonnegative := realSetSum.nonnegative with finiteRest, weights,538    subsetRest, restBounds539  have sumS := realSetSum.real with finiteS, weights, subsetS540  have sumRest := realSetSum.real with finiteRest, weights, subsetRest541  rw split542  linarith543544theorem realSetSum.insert_member (V Ω w a : Set)545  requires finite : Finite(V)546  requires weights : w : Ω → ℝ547  requires subset : V ⊆ Ω548  requires member : a ∈ V549  shows realSetSum(V, w) = (realSetSum(V ∖ {a}, w):R) + (w(a):R)550proof551  have rest := difference.subset_left at V, {a}552  have finiteRest := Finite.subset with finite, rest553  have subsetRest := Subset.transitive with rest, subset554  have inDomain := subset with a, member555  have fresh : ¬(a ∈ V ∖ {a}) by simp556  have restored := insert.restore with member557  have inserted := realSetSum.insert with finiteRest, weights, subsetRest,558      inDomain, fresh559  rw restored at inserted560  exact inserted561562-- Masking by S and summing over V counts only the points of V ∩ S.563theorem realSetSum.masked_intersection (V S Ω w : Set)564  requires finite : Finite(V)565  requires weights : w : Ω → ℝ566  requires subset : V ⊆ Ω567  shows realSetSum(V, maskedWeight(Ω, S, w)) = realSetSum(V ∩ S, w)568proof569  have masked := maskedWeight.function at Ω, S, w with weights570  have inner := intersection.subset_left at V, S571  have subsetMeet := Subset.transitive with inner, subset572  have vanishes : ∀ x ∈ V, ¬(x ∈ V ∩ S) → maskedWeight(Ω, S, w)(x) = (0:R)573    intros x hx outside574    have member := subset with x, hx575    have notS : ¬(x ∈ S)576      intro inS577      apply outside578      exact intersection.membership.backward with ⟨hx, inS⟩579    exact maskedWeight.outside with weights, member, notS580  have restricted := realSetSum.restrict with finite, masked, subset, inner,581      vanishes582  have agree : ∀ x ∈ V ∩ S, maskedWeight(Ω, S, w)(x) = w(x)583    intros x hx584    have member := subsetMeet with x, hx585    have inS := intersection.membership.forward with hx586    exact maskedWeight.inside with weights, member, inS.right587  have same := realSetSum.congr with masked, weights, subsetMeet, agree588  rw [restricted, same]589  rfl590591-- The real indicator of S on Ω.592defgraph realIndicator (Ω S : Set) (x ∈ Ω) : ℝ := realNat(indicator(S, x))593proof594  have natural := indicator.natural at S, x595  exact realNat.real at indicator(S, x)596597theorem realIndicator.inside (Ω S x : Set)598  requires member : x ∈ Ω599  requires inside : x ∈ S600  shows realIndicator(Ω, S)(x) = (1:R)601proof602  have value := realIndicator.value at Ω, S, x with member603  have one := indicator.member with inside604  rw [value, one, realNat.one]605  rfl606607theorem realIndicator.outside (Ω S x : Set)608  requires member : x ∈ Ω609  requires outside : ¬(x ∈ S)610  shows realIndicator(Ω, S)(x) = (0:R)611proof612  have value := realIndicator.value at Ω, S, x with member613  have zero := indicator.absent with outside614  rw [value, zero, realNat.zero]615  rfl616617theorem realIndicator.nonnegative (Ω S x : Set)618  requires member : x ∈ Ω619  shows (0:R) ≤ (realIndicator(Ω, S)(x):R)620proof621  have value := realIndicator.value at Ω, S, x with member622  have natural := indicator.natural at S, x623  have nonnegative := realNat.zero_le at indicator(S, x)624  rw value625  exact nonnegative626627theorem realIndicator.le_one (Ω S x : Set)628  requires member : x ∈ Ω629  shows (realIndicator(Ω, S)(x):R) ≤ (1:R)630proof631  have alternatives : x ∈ S ∨ ¬(x ∈ S) by tauto632  cases alternatives with inside | outside633  . have one := realIndicator.inside with member, inside634    rw one635    exact realLe.reflexive with realOne.real636  . have zero := realIndicator.outside with member, outside637    rw zero638    have one := realZero.lt_one639    linarith640641-- The indicator of S is the constant one masked by S, so its sum counts.642theorem realSetSum.indicator (V S Ω : Set)643  requires finite : Finite(V)644  requires subset : V ⊆ Ω645  shows realSetSum(V, realIndicator(Ω, S)) = (realNat(cardinality(V ∩ S)):R)646proof647  have oneReal := realOne.real648  have ones := constantFunction.function at Ω, ℝ, (1:R) with oneReal649  have indicator := realIndicator.function at Ω, S650  have masked := maskedWeight.function at Ω, S, constantFunction(Ω, ℝ,651      (1:R)) with ones652  have agree : ∀ x ∈ V, realIndicator(Ω, S)(x) =653      maskedWeight(Ω, S, constantFunction(Ω, ℝ, (1:R)))(x)654    intros x hx655    have member := subset with x, hx656    have value := realIndicator.value at Ω, S, x with member657    have maskValue := maskedWeight.value at Ω, S, constantFunction(Ω, ℝ,658        (1:R)), x with659      ones, member660    have one := constantFunction.apply at Ω, ℝ, x, (1:R) with member, oneReal661    have natural := indicator.natural at S, x662    have maskReal := realNat.real at indicator(S, x)663    rw [value, maskValue, one]664    ring665  have same := realSetSum.congr with indicator, masked, subset, agree666  have counted := realSetSum.masked_intersection at V, S, Ω,667    constantFunction(Ω, ℝ, (1:R)) with finite, ones, subset668  have inner := intersection.subset_left at V, S669  have finiteMeet := Finite.subset with finite, inner670  have subsetMeet := Subset.transitive with inner, subset671  have constant := realSetSum.constant at V ∩ S, Ω, (1:R) with finiteMeet,672      subsetMeet673  have natural := cardinality.nat with finiteMeet674  have countReal := realNat.real at cardinality(V ∩ S)675  rw [same, counted, constant]676  ring677