BoxIntegral.BoxAdditiveMap.sum_partition_boxes
theorem BoxIntegral.BoxAdditiveMap.sum_partition_boxes :
∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {I : BoxIntegral.Box ι}
(f : BoxIntegral.BoxAdditiveMap ι M I₀),
↑I ≤ I₀ → ∀ {π : BoxIntegral.Prepartition I}, π.IsPartition → (π.boxes.sum fun J => f J) = f I
This theorem states that for any type `ι`, and `M` which is an additive commutative monoid, given a 'top-attached' box `I₀` of type `ι` and a box `I` of the same type, and a box-additive map `f` from `I₀` to `M`, if `I` is less than or equal to `I₀`, then for any prepartition `π` of `I` which is also a partition, the sum of `f` applied to each box in `π` is equal to `f` applied to `I`. In other words, the value of the box-additive map on the entire box `I` is equal to the sum of its values on the smaller boxes of the partition.
More concisely: For any additive commutative monoid M, type ι, top-attached box I₀ of type ι, box I with I ≤ I₀, and box-additive map f from I₀ to M, if π is a partition of I that is also a prepartition, then ∑(π)(i) (f i) = f (∑(ι) i), where ∑(π)(i) denotes the sum of boxes in partition π that map to i under the canonical bijection from I to π.
|
BoxIntegral.BoxAdditiveMap.sum_boxes_congr
theorem BoxIntegral.BoxAdditiveMap.sum_boxes_congr :
∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {I : BoxIntegral.Box ι}
[inst_1 : Finite ι] (f : BoxIntegral.BoxAdditiveMap ι M I₀),
↑I ≤ I₀ →
∀ {π₁ π₂ : BoxIntegral.Prepartition I},
π₁.iUnion = π₂.iUnion → (π₁.boxes.sum fun J => f J) = π₂.boxes.sum fun J => f J
This theorem states that if `f` is a box-additive function on subboxes of `I` and `π₁`, `π₂` are two prepartitions of `I` that cover the same part of `I`, then the sum of the function `f` applied to the boxes of `π₁` equals the sum of the function `f` applied to the boxes of `π₂`. The box-additive function `f` is defined on a space that includes `I` and possibly more (`I₀`). The theorem also requires that the box `I` is enclosed within `I₀`. This result holds true in the context where we are working with a finite-dimensional space (indicated by `Finite ι`) and for any commutative monoid `M`.
More concisely: If `f` is a box-additive function on subboxes of `I`, enclosed in `I₀`, and `π₁` and `π₂` are two partitions of `I` covering the same subinterval of `I` in a finite-dimensional space `ι` and commutative monoid `M`, then the sum of `f` applied to the boxes of `π₁` equals the sum of `f` applied to the boxes of `π₂`.
|