mathlib3 documentation

analysis.box_integral.partition.additive

Box additive functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We say that a function f : box ι → M from boxes in ℝⁿ to a commutative additive monoid M is box additive on subboxes of I₀ : with_top (box ι) if for any box J, ↑J ≤ I₀, and a partition π of J, f J = ∑ J' in π.boxes, f J'. We use I₀ : with_top (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

source
structure box_integral.box_additive_map (ι : Type u_3) (M : Type u_4) [add_comm_monoid M] (I : with_top (box_integral.box ι)) :
Type (max u_3 u_4)

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 : with_bot (box ι): the value I = ⊤ corresponds to functions box additive on the whole space.

Instances for box_integral.box_additive_map
source
@[protected, instance]
def box_integral.box_additive_map.has_coe_to_fun {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} :
has_coe_to_fun (box_integral.box_additive_map ι M I₀) (λ (_x : box_integral.box_additive_map ι M I₀), box_integral.box ι → M)
Equations
source
@[simp]
theorem box_integral.box_additive_map.to_fun_eq_coe {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} (f : box_integral.box_additive_map ι M I₀) :
f.to_fun = ⇑f
source
@[simp]
theorem box_integral.box_additive_map.coe_mk {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} (f : box_integral.box ι → M) (h : ∀ (J : box_integral.box ι), ↑J ≤ I₀ → ∀ (π : box_integral.prepartition J), π.is_partition → π.boxes.sum (λ (Ji : box_integral.box ι), f Ji) = f J) :
⇑{to_fun := f, sum_partition_boxes' := h} = f
source
theorem box_integral.box_additive_map.coe_injective {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} :
function.injective (λ (f : box_integral.box_additive_map ι M I₀) (x : box_integral.box ι), ⇑f x)
source
@[simp]
theorem box_integral.box_additive_map.coe_inj {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} {f g : box_integral.box_additive_map ι M I₀} :
⇑f = ⇑g ↔ f = g
source
theorem box_integral.box_additive_map.sum_partition_boxes {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} {I : box_integral.box ι} (f : box_integral.box_additive_map ι M I₀) (hI : ↑I ≤ I₀) {π : box_integral.prepartition I} (h : π.is_partition) :
π.boxes.sum (λ (J : box_integral.box ι), ⇑f J) = ⇑f I
source
@[simp]
theorem box_integral.box_additive_map.has_zero_zero_apply {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} :
⇑0 = 0
source
@[protected, instance]
def box_integral.box_additive_map.has_zero {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} :
has_zero (box_integral.box_additive_map ι M I₀)
Equations
source
@[protected, instance]
def box_integral.box_additive_map.inhabited {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} :
inhabited (box_integral.box_additive_map ι M I₀)
Equations
source
@[protected, instance]
def box_integral.box_additive_map.has_add {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} :
has_add (box_integral.box_additive_map ι M I₀)
Equations
source
@[protected, instance]
def box_integral.box_additive_map.has_smul {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} {R : Type u_3} [monoid R] [distrib_mul_action R M] :
has_smul R (box_integral.box_additive_map ι M I₀)
Equations
source
@[protected, instance]
def box_integral.box_additive_map.add_comm_monoid {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} :
add_comm_monoid (box_integral.box_additive_map ι M I₀)
Equations
source
@[simp]
theorem box_integral.box_additive_map.map_split_add {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} {I : box_integral.box ι} (f : box_integral.box_additive_map ι M I₀) (hI : ↑I ≤ I₀) (i : ι) (x : ℝ) :
option.elim 0 ⇑f (I.split_lower i x) + option.elim 0 ⇑f (I.split_upper i x) = ⇑f I
source
@[simp]
theorem box_integral.box_additive_map.restrict_apply {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} (f : box_integral.box_additive_map ι M I₀) (I : with_top (box_integral.box ι)) (hI : I ≤ I₀) (ᾰ : box_integral.box ι) :
⇑(f.restrict I hI) ᾰ = ⇑f ᾰ
source
def box_integral.box_additive_map.restrict {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} (f : box_integral.box_additive_map ι M I₀) (I : with_top (box_integral.box ι)) (hI : I ≤ I₀) :
box_integral.box_additive_map ι M I

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

Equations
source
def box_integral.box_additive_map.of_map_split_add {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] [fintype ι] (f : box_integral.box ι → M) (I₀ : with_top (box_integral.box ι)) (hf : ∀ (I : box_integral.box ι), ↑I ≤ I₀ → ∀ {i : ι} {x : ℝ}, x ∈ set.Ioo (I.lower i) (I.upper i) → option.elim 0 f (I.split_lower i x) + option.elim 0 f (I.split_upper i x) = f I) :
box_integral.box_additive_map ι M I₀

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

Equations
source
def box_integral.box_additive_map.map {ι : Type u_1} {M : Type u_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] {I₀ : with_top (box_integral.box ι)} (f : box_integral.box_additive_map ι M I₀) (g : M →+ N) :
box_integral.box_additive_map ι 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
source
@[simp]
theorem box_integral.box_additive_map.map_apply {ι : Type u_1} {M : Type u_2} {N : Type u_3} [add_comm_monoid M] [add_comm_monoid N] {I₀ : with_top (box_integral.box ι)} (f : box_integral.box_additive_map ι M I₀) (g : M →+ N) :
⇑(f.map g) = ⇑g ∘ ⇑f
source
theorem box_integral.box_additive_map.sum_boxes_congr {ι : Type u_1} {M : Type u_2} [add_comm_monoid M] {I₀ : with_top (box_integral.box ι)} {I : box_integral.box ι} [finite ι] (f : box_integral.box_additive_map ι M I₀) (hI : ↑I ≤ I₀) {π₁ π₂ : box_integral.prepartition I} (h : π₁.Union = π₂.Union) :
π₁.boxes.sum (λ (J : box_integral.box ι), ⇑f J) = π₂.boxes.sum (λ (J : box_integral.box ι), ⇑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.

source
noncomputable def box_integral.box_additive_map.to_smul {ι : Type u_1} {I₀ : with_top (box_integral.box ι)} {E : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] (f : box_integral.box_additive_map ι ℝ I₀) :
box_integral.box_additive_map ι (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
source
@[simp]
theorem box_integral.box_additive_map.to_smul_apply {ι : Type u_1} {I₀ : with_top (box_integral.box ι)} {E : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] (f : box_integral.box_additive_map ι ℝ I₀) (I : box_integral.box ι) (x : E) :
⇑(⇑(f.to_smul) I) x = ⇑f I • x
source
@[simp]
theorem box_integral.box_additive_map.upper_sub_lower_apply {n : ℕ} {G : Type u} [add_comm_group G] (I₀ : box_integral.box (fin (n + 1))) (i : fin (n + 1)) (f : ℝ → box_integral.box (fin n) → G) (fb : ↥(set.Icc (I₀.lower i) (I₀.upper i)) → box_integral.box_additive_map (fin n) G ↑(I₀.face i)) (hf : ∀ (x : ℝ) (hx : x ∈ set.Icc (I₀.lower i) (I₀.upper i)) (J : box_integral.box (fin n)), f x J = ⇑(fb ⟨x, hx⟩) J) (J : box_integral.box (fin (n + 1))) :
⇑(box_integral.box_additive_map.upper_sub_lower I₀ i f fb hf) J = f (J.upper i) (J.face i) - f (J.lower i) (J.face i)
source
def box_integral.box_additive_map.upper_sub_lower {n : ℕ} {G : Type u} [add_comm_group G] (I₀ : box_integral.box (fin (n + 1))) (i : fin (n + 1)) (f : ℝ → box_integral.box (fin n) → G) (fb : ↥(set.Icc (I₀.lower i) (I₀.upper i)) → box_integral.box_additive_map (fin n) G ↑(I₀.face i)) (hf : ∀ (x : ℝ) (hx : x ∈ set.Icc (I₀.lower i) (I₀.upper i)) (J : box_integral.box (fin n)), f x J = ⇑(fb ⟨x, hx⟩) J) :
box_integral.box_additive_map (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 λ J, f (J.upper i) (J.face i) - f (J.lower i) (J.face i) is box-additive on subboxes of I₀.

Equations