Box additive functions

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

rectangular box, additive function

structure BoxIntegral.BoxAdditiveMap (ι : Type u_3) (M : Type u_4) [AddCommMonoid M] (I : WithTop (BoxIntegral.Box ι)) : Type (max u_3 u_4)

• toFun : BoxIntegral.Box ι → M
• sum_partition_boxes' : ∀ (J : BoxIntegral.Box ι), ↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), BoxIntegral.Prepartition.IsPartition π → (Finset.sum π.boxes fun Ji => BoxIntegral.BoxAdditiveMap.toFun s Ji) = BoxIntegral.BoxAdditiveMap.toFun s J

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.

def BoxIntegral.«term_→ᵇᵃ_» : Lean.TrailingParserDescr

Equations

• BoxIntegral.«term_→ᵇᵃ_» = Lean.ParserDescr.trailingNode `BoxIntegral.term_→ᵇᵃ_ 25 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᵇᵃ ") (Lean.ParserDescr.cat `term 0))

def BoxIntegral.«term_→ᵇᵃ[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

instance BoxIntegral.BoxAdditiveMap.instFunLikeBoxAdditiveMapBox {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} : FunLike (BoxIntegral.BoxAdditiveMap ι M I₀) (BoxIntegral.Box ι) fun x => M

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoxIntegral.BoxAdditiveMap.coe_mk {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} (f : BoxIntegral.Box ι → M) (h : ∀ (J : BoxIntegral.Box ι), ↑J ≤ I₀ → ∀ (π : BoxIntegral.Prepartition J), BoxIntegral.Prepartition.IsPartition π → (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} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} : Function.Injective fun f x => ↑f x

theorem BoxIntegral.BoxAdditiveMap.coe_inj {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {f : BoxIntegral.BoxAdditiveMap ι M I₀} {g : BoxIntegral.BoxAdditiveMap ι M I₀} : ↑f = ↑g ↔ f = g

theorem BoxIntegral.BoxAdditiveMap.sum_partition_boxes {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {I : BoxIntegral.Box ι} (f : BoxIntegral.BoxAdditiveMap ι M I₀) (hI : ↑I ≤ I₀) {π : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.IsPartition π) : (Finset.sum π.boxes fun J => ↑f J) = ↑f I

@[simp]

theorem BoxIntegral.BoxAdditiveMap.instZeroBoxAdditiveMap_zero_apply {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} : ↑0 = 0

instance BoxIntegral.BoxAdditiveMap.instZeroBoxAdditiveMap {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} : Zero (BoxIntegral.BoxAdditiveMap ι M I₀)

Equations

• One or more equations did not get rendered due to their size.

instance BoxIntegral.BoxAdditiveMap.instInhabitedBoxAdditiveMap {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} : Inhabited (BoxIntegral.BoxAdditiveMap ι M I₀)

Equations

• BoxIntegral.BoxAdditiveMap.instInhabitedBoxAdditiveMap = { default := 0 }

instance BoxIntegral.BoxAdditiveMap.instAddBoxAdditiveMap {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} : Add (BoxIntegral.BoxAdditiveMap ι M I₀)

Equations

• One or more equations did not get rendered due to their size.

instance BoxIntegral.BoxAdditiveMap.instSMulBoxAdditiveMap {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {R : Type u_4} [Monoid R] [DistribMulAction R M] : SMul R (BoxIntegral.BoxAdditiveMap ι M I₀)

Equations

• One or more equations did not get rendered due to their size.

instance BoxIntegral.BoxAdditiveMap.instAddCommMonoidBoxAdditiveMap {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} : AddCommMonoid (BoxIntegral.BoxAdditiveMap ι M I₀)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoxIntegral.BoxAdditiveMap.map_split_add {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {I : BoxIntegral.Box ι} (f : BoxIntegral.BoxAdditiveMap ι M I₀) (hI : ↑I ≤ I₀) (i : ι) (x : ℝ) : Option.elim' 0 (↑f) (BoxIntegral.Box.splitLower I i x) + Option.elim' 0 (↑f) (BoxIntegral.Box.splitUpper I i x) = ↑f I

@[simp]

theorem BoxIntegral.BoxAdditiveMap.restrict_apply {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} (f : BoxIntegral.BoxAdditiveMap ι M I₀) (I : WithTop (BoxIntegral.Box ι)) (hI : I ≤ I₀) (a : BoxIntegral.Box ι) : ↑(BoxIntegral.BoxAdditiveMap.restrict f I hI) a = ↑f a

def BoxIntegral.BoxAdditiveMap.restrict {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} (f : BoxIntegral.BoxAdditiveMap ι M I₀) (I : WithTop (BoxIntegral.Box ι)) (hI : I ≤ I₀) : BoxIntegral.BoxAdditiveMap ι M I

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

Equations

• One or more equations did not get rendered due to their size.

def BoxIntegral.BoxAdditiveMap.ofMapSplitAdd {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] [Fintype ι] (f : BoxIntegral.Box ι → M) (I₀ : WithTop (BoxIntegral.Box ι)) (hf : ∀ (I : BoxIntegral.Box ι), ↑I ≤ I₀ → ∀ {i : ι} {x : ℝ}, x ∈ Set.Ioo (BoxIntegral.Box.lower I i) (BoxIntegral.Box.upper I i) → Option.elim' 0 f (BoxIntegral.Box.splitLower I i x) + Option.elim' 0 f (BoxIntegral.Box.splitUpper I i x) = f I) : BoxIntegral.BoxAdditiveMap ι M I₀

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BoxIntegral.BoxAdditiveMap.map_apply {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] {I₀ : WithTop (BoxIntegral.Box ι)} (f : BoxIntegral.BoxAdditiveMap ι M I₀) (g : M →+ N) : ↑(BoxIntegral.BoxAdditiveMap.map f g) = ↑g ∘ ↑f

def BoxIntegral.BoxAdditiveMap.map {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] {I₀ : WithTop (BoxIntegral.Box ι)} (f : BoxIntegral.BoxAdditiveMap ι M I₀) (g : M →+ N) : BoxIntegral.BoxAdditiveMap ι N I₀

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

Equations

• One or more equations did not get rendered due to their size.

theorem BoxIntegral.BoxAdditiveMap.sum_boxes_congr {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {I : BoxIntegral.Box ι} [Finite ι] (f : BoxIntegral.BoxAdditiveMap ι M I₀) (hI : ↑I ≤ I₀) {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : BoxIntegral.Prepartition.iUnion π₁ = BoxIntegral.Prepartition.iUnion π₂) : (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₀ : WithTop (BoxIntegral.Box ι)} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : BoxIntegral.BoxAdditiveMap ι ℝ I₀) : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] E) I₀

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.

Equations

• BoxIntegral.BoxAdditiveMap.toSMul f = BoxIntegral.BoxAdditiveMap.map f (LinearMap.toAddMonoidHom ↑(ContinuousLinearMap.lsmul ℝ ℝ))

@[simp]

theorem BoxIntegral.BoxAdditiveMap.toSMul_apply {ι : Type u_1} {I₀ : WithTop (BoxIntegral.Box ι)} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : BoxIntegral.BoxAdditiveMap ι ℝ I₀) (I : BoxIntegral.Box ι) (x : E) : ↑(↑(BoxIntegral.BoxAdditiveMap.toSMul f) I) x = ↑f I • x

@[simp]

theorem BoxIntegral.BoxAdditiveMap.upperSubLower_apply {n : ℕ} {G : Type u} [AddCommGroup G] (I₀ : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) (f : ℝ → BoxIntegral.Box (Fin n) → G) (fb : ↑(Set.Icc (BoxIntegral.Box.lower I₀ i) (BoxIntegral.Box.upper I₀ i)) → BoxIntegral.BoxAdditiveMap (Fin n) G ↑(BoxIntegral.Box.face I₀ i)) (hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (BoxIntegral.Box.lower I₀ i) (BoxIntegral.Box.upper I₀ i)) (J : BoxIntegral.Box (Fin n)), f x J = ↑(fb { val := x, property := hx }) J) (J : BoxIntegral.Box (Fin (n + 1))) : ↑(BoxIntegral.BoxAdditiveMap.upperSubLower I₀ i f fb hf) J = f (BoxIntegral.Box.upper J i) (BoxIntegral.Box.face J i) - f (BoxIntegral.Box.lower J i) (BoxIntegral.Box.face J i)

def BoxIntegral.BoxAdditiveMap.upperSubLower {n : ℕ} {G : Type u} [AddCommGroup G] (I₀ : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) (f : ℝ → BoxIntegral.Box (Fin n) → G) (fb : ↑(Set.Icc (BoxIntegral.Box.lower I₀ i) (BoxIntegral.Box.upper I₀ i)) → BoxIntegral.BoxAdditiveMap (Fin n) G ↑(BoxIntegral.Box.face I₀ i)) (hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (BoxIntegral.Box.lower I₀ i) (BoxIntegral.Box.upper I₀ i)) (J : BoxIntegral.Box (Fin n)), 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₀.

Equations

• One or more equations did not get rendered due to their size.