Documentation

Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Induction on subboxes #

In this file we prove (see BoxIntegral.Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic) that for every box I in ℝⁿ and a function r : ℝⁿ → ℝ positive on I there exists a tagged partition π of I such that

Later we will use this lemma to prove that the Henstock filter is nontrivial, hence the Henstock integral is well-defined.

Tags #

partition, tagged partition, Henstock integral

Split a box in ℝⁿ into 2 ^ n boxes by hyperplanes passing through its center.

Equations
Instances For
    @[simp]
    theorem BoxIntegral.Prepartition.mem_splitCenter {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} :
    J BoxIntegral.Prepartition.splitCenter I ∃ (s : Set ι), I.splitCenterBox s = J
    theorem BoxIntegral.Prepartition.upper_sub_lower_of_mem_splitCenter {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} {J : BoxIntegral.Box ι} (h : J BoxIntegral.Prepartition.splitCenter I) (i : ι) :
    J.upper i - J.lower i = (I.upper i - I.lower i) / 2
    theorem BoxIntegral.Box.subbox_induction_on {ι : Type u_1} [Fintype ι] {p : BoxIntegral.Box ιProp} (I : BoxIntegral.Box ι) (H_ind : JI, (∀ J'BoxIntegral.Prepartition.splitCenter J, p J')p J) (H_nhds : zBoxIntegral.Box.Icc I, UnhdsWithin z (BoxIntegral.Box.Icc I), JI, ∀ (m : ), z BoxIntegral.Box.Icc JBoxIntegral.Box.Icc J U(∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m)p J) :
    p I

    Let p be a predicate on Box ι, let I be a box. Suppose that the following two properties hold true.

    • Consider a smaller box J ≤ I. The hyperplanes passing through the center of J split it into 2 ^ n boxes. If p holds true on each of these boxes, then it true on J.
    • For each z in the closed box I.Icc there exists a neighborhood U of z within I.Icc such that for every box J ≤ I such that z ∈ J.Icc ⊆ U, if J is homothetic to I with a coefficient of the form 1 / 2 ^ m, then p is true on J.

    Then p I is true. See also BoxIntegral.Box.subbox_induction_on' for a version using BoxIntegral.Box.splitCenterBox instead of BoxIntegral.Prepartition.splitCenter.

    theorem BoxIntegral.Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) (r : (ι)(Set.Ioi 0)) :
    ∃ (π : BoxIntegral.TaggedPrepartition I), π.IsPartition π.IsHenstock π.IsSubordinate r (∀ Jπ, ∃ (m : ), ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) π.distortion = I.distortion

    Given a box I in ℝⁿ and a function r : ℝⁿ → (0, ∞), there exists a tagged partition π of I such that

    • π is a Henstock partition;
    • π is subordinate to r;
    • each box in π is homothetic to I with coefficient of the form 1 / 2 ^ m.

    This lemma implies that the Henstock filter is nontrivial, hence the Henstock integral is well-defined.

    theorem BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (r : (ι)(Set.Ioi 0)) (π : BoxIntegral.Prepartition I) :
    ∃ (π' : BoxIntegral.TaggedPrepartition I), π'.toPrepartition π π'.IsHenstock π'.IsSubordinate r π'.distortion = π.distortion π'.iUnion = π.iUnion

    Given a box I in ℝⁿ, a function r : ℝⁿ → (0, ∞), and a prepartition π of I, there exists a tagged prepartition π' of I such that

    • each box of π' is included in some box of π;
    • π' is a Henstock partition;
    • π' is subordinate to r;
    • π' covers exactly the same part of I as π;
    • the distortion of π' is equal to the distortion of π.

    Given a prepartition π of a box I and a function r : ℝⁿ → (0, ∞), π.toSubordinate r is a tagged partition π' such that

    • each box of π' is included in some box of π;
    • π' is a Henstock partition;
    • π' is subordinate to r;
    • π' covers exactly the same part of I as π;
    • the distortion of π' is equal to the distortion of π.
    Equations
    • π.toSubordinate r = .choose
    Instances For
      theorem BoxIntegral.Prepartition.toSubordinate_toPrepartition_le {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι)(Set.Ioi 0)) :
      (π.toSubordinate r).toPrepartition π
      theorem BoxIntegral.Prepartition.isHenstock_toSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι)(Set.Ioi 0)) :
      (π.toSubordinate r).IsHenstock
      theorem BoxIntegral.Prepartition.isSubordinate_toSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι)(Set.Ioi 0)) :
      (π.toSubordinate r).IsSubordinate r
      @[simp]
      theorem BoxIntegral.Prepartition.distortion_toSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι)(Set.Ioi 0)) :
      (π.toSubordinate r).distortion = π.distortion
      @[simp]
      theorem BoxIntegral.Prepartition.iUnion_toSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι)(Set.Ioi 0)) :
      (π.toSubordinate r).iUnion = π.iUnion
      def BoxIntegral.TaggedPrepartition.unionComplToSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)(Set.Ioi 0)) :

      Given a tagged prepartition π₁, a prepartition π₂ that covers exactly I \ π₁.iUnion, and a function r : ℝⁿ → (0, ∞), returns the union of π₁ and π₂.toSubordinate r. This partition π has the following properties:

      • π is a partition, i.e. it covers the whole I;
      • π₁.boxes ⊆ π.boxes;
      • π.tag J = π₁.tag J whenever J ∈ π₁;
      • π is Henstock outside of π₁: π.tag J ∈ J.Icc whenever J ∈ π, J ∉ π₁;
      • π is subordinate to r outside of π₁;
      • the distortion of π is equal to the maximum of the distortions of π₁ and π₂.
      Equations
      • π₁.unionComplToSubordinate π₂ hU r = π₁.disjUnion (π₂.toSubordinate r)
      Instances For
        theorem BoxIntegral.TaggedPrepartition.isPartition_unionComplToSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)(Set.Ioi 0)) :
        (π₁.unionComplToSubordinate π₂ hU r).IsPartition
        @[simp]
        theorem BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)(Set.Ioi 0)) :
        (π₁.unionComplToSubordinate π₂ hU r).boxes = π₁.boxes (π₂.toSubordinate r).boxes
        @[simp]
        theorem BoxIntegral.TaggedPrepartition.iUnion_unionComplToSubordinate_boxes {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)(Set.Ioi 0)) :
        (π₁.unionComplToSubordinate π₂ hU r).iUnion = I
        @[simp]
        theorem BoxIntegral.TaggedPrepartition.distortion_unionComplToSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = I \ π₁.iUnion) (r : (ι)(Set.Ioi 0)) :
        (π₁.unionComplToSubordinate π₂ hU r).distortion = max π₁.distortion π₂.distortion