toBoxAdditive — Mathlib

English

The map μ ↦ μ.real defines a box-additive map on boxes: J ↦ μ.real J, with the partition-sum property over finite box partitions.

Русский

Отображение μ ↦ μ.real задаёт боково‑добавляемое отображение на коробках: J ↦ μ.real J, c его свойство суммы по разбиениям коробок.

LaTeX

$$$\\text{toBoxAdditive}(\\mu) : ι \\to^b π ℝ$ is box-additive with sum partition property, i.e., for any J and partition π, ∑_{K \\in π.boxes} μ.real(K) = μ.real(J).$$$

Lean4

/-- If `μ` is a locally finite measure on `ℝⁿ`, then `fun J ↦ μ.real J` is a box-additive
function. -/
@[simps]
def toBoxAdditive [Finite ι] (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure μ] : ι →ᵇᵃ[⊤] ℝ
    where
  toFun J := μ.real J
  sum_partition_boxes' J _ π hπ := by rw [← π.measure_iUnion_toReal, hπ.iUnion_eq]

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