-- Real-valued sums over finite sets
-- 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.Probability.SetSum
import Algebra.Ring.SumSupport
import Real.Natural
import Cardinal

-- The sum of a real-valued weight over a finite set, as the canonical
-- commutative ring sum of the reals.
def realSetSum (V w : Set) : Set :=
  finiteRingSum(V, ℝ, realAdd, realZero, realNeg, realMul, realOne, restrict(w,
    V))

theorem realSetSum.real (V Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  shows Real(realSetSum(V, w))
proof
  have ring := reals.comm_ring
  have restricted := restrict.domain_function with weights, subset
  have closed := finiteRingSum.closed with ring, finite, restricted
  unfold realSetSum
  exact closed

theorem realSetSum.empty (w : Set)
  shows realSetSum(∅, w) = (0:R)
proof
  have ring := reals.comm_ring
  have restricted : restrict(w, ∅) : ∅ → ℝ
    have same := restrict.empty at w
    rw same
    exact FunctionBetween.empty at ℝ
  have sum := finiteRingSum.empty with ring, restricted
  unfold realSetSum
  cc

-- An enumeration of the index set turns the sum into an indexed sum of the
-- original weight.
theorem realSetSum.enumeration (V Ω w f : Set, n : Nat)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires enumeration : BijectiveBetween(f, n, V)
  shows realSetSum(V, w) = indexedRingSum(w, f, realAdd, realZero, n)
proof
  have ring := reals.comm_ring
  have restricted := restrict.domain_function with weights, subset
  have sum := finiteRingSum.enumeration at V, ℝ, realAdd, realZero, realNeg,
    realMul, realOne, restrict(w, V), f, n with ring, restricted, enumeration
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have values : ∀ i ∈ n, restrict(w, V)(f(i)) = w(f(i))
    intros i hi
    have member := FunctionBetween.apply_closed with function, hi
    exact restrict.domain_apply with weights, subset, member
  have congr := indexedRingSum.congr at restrict(w, V), w, f, f, realAdd,
      realZero, n
  have same := congr with values
  unfold realSetSum
  cc

theorem realSetSum.weighted_values (V Ω w f : Set, n : Nat)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires function : f : n → V
  shows WeightedValues(w, f, ℝ, n)
proof
  intros i hi
  have inV := FunctionBetween.apply_closed with function, hi
  have inDomain := subset with f(i), inV
  exact FunctionBetween.apply_closed with weights, inDomain

theorem realSetSum.insert (V Ω w a : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires member : a ∈ Ω
  requires fresh : ¬(a ∈ V)
  shows realSetSum(insert(a, V), w) = (realSetSum(V, w):R) + (w(a):R)
proof
  have ring := reals.comm_ring
  have bigger : insert(a, V) ⊆ Ω by simp
  have inner : V ⊆ insert(a, V) by simp
  have selfMember : a ∈ insert(a, V) by simp
  have restricted := restrict.domain_function with weights, bigger
  have inserted := finiteRingSum.insert with ring, finite, restricted, fresh
  have nested := restrict.nested at w, V, insert(a, V) with inner
  have value := restrict.domain_apply with weights, bigger, selfMember
  unfold realSetSum
  cc

theorem realSetSum.singleton (Ω w a : Set)
  requires weights : w : Ω → ℝ
  requires member : a ∈ Ω
  shows realSetSum({a}, w) = w(a)
proof
  have same : insert(a, ∅) = {a}
    ext y
    simp
  have finite := Finite.empty
  have subset := empty.subset at Ω
  have fresh := set.empty at a
  have inserted := realSetSum.insert with finite, weights, subset, member, fresh
  have emptySum := realSetSum.empty at w
  have value := FunctionBetween.apply_closed with weights, member
  rw same at inserted
  rw [inserted, emptySum]
  ring

theorem realSetSum.congr (V Ω w v : Set)
  requires weightsW : w : Ω → ℝ
  requires weightsV : v : Ω → ℝ
  requires subset : V ⊆ Ω
  requires values : ∀ x ∈ V, w(x) = v(x)
  shows realSetSum(V, w) = realSetSum(V, v)
proof
  have restrictedW := restrict.domain_function with weightsW, subset
  have restrictedV := restrict.domain_function with weightsV, subset
  have same : ∀ x ∈ V, restrict(w, V)(x) = restrict(v, V)(x)
    intros x hx
    have left := restrict.domain_apply with weightsW, subset, hx
    have right := restrict.domain_apply with weightsV, subset, hx
    have equal := values with x, hx
    cc
  have equal := FunctionBetween.ext with restrictedW, restrictedV, same
  unfold realSetSum
  cc

theorem realSetSum.zero (V Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires values : ∀ x ∈ V, w(x) = (0:R)
  shows realSetSum(V, w) = (0:R)
proof
  have ring := reals.comm_ring
  have restricted := restrict.domain_function with weights, subset
  have vanishing : ∀ x ∈ V, restrict(w, V)(x) = realZero
    intros x hx
    have value := restrict.domain_apply with weights, subset, hx
    have zero := values with x, hx
    cc
  have sum := finiteRingSum.zero with ring, finite, restricted, vanishing
  unfold realSetSum
  cc

-- Indexed real sums of nonnegative terms are nonnegative.
theorem indexedRingSum.real_nonnegative (w f : Set, n : Nat)
  shows WeightedValues(w, f, ℝ, n) → (∀ i ∈ n, (0:R) ≤ (w(f(i)):R)) →
    (0:R) ≤ (indexedRingSum(w, f, realAdd, realZero, n):R)
proof
  induction n
  | zero =>
    intros values bounds
    rw indexedRingSum
    exact realLe.reflexive with realZero.real
  | succ(k) using ih =>
    intros values bounds
    have ring := reals.comm_ring
    have prefix := WeightedValues.prefix at w, f, ℝ, k with values
    have last := WeightedValues.last at w, f, ℝ, k with values
    have prefixBounds : ∀ i ∈ k, (0:R) ≤ (w(f(i)):R)
      intros i hi
      have next := membership.into_successor at i, k with *
      exact bounds with i, next
    have lastBound := bounds with k, membership.self_successor at k with *
    have previous := ih with prefix, prefixBounds
    have closure := indexedRingSum.closed at ℝ, realAdd, realZero, realNeg,
      realMul, realOne, w, f, k with ring
    have sumReal := closure with prefix
    rw indexedRingSum
    linarith

theorem realSetSum.nonnegative (V Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires bounds : ∀ x ∈ V, (0:R) ≤ (w(x):R)
  shows (0:R) ≤ (realSetSum(V, w):R)
proof
  obtain ⟨n, natural, f, enumeration⟩ := Finite.enumeration with finite
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have sum := realSetSum.enumeration with weights, subset, enumeration
  have values := realSetSum.weighted_values with weights, subset, function
  have indexBounds : ∀ i ∈ n, (0:R) ≤ (w(f(i)):R)
    intros i hi
    have member := FunctionBetween.apply_closed with function, hi
    exact bounds with f(i), member
  have nonnegative := indexedRingSum.real_nonnegative at w, f, n
  rw sum
  exact nonnegative with values, indexBounds

theorem indexedRingSum.real_monotone (w v f : Set, n : Nat)
  shows WeightedValues(w, f, ℝ, n) → WeightedValues(v, f, ℝ, n) →
    (∀ i ∈ n, (w(f(i)):R) ≤ (v(f(i)):R)) →
    (indexedRingSum(w, f, realAdd, realZero, n):R) ≤
      (indexedRingSum(v, f, realAdd, realZero, n):R)
proof
  induction n
  | zero =>
    intros valuesW valuesV bounds
    rw [indexedRingSum, indexedRingSum]
    exact realLe.reflexive with realZero.real
  | succ(k) using ih =>
    intros valuesW valuesV bounds
    have ring := reals.comm_ring
    have prefixW := WeightedValues.prefix at w, f, ℝ, k with valuesW
    have prefixV := WeightedValues.prefix at v, f, ℝ, k with valuesV
    have lastW := WeightedValues.last at w, f, ℝ, k with valuesW
    have lastV := WeightedValues.last at v, f, ℝ, k with valuesV
    have prefixBounds : ∀ i ∈ k, (w(f(i)):R) ≤ (v(f(i)):R)
      intros i hi
      have next := membership.into_successor at i, k with *
      exact bounds with i, next
    have lastBound := bounds with k, membership.self_successor at k with *
    have previous := ih with prefixW, prefixV, prefixBounds
    have closureW := indexedRingSum.closed at ℝ, realAdd, realZero, realNeg,
      realMul, realOne, w, f, k with ring
    have closureV := indexedRingSum.closed at ℝ, realAdd, realZero, realNeg,
      realMul, realOne, v, f, k with ring
    have sumW := closureW with prefixW
    have sumV := closureV with prefixV
    rw [indexedRingSum, indexedRingSum]
    linarith

theorem realSetSum.monotone (V Ω w v : Set)
  requires finite : Finite(V)
  requires weightsW : w : Ω → ℝ
  requires weightsV : v : Ω → ℝ
  requires subset : V ⊆ Ω
  requires bounds : ∀ x ∈ V, (w(x):R) ≤ (v(x):R)
  shows (realSetSum(V, w):R) ≤ (realSetSum(V, v):R)
proof
  obtain ⟨n, natural, f, enumeration⟩ := Finite.enumeration with finite
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have sumW := realSetSum.enumeration with weightsW, subset, enumeration
  have sumV := realSetSum.enumeration with weightsV, subset, enumeration
  have valuesW := realSetSum.weighted_values with weightsW, subset, function
  have valuesV := realSetSum.weighted_values with weightsV, subset, function
  have indexBounds : ∀ i ∈ n, (w(f(i)):R) ≤ (v(f(i)):R)
    intros i hi
    have member := FunctionBetween.apply_closed with function, hi
    exact bounds with f(i), member
  have monotone := indexedRingSum.real_monotone at w, v, f, n
  rw [sumW, sumV]
  exact monotone with valuesW, valuesV, indexBounds

-- Pointwise sum of two real-valued functions on the same domain.
defgraph weightAdd (Ω w v : Set) (x ∈ Ω) : ℝ := call2(realAdd, w(x), v(x))
requires weightsW : w : Ω → ℝ
requires weightsV : v : Ω → ℝ
proof
  have left := FunctionBetween.apply_closed with weightsW, member
  have right := FunctionBetween.apply_closed with weightsV, member
  exact realAddValue.real at w(x), v(x)

theorem realSetSum.add (V Ω w v : Set)
  requires finite : Finite(V)
  requires weightsW : w : Ω → ℝ
  requires weightsV : v : Ω → ℝ
  requires subset : V ⊆ Ω
  shows realSetSum(V, weightAdd(Ω, w, v)) =
    (realSetSum(V, w):R) + (realSetSum(V, v):R)
proof
  have ring := reals.comm_ring
  obtain ⟨n, natural, f, enumeration⟩ := Finite.enumeration with finite
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have combined := weightAdd.function with weightsW, weightsV
  have sumW := realSetSum.enumeration with weightsW, subset, enumeration
  have sumV := realSetSum.enumeration with weightsV, subset, enumeration
  have sumBoth := realSetSum.enumeration with combined, subset, enumeration
  have valuesW := realSetSum.weighted_values with weightsW, subset, function
  have valuesV := realSetSum.weighted_values with weightsV, subset, function
  have equations : ∀ i ∈ n, weightAdd(Ω, w, v)(f(i)) = (w(f(i)):R) + (v(f(i)):R)
    intros i hi
    have inV := FunctionBetween.apply_closed with function, hi
    have inDomain := subset with f(i), inV
    exact weightAdd.value with weightsW, weightsV, inDomain
  have distribute := indexedRingSum.add at ℝ, realAdd, realZero, realNeg,
      realMul,
    realOne, w, v, weightAdd(Ω, w, v), f, n with ring
  rw [sumBoth, sumW, sumV]
  exact distribute with valuesW, valuesV, equations

-- Pointwise scaling of a real-valued function by a constant.
defgraph weightScale (Ω : Set) (c : Real) (w : Set) (x ∈ Ω) : ℝ :=
  call2(realMul, c, w(x))
requires weights : w : Ω → ℝ
proof
  have value := FunctionBetween.apply_closed with weights, member
  exact realMulValue.real at c, w(x)

theorem realSetSum.scale (V Ω w : Set) (c : Real)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  shows realSetSum(V, weightScale(Ω, c, w)) = c * (realSetSum(V, w):R)
proof
  have ring := reals.comm_ring
  have scalar : c ∈ ℝ by simp [Real]
  obtain ⟨n, natural, f, enumeration⟩ := Finite.enumeration with finite
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have scaled := weightScale.function at Ω, c, w with weights
  have sumW := realSetSum.enumeration with weights, subset, enumeration
  have sumScaled := realSetSum.enumeration with scaled, subset, enumeration
  have valuesW := realSetSum.weighted_values with weights, subset, function
  have equations : ∀ i ∈ n, weightScale(Ω, c, w)(f(i)) = c * (w(f(i)):R)
    intros i hi
    have inV := FunctionBetween.apply_closed with function, hi
    have inDomain := subset with f(i), inV
    exact weightScale.value at Ω, c, w, f(i) with weights, inDomain
  have distribute := indexedRingSum.scale at ℝ, realAdd, realZero, realNeg,
      realMul,
    realOne, w, c, weightScale(Ω, c, w), f, n with ring, scalar
  rw [sumScaled, sumW]
  exact distribute with valuesW, equations

theorem indexedRingSum.real_constant (Ω f : Set) (c : Real) (n : Nat)
  shows (∀ i ∈ n, f(i) ∈ Ω) →
    indexedRingSum(constantFunction(Ω, ℝ, c), f, realAdd, realZero, n) =
      (realNat(n):R) * c
proof
  induction n
  | zero =>
    intro values
    rw [indexedRingSum, realNat.zero]
    ring
  | succ(k) using ih =>
    intro values
    have scalar : c ∈ ℝ by simp [Real]
    have prefix : ∀ i ∈ k, f(i) ∈ Ω
      intros i hi
      have next := membership.into_successor at i, k with *
      exact values with i, next
    have last := values with k, membership.self_successor at k with *
    have previous := ih with prefix
    have value := constantFunction.apply with last, scalar
    have natural := realNat.real at k
    rw [indexedRingSum, previous, value, realNat.succ]
    ring

theorem realSetSum.constant (V Ω : Set) (c : Real)
  requires finite : Finite(V)
  requires subset : V ⊆ Ω
  shows realSetSum(V, constantFunction(Ω, ℝ,
      c)) = (realNat(cardinality(V)):R) * c
proof
  have scalar : c ∈ ℝ by simp [Real]
  have weights := constantFunction.function at Ω, ℝ, c with scalar
  obtain ⟨natural, g, bijective⟩ := cardinality.correct with finite
  have enumeration := converse.bijective with bijective
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have sum := realSetSum.enumeration with weights, subset, enumeration
  have values : ∀ i ∈ cardinality(V), converse(g, V, cardinality(V))(i) ∈ Ω
    intros i hi
    have inV := FunctionBetween.apply_closed with function, hi
    exact subset with converse(g, V, cardinality(V))(i), inV
  have constant := indexedRingSum.real_constant at Ω, converse(g, V,
      cardinality(V)),
    c, cardinality(V)
  rw sum
  exact constant with values

-- A real sum restricted to the support of its weight.
theorem realSetSum.restrict (V S Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires inner : S ⊆ V
  requires vanishes : ∀ x ∈ V, ¬(x ∈ S) → w(x) = (0:R)
  shows realSetSum(V, w) = realSetSum(S, w)
proof
  have ring := reals.comm_ring
  have restricted := restrict.domain_function with weights, subset
  have vanishing : ∀ x ∈ V, ¬(x ∈ S) → restrict(w, V)(x) = realZero
    intros x hx outside
    have value := restrict.domain_apply with weights, subset, hx
    have zero := vanishes with x, hx, outside
    cc
  have sum := finiteRingSum.restrict at V, S, ℝ, realAdd, realZero, realNeg,
    realMul, realOne, restrict(w, V) with ring, finite, restricted, inner,
      vanishing
  have nested := restrict.nested at w, S, V with inner
  unfold realSetSum
  cc

-- The weight w cut down to S: w on S and zero elsewhere.
defgraph maskedWeight (Ω S w : Set) (x ∈ Ω) : ℝ :=
  call2(realMul, realNat(indicator(S, x)), w(x))
requires weights : w : Ω → ℝ
proof
  have natural := indicator.natural at S, x
  have mask := realNat.real at indicator(S, x)
  have value := FunctionBetween.apply_closed with weights, member
  exact realMulValue.real at realNat(indicator(S, x)), w(x)

theorem maskedWeight.inside (Ω S w x : Set)
  requires weights : w : Ω → ℝ
  requires member : x ∈ Ω
  requires inside : x ∈ S
  shows maskedWeight(Ω, S, w)(x) = w(x)
proof
  have value := maskedWeight.value at Ω, S, w, x with weights, member
  have one := indicator.member with inside
  have valueReal := FunctionBetween.apply_closed with weights, member
  rw [value, one, realNat.one]
  ring

theorem maskedWeight.outside (Ω S w x : Set)
  requires weights : w : Ω → ℝ
  requires member : x ∈ Ω
  requires outside : ¬(x ∈ S)
  shows maskedWeight(Ω, S, w)(x) = (0:R)
proof
  have value := maskedWeight.value at Ω, S, w, x with weights, member
  have zero := indicator.absent with outside
  have valueReal := FunctionBetween.apply_closed with weights, member
  rw [value, zero, realNat.zero]
  ring

-- The masked weight sums over V to the original weight summed over S.
theorem realSetSum.masked (V S Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires inner : S ⊆ V
  shows realSetSum(V, maskedWeight(Ω, S, w)) = realSetSum(S, w)
proof
  have masked := maskedWeight.function at Ω, S, w with weights
  have finiteS := Finite.subset with finite, inner
  have subsetS := Subset.transitive with inner, subset
  have vanishes : ∀ x ∈ V, ¬(x ∈ S) → maskedWeight(Ω, S, w)(x) = (0:R)
    intros x hx outside
    have member := subset with x, hx
    exact maskedWeight.outside with weights, member, outside
  have restricted := realSetSum.restrict with finite, masked, subset, inner,
      vanishes
  have agree : ∀ x ∈ S, maskedWeight(Ω, S, w)(x) = w(x)
    intros x hx
    have member := subsetS with x, hx
    exact maskedWeight.inside with weights, member, hx
  have same := realSetSum.congr with masked, weights, subsetS, agree
  rw [restricted, same]
  rfl

theorem realSetSum.union_disjoint (V W Ω w : Set)
  requires finiteV : Finite(V)
  requires finiteW : Finite(W)
  requires weights : w : Ω → ℝ
  requires subsetV : V ⊆ Ω
  requires subsetW : W ⊆ Ω
  requires disjoint : Disjoint(V, W)
  shows realSetSum(V ∪ W, w) = (realSetSum(V, w):R) + (realSetSum(W, w):R)
proof
  have finite := Finite.union with finiteV, finiteW
  have subset : V ∪ W ⊆ Ω by simp
  have innerV := union2.subset_left at V, W
  have innerW := union2.subset_right at V, W
  have maskV := maskedWeight.function at Ω, V, w with weights
  have maskW := maskedWeight.function at Ω, W, w with weights
  have combined := weightAdd.function with maskV, maskW
  have absent := Disjoint.iff.forward with disjoint
  have split : ∀ y ∈ V ∪ W, w(y) = weightAdd(Ω, maskedWeight(Ω, V, w),
      maskedWeight(Ω, W, w))(y)
    intros y hy
    have member := subset with y, hy
    have valueReal := FunctionBetween.apply_closed with weights, member
    have added := weightAdd.value with maskV, maskW, member
    have alternatives := union2.membership.forward with hy
    cases alternatives with inV | inW
    . have notW := absent with y, inV
      have left := maskedWeight.inside at Ω, V, w, y with weights, member, inV
      have right := maskedWeight.outside at Ω, W, w, y with weights, member,
          notW
      rw [added, left, right]
      ring
    . have notV : ¬(y ∈ V)
        intro inV
        exact absent with y, inV, inW
      have left := maskedWeight.outside at Ω, V, w, y with weights, member, notV
      have right := maskedWeight.inside at Ω, W, w, y with weights, member, inW
      rw [added, left, right]
      ring
  have same := realSetSum.congr with weights, combined, subset, split
  have sumAdd := realSetSum.add with finite, maskV, maskW, subset
  have sumV := realSetSum.masked with finite, weights, subset, innerV
  have sumW := realSetSum.masked with finite, weights, subset, innerW
  rw [same, sumAdd, sumV, sumW]
  rfl

theorem realSetSum.difference (V S Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires inner : S ⊆ V
  shows realSetSum(V, w) = (realSetSum(S, w):R) + (realSetSum(V ∖ S, w):R)
proof
  have rest := difference.subset_left at V, S
  have finiteS := Finite.subset with finite, inner
  have finiteRest := Finite.subset with finite, rest
  have subsetS := Subset.transitive with inner, subset
  have subsetRest := Subset.transitive with rest, subset
  have disjoint := Disjoint.difference_right at V, S
  have union := difference.union2_of_subset with inner
  have sum := realSetSum.union_disjoint with finiteS, finiteRest, weights,
    subsetS, subsetRest, disjoint
  rw union at sum
  exact sum

theorem realSetSum.subset_le (V S Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires inner : S ⊆ V
  requires bounds : ∀ x ∈ V, (0:R) ≤ (w(x):R)
  shows (realSetSum(S, w):R) ≤ (realSetSum(V, w):R)
proof
  have rest := difference.subset_left at V, S
  have finiteS := Finite.subset with finite, inner
  have finiteRest := Finite.subset with finite, rest
  have subsetS := Subset.transitive with inner, subset
  have subsetRest := Subset.transitive with rest, subset
  have split := realSetSum.difference with finite, weights, subset, inner
  have restBounds : ∀ x ∈ V ∖ S, (0:R) ≤ (w(x):R)
    intros x hx
    have inV := rest with x, hx
    exact bounds with x, inV
  have restNonnegative := realSetSum.nonnegative with finiteRest, weights,
    subsetRest, restBounds
  have sumS := realSetSum.real with finiteS, weights, subsetS
  have sumRest := realSetSum.real with finiteRest, weights, subsetRest
  rw split
  linarith

theorem realSetSum.insert_member (V Ω w a : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  requires member : a ∈ V
  shows realSetSum(V, w) = (realSetSum(V ∖ {a}, w):R) + (w(a):R)
proof
  have rest := difference.subset_left at V, {a}
  have finiteRest := Finite.subset with finite, rest
  have subsetRest := Subset.transitive with rest, subset
  have inDomain := subset with a, member
  have fresh : ¬(a ∈ V ∖ {a}) by simp
  have restored := insert.restore with member
  have inserted := realSetSum.insert with finiteRest, weights, subsetRest,
      inDomain, fresh
  rw restored at inserted
  exact inserted

-- Masking by S and summing over V counts only the points of V ∩ S.
theorem realSetSum.masked_intersection (V S Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℝ
  requires subset : V ⊆ Ω
  shows realSetSum(V, maskedWeight(Ω, S, w)) = realSetSum(V ∩ S, w)
proof
  have masked := maskedWeight.function at Ω, S, w with weights
  have inner := intersection.subset_left at V, S
  have subsetMeet := Subset.transitive with inner, subset
  have vanishes : ∀ x ∈ V, ¬(x ∈ V ∩ S) → maskedWeight(Ω, S, w)(x) = (0:R)
    intros x hx outside
    have member := subset with x, hx
    have notS : ¬(x ∈ S)
      intro inS
      apply outside
      exact intersection.membership.backward with ⟨hx, inS⟩
    exact maskedWeight.outside with weights, member, notS
  have restricted := realSetSum.restrict with finite, masked, subset, inner,
      vanishes
  have agree : ∀ x ∈ V ∩ S, maskedWeight(Ω, S, w)(x) = w(x)
    intros x hx
    have member := subsetMeet with x, hx
    have inS := intersection.membership.forward with hx
    exact maskedWeight.inside with weights, member, inS.right
  have same := realSetSum.congr with masked, weights, subsetMeet, agree
  rw [restricted, same]
  rfl

-- The real indicator of S on Ω.
defgraph realIndicator (Ω S : Set) (x ∈ Ω) : ℝ := realNat(indicator(S, x))
proof
  have natural := indicator.natural at S, x
  exact realNat.real at indicator(S, x)

theorem realIndicator.inside (Ω S x : Set)
  requires member : x ∈ Ω
  requires inside : x ∈ S
  shows realIndicator(Ω, S)(x) = (1:R)
proof
  have value := realIndicator.value at Ω, S, x with member
  have one := indicator.member with inside
  rw [value, one, realNat.one]
  rfl

theorem realIndicator.outside (Ω S x : Set)
  requires member : x ∈ Ω
  requires outside : ¬(x ∈ S)
  shows realIndicator(Ω, S)(x) = (0:R)
proof
  have value := realIndicator.value at Ω, S, x with member
  have zero := indicator.absent with outside
  rw [value, zero, realNat.zero]
  rfl

theorem realIndicator.nonnegative (Ω S x : Set)
  requires member : x ∈ Ω
  shows (0:R) ≤ (realIndicator(Ω, S)(x):R)
proof
  have value := realIndicator.value at Ω, S, x with member
  have natural := indicator.natural at S, x
  have nonnegative := realNat.zero_le at indicator(S, x)
  rw value
  exact nonnegative

theorem realIndicator.le_one (Ω S x : Set)
  requires member : x ∈ Ω
  shows (realIndicator(Ω, S)(x):R) ≤ (1:R)
proof
  have alternatives : x ∈ S ∨ ¬(x ∈ S) by tauto
  cases alternatives with inside | outside
  . have one := realIndicator.inside with member, inside
    rw one
    exact realLe.reflexive with realOne.real
  . have zero := realIndicator.outside with member, outside
    rw zero
    have one := realZero.lt_one
    linarith

-- The indicator of S is the constant one masked by S, so its sum counts.
theorem realSetSum.indicator (V S Ω : Set)
  requires finite : Finite(V)
  requires subset : V ⊆ Ω
  shows realSetSum(V, realIndicator(Ω, S)) = (realNat(cardinality(V ∩ S)):R)
proof
  have oneReal := realOne.real
  have ones := constantFunction.function at Ω, ℝ, (1:R) with oneReal
  have indicator := realIndicator.function at Ω, S
  have masked := maskedWeight.function at Ω, S, constantFunction(Ω, ℝ,
      (1:R)) with ones
  have agree : ∀ x ∈ V, realIndicator(Ω, S)(x) =
      maskedWeight(Ω, S, constantFunction(Ω, ℝ, (1:R)))(x)
    intros x hx
    have member := subset with x, hx
    have value := realIndicator.value at Ω, S, x with member
    have maskValue := maskedWeight.value at Ω, S, constantFunction(Ω, ℝ,
        (1:R)), x with
      ones, member
    have one := constantFunction.apply at Ω, ℝ, x, (1:R) with member, oneReal
    have natural := indicator.natural at S, x
    have maskReal := realNat.real at indicator(S, x)
    rw [value, maskValue, one]
    ring
  have same := realSetSum.congr with indicator, masked, subset, agree
  have counted := realSetSum.masked_intersection at V, S, Ω,
    constantFunction(Ω, ℝ, (1:R)) with finite, ones, subset
  have inner := intersection.subset_left at V, S
  have finiteMeet := Finite.subset with finite, inner
  have subsetMeet := Subset.transitive with inner, subset
  have constant := realSetSum.constant at V ∩ S, Ω, (1:R) with finiteMeet,
      subsetMeet
  have natural := cardinality.nat with finiteMeet
  have countReal := realNat.real at cardinality(V ∩ S)
  rw [same, counted, constant]
  ring