# Documentation

We say that a function f : Box ι → M from boxes in ℝⁿ to a commutative additive monoid M is box additive on subboxes of I₀ : WithTop (Box ι) if for any box J, ↑J ≤ I₀, and a partition π of J, f J = ∑ J' in π.boxes, f J'. We use I₀ : WithTop (Box ι) instead of I₀ : Box ι to use the same definition for functions box additive on subboxes of a box and for functions box additive on all boxes.

Examples of box-additive functions include the measure of a box and the integral of a fixed integrable function over a box.

In this file we define box-additive functions and prove that a function such that f J = f (J ∩ {x | x i < y}) + f (J ∩ {x | y ≤ x i}) is box-additive.

### Tags #

structure BoxIntegral.BoxAdditiveMap (ι : Type u_3) (M : Type u_4) [] (I : ) :
Type (max u_3 u_4)
• toFun : M
• sum_partition_boxes' : ∀ (J : ), J I∀ (π : ), (Finset.sum π.boxes fun Ji => ) =

A function on Box ι is called box additive if for every box J and a partition π of J we have f J = ∑ Ji in π.boxes, f Ji. A function is called box additive on subboxes of I : Box ι if the same property holds for J ≤ I. We formalize these two notions in the same definition using I : WithBot (Box ι): the value I = ⊤ corresponds to functions box additive on the whole space.

Instances For
Instances For
Instances For
instance BoxIntegral.BoxAdditiveMap.instFunLikeBoxAdditiveMapBox {ι : Type u_1} {M : Type u_2} [] {I₀ : } :
FunLike () () fun x => M
@[simp]
theorem BoxIntegral.BoxAdditiveMap.coe_mk {ι : Type u_1} {M : Type u_2} [] {I₀ : } (f : M) (h : ∀ (J : ), J I₀∀ (π : ), (Finset.sum π.boxes fun Ji => f Ji) = f J) :
{ toFun := f, sum_partition_boxes' := h } = f
theorem BoxIntegral.BoxAdditiveMap.coe_injective {ι : Type u_1} {M : Type u_2} [] {I₀ : } :
Function.Injective fun f x => f x
theorem BoxIntegral.BoxAdditiveMap.coe_inj {ι : Type u_1} {M : Type u_2} [] {I₀ : } {f : } {g : } :
f = g f = g
theorem BoxIntegral.BoxAdditiveMap.sum_partition_boxes {ι : Type u_1} {M : Type u_2} [] {I₀ : } {I : } (f : ) (hI : I I₀) {π : } :
(Finset.sum π.boxes fun J => f J) = f I
@[simp]
theorem BoxIntegral.BoxAdditiveMap.instZeroBoxAdditiveMap_zero_apply {ι : Type u_1} {M : Type u_2} [] {I₀ : } :
0 = 0
instance BoxIntegral.BoxAdditiveMap.instZeroBoxAdditiveMap {ι : Type u_1} {M : Type u_2} [] {I₀ : } :
Zero ()
instance BoxIntegral.BoxAdditiveMap.instSMulBoxAdditiveMap {ι : Type u_1} {M : Type u_2} [] {I₀ : } {R : Type u_4} [] [] :
SMul R ()
@[simp]
theorem BoxIntegral.BoxAdditiveMap.map_split_add {ι : Type u_1} {M : Type u_2} [] {I₀ : } {I : } (f : ) (hI : I I₀) (i : ι) (x : ) :
Option.elim' 0 (f) () + Option.elim' 0 (f) () = f I
@[simp]
theorem BoxIntegral.BoxAdditiveMap.restrict_apply {ι : Type u_1} {M : Type u_2} [] {I₀ : } (f : ) (I : ) (hI : I I₀) (a : ) :
↑() a = f a
def BoxIntegral.BoxAdditiveMap.restrict {ι : Type u_1} {M : Type u_2} [] {I₀ : } (f : ) (I : ) (hI : I I₀) :

If f is box-additive on subboxes of I₀, then it is box-additive on subboxes of any I ≤ I₀.

Instances For
def BoxIntegral.BoxAdditiveMap.ofMapSplitAdd {ι : Type u_1} {M : Type u_2} [] [] (f : M) (I₀ : ) (hf : ∀ (I : ), I I₀∀ {i : ι} {x : }, x Set.Ioo () ()Option.elim' 0 f () + Option.elim' 0 f () = f I) :

If f : Box ι → M is box additive on partitions of the form split I i x, then it is box additive.

Instances For
@[simp]
theorem BoxIntegral.BoxAdditiveMap.map_apply {ι : Type u_1} {M : Type u_2} {N : Type u_3} [] [] {I₀ : } (f : ) (g : M →+ N) :
= g f
def BoxIntegral.BoxAdditiveMap.map {ι : Type u_1} {M : Type u_2} {N : Type u_3} [] [] {I₀ : } (f : ) (g : M →+ N) :

If g : M → N is an additive map and f is a box additive map, then g ∘ f is a box additive map.

Instances For
theorem BoxIntegral.BoxAdditiveMap.sum_boxes_congr {ι : Type u_1} {M : Type u_2} [] {I₀ : } {I : } [] (f : ) (hI : I I₀) {π₁ : } {π₂ : } :
(Finset.sum π₁.boxes fun J => f J) = Finset.sum π₂.boxes fun J => f J

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 ∑ J in π₁.boxes, f J = ∑ J in π₂.boxes, f J.

def BoxIntegral.BoxAdditiveMap.toSMul {ι : Type u_1} {I₀ : } {E : Type u_4} [] (f : ) :

If f is a box-additive map, then so is the map sending I to the scalar multiplication by f I as a continuous linear map from E to itself.

Instances For
@[simp]
theorem BoxIntegral.BoxAdditiveMap.toSMul_apply {ι : Type u_1} {I₀ : } {E : Type u_4} [] (f : ) (I : ) (x : E) :
↑() x = f I x
@[simp]
theorem BoxIntegral.BoxAdditiveMap.upperSubLower_apply {n : } {G : Type u} [] (I₀ : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) (f : G) (fb : ↑(Set.Icc () ())BoxIntegral.BoxAdditiveMap (Fin n) G ↑()) (hf : ∀ (x : ) (hx : x Set.Icc () ()) (J : ), f x J = ↑(fb { val := x, property := hx }) J) (J : BoxIntegral.Box (Fin (n + 1))) :
↑() J = f () () - f () ()
def BoxIntegral.BoxAdditiveMap.upperSubLower {n : } {G : Type u} [] (I₀ : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) (f : G) (fb : ↑(Set.Icc () ())BoxIntegral.BoxAdditiveMap (Fin n) G ↑()) (hf : ∀ (x : ) (hx : x Set.Icc () ()) (J : ), f x J = ↑(fb { val := x, property := hx }) J) :
BoxIntegral.BoxAdditiveMap (Fin (n + 1)) G I₀

Given a box I₀ in ℝⁿ⁺¹, f x : Box (Fin n) → G is a family of functions indexed by a real x and for x ∈ [I₀.lower i, I₀.upper i], f x is box-additive on subboxes of the i-th face of I₀, then fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i) is box-additive on subboxes of I₀.

Instances For