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' ∈ π.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
A function on Box ι is called box additive if for every box J and a partition π of J
we have f J = ∑ Ji ∈ π.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.
- toFun : BoxIntegral.Box ι → M
The function underlying this additive map.
- sum_partition_boxes' : ∀ (J : BoxIntegral.Box ι), ↑J ≤ I → ∀ (π : BoxIntegral.Prepartition J), π.IsPartition → ∑ Ji ∈ π.boxes, self.toFun Ji = self.toFun J
A function on Box ι is called box additive if for every box J and a partition π of J
we have f J = ∑ Ji ∈ π.boxes, f Ji.
Equations
- BoxIntegral.«term_→ᵇᵃ_» = Lean.ParserDescr.trailingNode `BoxIntegral.«term_→ᵇᵃ_» 25 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᵇᵃ ") (Lean.ParserDescr.cat `term 0))
A function on Box ι is called box additive if for every box J and a partition π of J
we have f J = ∑ Ji ∈ π.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.
Equations
- One or more equations did not get rendered due to their size.
Equations
- BoxIntegral.BoxAdditiveMap.instFunLikeBox = { coe := BoxIntegral.BoxAdditiveMap.toFun, coe_injective' := ⋯ }
Equations
- BoxIntegral.BoxAdditiveMap.instZero = { zero := { toFun := 0, sum_partition_boxes' := ⋯ } }
Equations
- BoxIntegral.BoxAdditiveMap.instInhabited = { default := 0 }
Equations
- BoxIntegral.BoxAdditiveMap.instAdd = { add := fun (f g : BoxIntegral.BoxAdditiveMap ι M I₀) => { toFun := ⇑f + ⇑g, sum_partition_boxes' := ⋯ } }
Equations
- BoxIntegral.BoxAdditiveMap.instSMulOfDistribMulAction = { smul := fun (r : R) (f : BoxIntegral.BoxAdditiveMap ι M I₀) => { toFun := r • ⇑f, sum_partition_boxes' := ⋯ } }
Equations
- BoxIntegral.BoxAdditiveMap.instAddCommMonoid = Function.Injective.addCommMonoid (fun (f : BoxIntegral.BoxAdditiveMap ι M I₀) (x : BoxIntegral.Box ι) => f x) ⋯ ⋯ ⋯ ⋯
If f is box-additive on subboxes of I₀, then it is box-additive on subboxes of any
I ≤ I₀.
Equations
- f.restrict I hI = { toFun := ⇑f, sum_partition_boxes' := ⋯ }
If f : Box ι → M is box additive on partitions of the form split I i x, then it is box
additive.
Equations
- BoxIntegral.BoxAdditiveMap.ofMapSplitAdd f I₀ hf = { toFun := f, sum_partition_boxes' := ⋯ }
If g : M → N is an additive map and f is a box additive map, then g ∘ f is a box additive
map.
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 ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J.
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
- f.toSMul = f.map (↑(ContinuousLinearMap.lsmul ℝ ℝ)).toAddMonoidHom
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.