BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq
theorem BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq :
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (r : (ι → ℝ) → ↑(Set.Ioi 0))
(π : BoxIntegral.Prepartition I),
∃ π',
π'.toPrepartition ≤ π ∧
π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion
This theorem states that, given a box `I` in `ℝⁿ`, a function `r : ℝⁿ → (0, ∞)`, and a prepartition `π` of `I`, there exists a tagged prepartition `π'` of `I` satisfying the following conditions:
* Each box of `π'` is included in some box of `π`.
* `π'` is a Henstock partition, meaning that for each box `J` in `π'`, the tag of `J` belongs to the closed interval corresponding to `J`.
* `π'` is subordinate to `r`, which means that each box `J` in `π'` is included in the closed ball with center at the tag of `J` and radius `r` evaluated at the tag of `J`.
* `π'` covers exactly the same part of `I` as `π`.
* The distortion of `π'` is equal to the distortion of `π`, where distortion refers to the maximum of distortions of its boxes.
More concisely: Given a box `I` in `ℝⁿ`, a function `r : ℝⁿ → (0, ∞)`, and a partition `π` of `I`, there exists a tagged Henstock partition `π'` of `I` subordinate to `r` that covers the same part of `I` as `π`, is a refinement of `π`, and has the same distortion as `π`.
|
BoxIntegral.Box.subbox_induction_on
theorem BoxIntegral.Box.subbox_induction_on :
∀ {ι : Type u_1} [inst : Fintype ι] {p : BoxIntegral.Box ι → Prop} (I : BoxIntegral.Box ι),
(∀ J ≤ I, (∀ J' ∈ BoxIntegral.Prepartition.splitCenter J, p J') → p J) →
(∀ z ∈ BoxIntegral.Box.Icc I,
∃ U ∈ nhdsWithin z (BoxIntegral.Box.Icc I),
∀ J ≤ I,
∀ (m : ℕ),
z ∈ BoxIntegral.Box.Icc J →
BoxIntegral.Box.Icc J ⊆ U →
(∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J) →
p I
The theorem states that if a property `p` holds for a box `I` in `ℝⁿ`, provided two conditions are met:
- The first condition is that when a smaller box `J` is contained within `I` and is split into `2 ^ n` boxes by hyperplanes passing through its center, if the property `p` holds for each of these split boxes, then it holds for `J`.
- The second condition is that for each point `z` in the closed interval representation of `I`, there exists a neighborhood `U` of `z` within that interval such that for every box `J` contained within `I` where `z` is in the closed interval representation of `J` which is a subset of `U`, and `J` is homothetic to `I` with a scaling factor of `1 / 2 ^ m` for some `m`, the property `p` holds for `J`.
Then the property `p` can be said to hold for the box `I`. There is a variant of this theorem which uses a different method of splitting the box.
More concisely: If a property `p` holds for a box `I` in `ℝⁿ`, and for all sub-boxes `J` of `I` that are homothetic to `I` with a scaling factor of `1 / 2 ^ m` and contain a point `z` in their closed interval representation, `p` holds for `J` given that it also holds for all sub-boxes obtained by splitting `J` into `2 ^ n` parts via hyperplanes through their centers, then `p` holds for `I`.
|
BoxIntegral.Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic
theorem BoxIntegral.Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic :
∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) (r : (ι → ℝ) → ↑(Set.Ioi 0)),
∃ π,
π.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 n-dimensional real space and a function `r` that maps from n-dimensional real space to the set of strictly positive real numbers, there exists a tagged partition `π` of the box `I` such that:
1. `π` is a Henstock partition, meaning that it is a partition of the box `I` that satisfies the Henstock condition - a specific condition in integration theory related to the tagging of the partition;
2. `π` is subordinate to the function `r`, meaning that the diameter of each set in the partition is less than or equal to the value of `r` at any point in the set;
3. For each box `J` in the partition `π`, there exists a non-negative integer `m` such that the length of the interval in the `i`-th dimension of the box `J` is equal to the length of the interval in the `i`-th dimension of the box `I` divided by 2 raised to the power of `m`; and
4. The distortion of the partition `π` is equal to the distortion of the box `I`.
This theorem implies that the Henstock filter is nontrivial, hence the Henstock integral, a kind of integral that generalizes the Riemann integral while being easier to define than the Lebesgue integral, is well-defined.
More concisely: Given a function `r` mapping n-dimensional real space to strictly positive real numbers, there exists a Henstock partition `π` of the n-dimensional box `I` that is subordinate to `r`, tagged, and has equal distortion to `I`.
|