integralSum_biUnionTagged — Mathlib

English

The integral sum over a bi-union of tagged partitions equals the sum over the partitions.

Русский

Сумма интеграла по би-объединению тегированных разбиений равна сумме по разбиениям.

LaTeX

$$$\forall f:\; (π: TaggedPrepartition I) (π': Prepartition I) (π'.IsPartition)\Rightarrow \mathrm{integralSum}(f, vol, π.biUnionPrepartition π') = \mathrm{integralSum}(f, vol, π)$$$

Lean4

theorem integralSum_biUnionTagged (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : Prepartition I)
    (πi : ∀ J, TaggedPrepartition J) :
    integralSum f vol (π.biUnionTagged πi) = ∑ J ∈ π.boxes, integralSum f vol (πi J) :=
  by
  refine (π.sum_biUnion_boxes _ _).trans <| sum_congr rfl fun J hJ => sum_congr rfl fun J' hJ' => ?_
  rw [π.tag_biUnionTagged hJ hJ']

Похожие утверждения