Documentation

Mathlib.Analysis.BoxIntegral.Partition.Additive

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

structure BoxIntegral.BoxAdditiveMap (ι : Type u_3) (M : Type u_4) [AddCommMonoid M] (I : WithTop (BoxIntegral.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 ∈ π.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
    theorem BoxIntegral.BoxAdditiveMap.sum_partition_boxes' {ι : Type u_3} {M : Type u_4} [AddCommMonoid M] {I : WithTop (BoxIntegral.Box ι)} (self : BoxIntegral.BoxAdditiveMap ι M I) (J : BoxIntegral.Box ι) :
    J I∀ (π : BoxIntegral.Prepartition J), π.IsPartitionJiπ.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
    Instances For

      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.
      Instances For
        Equations
        • BoxIntegral.BoxAdditiveMap.instFunLikeBox = { coe := BoxIntegral.BoxAdditiveMap.toFun, coe_injective' := }
        @[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), π.IsPartitionJiπ.boxes, f Ji = f J) :
        { toFun := f, sum_partition_boxes' := h } = f
        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 : π.IsPartition) :
        Jπ.boxes, f J = f I
        @[simp]
        theorem BoxIntegral.BoxAdditiveMap.instZero_zero_apply {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} :
        0 = 0
        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
        @[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) (I.splitLower i x) + Option.elim' 0 (⇑f) (I.splitUpper 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 ι) :
        (f.restrict I hI) a = f a

        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' := }
        Instances For
          def BoxIntegral.BoxAdditiveMap.ofMapSplitAdd {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] [Finite ι] (f : BoxIntegral.Box ιM) (I₀ : WithTop (BoxIntegral.Box ι)) (hf : ∀ (I : BoxIntegral.Box ι), I I₀∀ {i : ι} {x : }, x Set.Ioo (I.lower i) (I.upper i)Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I) :

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

          Equations
          Instances For
            @[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) :
            (f.map 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) :

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

            Equations
            • f.map g = { toFun := g f, sum_partition_boxes' := }
            Instances For
              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 : π₁.iUnion = π₂.iUnion) :
              Jπ₁.boxes, f J = Jπ₂.boxes, 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 ∈ π₁.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
              Instances For
                @[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) :
                (f.toSMul 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 (I₀.lower i) (I₀.upper i))BoxIntegral.BoxAdditiveMap (Fin n) G (I₀.face i)) (hf : ∀ (x : ) (hx : x Set.Icc (I₀.lower i) (I₀.upper i)) (J : BoxIntegral.Box (Fin n)), f x J = (fb x, hx) J) (J : BoxIntegral.Box (Fin (n + 1))) :
                (BoxIntegral.BoxAdditiveMap.upperSubLower I₀ i f fb hf) J = f (J.upper i) (J.face i) - f (J.lower i) (J.face 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 (I₀.lower i) (I₀.upper i))BoxIntegral.BoxAdditiveMap (Fin n) G (I₀.face i)) (hf : ∀ (x : ) (hx : x Set.Icc (I₀.lower i) (I₀.upper i)) (J : BoxIntegral.Box (Fin n)), f x J = (fb x, 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.
                Instances For