BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq
theorem BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι}
{π : BoxIntegral.TaggedPrepartition I} [inst_4 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E}
{vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {c : NNReal} {ε : ℝ} [inst_5 : CompleteSpace F]
(h : BoxIntegral.Integrable I l f vol),
0 < ε →
l.MemBaseSet I c (h.convergenceR ε c) π →
∀ {π₀ : BoxIntegral.Prepartition I},
π.iUnion = π₀.iUnion →
dist (BoxIntegral.integralSum f vol π) (π₀.boxes.sum fun J => BoxIntegral.integral J l f vol) ≤ ε
The **Henstock-Sacks inequality** theorem states that for a function `r` mapping from ℝⁿ to the open interval (0, ∞), if for any tagged partition of `I` subordinate to `r`, the integral sum of a function `f` over this partition differs from the integral of `f` by at most `ε`, then for any tagged prepartition `π` subordinate to `r`, the integral sum of `f` over this prepartition differs from the integral of `f` over the part of `I` covered by `π` by at most `ε`.
This theorem is more precisely stated in Lean 4 with the use of `BoxIntegral.Integrable.convergenceR` instead of a predicate assumption on `r`, and `BoxIntegral.IntegrationParams.MemBaseSet` instead of the phrase "subordinate to `r`" due to additional requirements such as the partition being a Henstock partition or having a bounded distortion. Also, an extra argument `π₀ : prepartition I` and an assumption `π.Union = π₀.Union` is used instead of `π.to_prepartition`.
More concisely: If for a function `r` mapping from ℝⁿ to (0, ∞) and a function `f`, the integral sum of `f` over any tagged Henstock partition of `I` with respect to `r` is within `ε` of the integral of `f` over the interval, then the integral sum of `f` over any tagged prepartition of `I` subordinate to `r` with the same properties is also within `ε` of the integral of `f` over the part of `I` covered by the prepartition.
|
BoxIntegral.Integrable.to_subbox
theorem BoxIntegral.Integrable.to_subbox :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I J : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
[inst_5 : CompleteSpace F], BoxIntegral.Integrable I l f vol → J ≤ I → BoxIntegral.Integrable J l f vol
This theorem states that if a function `f` is integrable on a given box `I` (in the sense of the box integral), then it remains integrable when considered over any subbox `J` of `I`. This holds for any function from `ι -> ℝ` to `E`, where `ι` is any type, `E` is a normed additively commutative group, and `F` is a complete normed additively commutative group. The box `J` is considered a subbox of `I` if it is less than or equal to `I` in the order defined on boxes.
More concisely: If a function is integrable over a box in the sense of the box integral, then it is integrable over any subbox.
|
BoxIntegral.integrable_iff_cauchy_basis
theorem BoxIntegral.integrable_iff_cauchy_basis :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
[inst_5 : CompleteSpace F],
BoxIntegral.Integrable I l f vol ↔
∀ ε > 0,
∃ r,
(∀ (c : NNReal), l.RCond (r c)) ∧
∀ (c₁ c₂ : NNReal) (π₁ π₂ : BoxIntegral.TaggedPrepartition I),
l.MemBaseSet I c₁ (r c₁) π₁ →
π₁.IsPartition →
l.MemBaseSet I c₂ (r c₂) π₂ →
π₂.IsPartition → dist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ≤ ε
The theorem states that, for any types ι, E, F, given that E and F are both normed additive commutative groups and real vector spaces, and F is a complete space, along with a box 'I' of type 'BoxIntegral.Box ι' with ι being finite, integration parameters 'l', a function 'f' from ι → ℝ to E, and a volume 'vol' of type 'BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤', a function is integrable with respect to these parameters and volume if and only if for all positive real numbers ε, there exists a function 'r' from non-negative real numbers (NNReal) to real numbers such that the function 'r' satisfies the R-condition for all 'c' in NNReal, and for any two non-negative real numbers 'c₁' and 'c₂' and any two tagged pre-partitions 'π₁' and 'π₂' of the box 'I', if both 'π₁' and 'π₂' are partitions of 'I' that satisfy the base set condition with respect to 'c₁', 'r c₁', 'c₂', and 'r c₂' respectively, then the distance between the integral sums of 'f' with respect to 'vol' over 'π₁' and 'π₂' is less than or equal to ε. In other words, the integral sums of the function form a Cauchy net, which is a generalization of the Cauchy sequence concept for sets with a more general structure than the real numbers.
More concisely: A function from a finite type to a real vector space is integrable with respect to given parameters and a complete, normed additive commutative group if and only if its integral sums over all tagged pre-partitions form a Cauchy net.
|
BoxIntegral.HasIntegral.neg
theorem BoxIntegral.HasIntegral.neg :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
BoxIntegral.HasIntegral I l f vol y → BoxIntegral.HasIntegral I l (-f) vol (-y)
The theorem `BoxIntegral.HasIntegral.neg` states that for any given type `ι`, a normed add commutative group `E` and a normed space over `ℝ` for `E`, a normed add commutative group `F` and another normed space over `ℝ` for `F`, along with a box integral `I` over `ι`, a finite type over `ι`, an integration parameter `l`, a function `f` from `ι → ℝ` to `E`, a volume form `vol` as an additive map from the box integral to the top element of the continuous linear map from `E` to `F`, and a value `y` in `F`. If the box integral `I` integrates `f` with respect to `vol` to `y`, then the box integral `I` also integrates the negation of `f` with respect to `vol` to the negation of `y`.
More concisely: If a box integral over a type `ι` integrates a function `f` from `ι` to a normed space `E` over `ℝ` with respect to a volume form `vol` to a value `y` in another normed space `F`, then it also integrates the negation of `f` with respect to `vol` to the negation of `y`.
|
BoxIntegral.hasIntegral_iff
theorem BoxIntegral.hasIntegral_iff :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
BoxIntegral.HasIntegral I l f vol y ↔
∀ ε > 0,
∃ r,
(∀ (c : NNReal), l.RCond (r c)) ∧
∀ (c : NNReal) (π : BoxIntegral.TaggedPrepartition I),
l.MemBaseSet I c (r c) π → π.IsPartition → dist (BoxIntegral.integralSum f vol π) y ≤ ε
This theorem states the `ε`-`δ` definition of having an integral in the context of box integrals. Given a type `ι`, normed add commutative group `E`, normed space over the real numbers `ℝ` and `E`, `F` as another normed add commutative group, a normed space over the real numbers `ℝ` and `F`, a box `I`, an integration parameter `l`, a function `f` from `ι` to `ℝ` to `E`, a volume function `vol`, and a target value `y`, the function `f` has an integral over box `I` with parameters `l` and volume `vol` equal to `y` if and only if for every positive `ε`, there exists a function `r` from nonnegative real numbers to real numbers such that for every nonnegative real number `c`, `l.RCond (r c)` holds and for every tagged prepartition `π` of `I`, if `π` is a base set for `I` under `c` and `r c` and `π` is a partition, then the distance between the integral sum of `f` with volume `vol` over `π` and `y` is less than or equal to `ε`.
More concisely: For a given normed add commutative group `E`, normed space `F` over `ℝ`, box `I`, integration parameter `l`, function `f` from `ι` to `ℝ`, volume function `vol`, and target value `y`, `f` has an integral over box `I` with parameters `l` and volume `vol` equal to `y` if and only if for every `ε > 0`, there exists a function `r` such that for all `c > 0` and tagged prepartitions `π` of `I` that are a base set, partition, and satisfy `l.RCond (r c)`, the integral sum of `f` over `π` with volume `vol` is within `ε` of `y`.
|
BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet
theorem BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
{c₁ c₂ : NNReal} {ε₁ ε₂ : ℝ} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : BoxIntegral.Integrable I l f vol),
0 < ε₁ →
0 < ε₂ →
l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁ →
l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂ →
π₁.iUnion = π₂.iUnion →
dist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ≤ ε₁ + ε₂
This theorem is a form of the **Henstock-Sacks inequality**. It states that given functions `r₁` and `r₂` that map from ℝⁿ to the positive real numbers (0, ∞), such that for any tagged partition of `I` subordinate to `rₖ` (`k=1,2`), the integral sum of a function `f` over this partition differs from the integral of `f` by at most `εₖ`. Then, for any two tagged prepartitions `π₁` and `π₂` which are subordinate to `r₁` and `r₂` respectively and cover the same part of `I`, the integral sums of `f` over these prepartitions differ from each other by at most `ε₁ + ε₂`.
The theorem in Lean is a more precise formulation of this inequality. It replaces the predicate assumption on `r` with `BoxIntegral.Integrable.convergenceR`, and uses `BoxIntegral.IntegrationParams.MemBaseSet` instead of "subordinate to `r`" to account for additional requirements like being a Henstock partition or having a bounded distortion. The theorem provides that if the integrable function `f`, integration parameter `l`, measures `vol`, and two nonnegative numbers `c₁` and `c₂` satisfy certain conditions, then the distance between the integral sums of `f` with respect to two prepartitions `π₁` and `π₂` is less than or equal to `ε₁ + ε₂`.
More concisely: Given integrable functions `f` and tagged prepartitions `π₁` and `π₂` subordinate to `r₁` and `r₂` respectively, satisfying certain conditions, the integral sums of `f` over `π₁` and `π₂` differ by at most the sum of their individual error bounds.
|
BoxIntegral.HasIntegral.add
theorem BoxIntegral.HasIntegral.add :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f g : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
{y y' : F},
BoxIntegral.HasIntegral I l f vol y →
BoxIntegral.HasIntegral I l g vol y' → BoxIntegral.HasIntegral I l (f + g) vol (y + y')
This theorem states that for any two functions `f` and `g` that both have a box integral over a given box `I` with respect to a given set of integration parameters `l` and a certain volume form `vol`, if `f` has integral `y` and `g` has integral `y'`, then the function `f + g` (which is the sum of `f` and `g`) has an integral that is `y + y'` (the sum of the integrals of `f` and `g`). This is basically an application of the linearity of integration.
More concisely: The integral of the sum of two functions `f` and `g` over a box `I` with respect to a volume form `vol` and integration parameters `l` is equal to the sum of their integrals.
|
BoxIntegral.HasIntegral.integral_eq
theorem BoxIntegral.HasIntegral.integral_eq :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
BoxIntegral.HasIntegral I l f vol y → BoxIntegral.integral I l f vol = y
This theorem states that for any types `ι`, `E`, `F`, given that `E` and `F` are normed add commutative groups and also normed spaces over the real numbers ℝ, given a box `I` in the `ι`-dimensional space, an integration parameter `l`, a function `f` mapping from `ι → ℝ` to `E`, a volume function `vol` mapping from `ι` to a linear map from `E` to `F` and a value `y` in `F`, if `f` has an integral over the box `I` with respect to the volume `vol` that equals `y` under the integration parameter `l`, then the actual integral of `f` over the box `I` with respect to `vol` under `l` is indeed `y`.
More concisely: If `f : ι -> ℝ -> E`, `vol : ι -> E -> F`, `I : box ι`, `l : ℝ`, `y : F` satisfy `∫x in I, vol x . f x = y` (integral of `f` with respect to `vol` over `I` under `l` equals `y`), then `y = ∫x in I, vol x . f x` (the actual integral of `f` over `I` with respect to `vol` under `l` is equal to `y`).
|
BoxIntegral.Integrable.hasIntegral
theorem BoxIntegral.Integrable.hasIntegral :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
BoxIntegral.Integrable I l f vol → BoxIntegral.HasIntegral I l f vol (BoxIntegral.integral I l f vol)
The theorem `BoxIntegral.Integrable.hasIntegral` asserts that for any given types `ι`, `E`, and `F`, together with instances of `E` and `F` as normed add commutative groups and normed spaces over real numbers, an integrable box `I` of type `ι`, a finite type instance for `ι`, an integration parameter `l`, a function `f` mapping `ι → ℝ` to `E`, and a volume `vol` represented as a box additive map from `ι` to `E →L[ℝ] F`, if the function `f` is integrable over the box `I` with respect to the volume `vol` and the integration parameter `l`, then the integral of the function `f` over the box `I` is well-defined, i.e., `f` has an integral over `I` with respect to `vol` and `l`, and this integral is equal to the box integral of `f` over `I` with respect to `vol` and `l`.
More concisely: For any integrable function `f` from a box `I` to the normed space `E` over real numbers, with respect to a normed additive group `ι`, a finite type instance for `ι`, a normed space `F`, an integration parameter `l`, and a box additive map `vol` from `ι` to `E →ℝ[ℝ] F`, the integral of `f` over `I` with respect to `vol` and `l` exists and equals the box integral of `f` over `I` with respect to `vol` and `l`.
|
BoxIntegral.integrable_of_continuousOn
theorem BoxIntegral.integrable_of_continuousOn :
∀ {ι : Type u} {E : Type v} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : Fintype ι]
(l : BoxIntegral.IntegrationParams) [inst_3 : CompleteSpace E] {I : BoxIntegral.Box ι} {f : (ι → ℝ) → E},
ContinuousOn f (BoxIntegral.Box.Icc I) →
∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ],
BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul
The theorem `BoxIntegral.integrable_of_continuousOn` states that for any finite-dimensional, real-valued continuous function `f` defined on a closed interval `I`, and for any locally finite measure `μ`, the function `f` is box-integrable with respect to the measure `μ`. This is true for any integration parameters `l` and holds in the context of a normed additive commutative group `E` that is also a complete normed space over the real numbers. In other words, if the function `f` is continuous on the closed box `I`, it is guaranteed to be box-integrable with respect to any locally finite measure.
More concisely: If `f` is a continuous, real-valued function on a closed interval `I` and `μ` is a locally finite measure, then `f` is box-integrable with respect to `μ`.
|
BoxIntegral.Integrable.sum_integral_congr
theorem BoxIntegral.Integrable.sum_integral_congr :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
[inst_5 : CompleteSpace F],
BoxIntegral.Integrable I l f vol →
∀ {π₁ π₂ : BoxIntegral.Prepartition I},
π₁.iUnion = π₂.iUnion →
(π₁.boxes.sum fun J => BoxIntegral.integral J l f vol) =
π₂.boxes.sum fun J => BoxIntegral.integral J l f vol
This theorem states that if a function `f` is integrable on a box `I`, then the function that maps each subbox `J` to the integral of `f` over `J` is box-additive. Specifically, if `π₁` and `π₂` are two prepartitions of `I` such that the union of the boxes in `π₁` is the same as the union of the boxes in `π₂`, then the sum of the integrals of `f` over the boxes in `π₁` equals the sum of the integrals of `f` over the boxes in `π₂`. The theorem pertains to multiple dimensions, indicated by the type variable `ι`, and the function `f` maps each point in a box to a vector in a normed vector space `E`, while the integral produces a vector in another normed vector space `F`. This theorem is an unbundled version of the theorem `BoxIntegral.Integrable.toBoxAdditive`.
More concisely: If `f` is an integrable function over a box `I` in a normed vector space `E`, then the function mapping each subbox `J` to the integral of `f` over `J` is additive with respect to partitions of `I` in the sense that the sum of integrals over a partition `π₁` equals the sum of integrals over a partition `π₂` if and only if the unions of their boxes are equal.
|
BoxIntegral.Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity
theorem BoxIntegral.Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
BoxIntegral.Integrable I l f vol →
Filter.Tendsto (fun π => (BoxIntegral.integralSum f vol π.1, BoxIntegral.integralSum f vol π.2))
(l.toFilter I ×ˢ l.toFilter I ⊓ Filter.principal {π | π.1.iUnion = π.2.iUnion}) (uniformity F)
The theorem `BoxIntegral.Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity` states that if a function `f` is integrable on a box `I` along a given set of integration parameters `l`, then the integral sums of `f` over two sufficiently fine tagged prepartitions `π₁` and `π₂` (that is, their level of detail is judged by the filter corresponding to the integration parameters `l` applied to the box `I`) which cover the same part of `I`, become arbitrarily close to each other in the limit. This is asserted in the sense of the uniformity filter on F, which represents the idea of being "infinitesimally close" in the uniform space F. This theorem formalizes a fundamental property of the integral, that it doesn't change under refinement of the partition, in a precise rigorous way suitable for generalizations beyond standard Euclidean spaces.
More concisely: Given an integrable function `f` on a box `I` with respect to parameters `l`, and two tagged partitions `π₁` and `π₂` of `I` with matching subintervals, the integral sums of `f` over `π₁` and `π₂` approach each other as their level of detail increases, according to the uniformity filter on the space of integrable functions.
|
BoxIntegral.norm_integral_le_of_norm_le
theorem BoxIntegral.norm_integral_le_of_norm_le :
∀ {ι : Type u} {E : Type v} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {I : BoxIntegral.Box ι}
[inst_2 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {g : (ι → ℝ) → ℝ},
(∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ g x) →
∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
BoxIntegral.Integrable I l g μ.toBoxAdditive.toSMul →
‖BoxIntegral.integral I l f μ.toBoxAdditive.toSMul‖ ≤ BoxIntegral.integral I l g μ.toBoxAdditive.toSMul
This theorem states that for any normed additively commutative group `E` and normed real vector space, given a box `I`, integration parameters `l`, two functions `f` from the box to `E` and `g` from the box to real numbers, and a measure `μ` that is locally finite, if for all `x` in the box `I`, the norm of `f(x)` is less than or equal to `g(x)`, and if `g` is integrable, then the norm of the integral of `f` over `I` using the measure `μ` is less than or equal to the integral of `g` over `I` using the same measure. This theorem essentially gives an upper bound on the norm of the integral of a function.
More concisely: For any normed additively commutative group `E`, normed real vector space, box `I`, locally finite measure `μ`, integrable function `g` from `I` to real numbers, and functions `f` from `I` to `E` with `||f(x)|| ≤ g(x)` for all `x` in `I`, the norm of the integral of `f` over `I` using `μ` is less than or equal to the integral of `g` over `I` using the same measure.
|
BoxIntegral.Integrable.tendsto_integralSum_toFilteriUnion_single
theorem BoxIntegral.Integrable.tendsto_integralSum_toFilteriUnion_single :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I J : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
[inst_5 : CompleteSpace F],
BoxIntegral.Integrable I l f vol →
∀ (hJ : J ≤ I),
Filter.Tendsto (BoxIntegral.integralSum f vol) (l.toFilteriUnion I (BoxIntegral.Prepartition.single I J hJ))
(nhds (BoxIntegral.integral J l f vol))
The theorem `BoxIntegral.Integrable.tendsto_integralSum_toFilteriUnion_single` states that for any given box `I` and a subbox `J` of `I` (`J ≤ I`), if a function `f` is integrable on `I`, then the integral sums of `f` over tagged prepartitions that precisely cover the subbox `J` tend to the integral of `f` over `J` along a given integration parameter `l`. This trend is followed along the filter formed by the union of `l` and the singleton prepartition containing `J`. In essence, this theorem is about the convergence of an integral sum over a partition towards the integral value over a continuous domain.
More concisely: Given a box `I`, a subbox `J ≤ I`, and an integrable function `f` on `I`, the integral sums of `f` over tagged partitions covering `J` converge to the integral of `f` over `J` as the mesh size goes to zero along the filter formed by the union of `l` and the singleton partition containing `J`.
|
BoxIntegral.Integrable.tendsto_integralSum_sum_integral
theorem BoxIntegral.Integrable.tendsto_integralSum_sum_integral :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
[inst_5 : CompleteSpace F],
BoxIntegral.Integrable I l f vol →
∀ (π₀ : BoxIntegral.Prepartition I),
Filter.Tendsto (BoxIntegral.integralSum f vol) (l.toFilteriUnion I π₀)
(nhds (π₀.boxes.sum fun J => BoxIntegral.integral J l f vol))
This theorem states that given a tagged prepartition `π` of a box `I` in some finite-dimensional space, such that the union of `π` equals the union of another prepartition `π₀` of the same box, then the sum of the integrals of a function `f` over all the boxes in `π` tends to the sum of integrals of `f` over the boxes of `π₀`. This is under the conditions that `f` is an integrable function (according to the integration parameters `l` and a volume form `vol`) on the box `I`, with `f` mapping from ℝ^ι to a normed additive commutative group `E`, and `vol` mapping from `E` to a normed additive commutative group `F`, both `E` and `F` are complete spaces over reals. The theorem is asserting a property of convergence in topology, where the notion of convergence is defined by the 'Filter.Tendsto' predicate which says that the 'limit of the integral sum' function at the filter `l.toFilteriUnion I π₀` is a neighborhood of the sum of integrals over the boxes of `π₀`.
More concisely: Given integrable functions `f` and volume forms `vol` on a finite-dimensional box `I`, if tagged partitions `π` and `π₀` of `I` have the same union and `π�'s sum of integrals of `f` tends to the limit in `F` as the partition size goes to zero according to `l`, then the sum of integrals of `f` over `π₀` is the limit of the sum of integrals over `π`.
|
BoxIntegral.integral_nonneg
theorem BoxIntegral.integral_nonneg :
∀ {ι : Type u} {I : BoxIntegral.Box ι} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} {g : (ι → ℝ) → ℝ},
(∀ x ∈ BoxIntegral.Box.Icc I, 0 ≤ g x) →
∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ],
0 ≤ BoxIntegral.integral I l g μ.toBoxAdditive.toSMul
This theorem states that the integral of a nonnegative function with respect to a volume generated by a locally-finite measure is nonnegative. More specifically, for any type `ι`, any `BoxIntegral.Box I` of type `ι`, any integration parameters `l`, any function `g` that maps a real-valued function on `ι` to a real number, if `g x` is nonnegative for all `x` in the closed box `BoxIntegral.Box.Icc I`, and any measure `μ` that is a locally finite measure, then the box integral of `g` with respect to `μ.toBoxAdditive.toSMul` is nonnegative.
More concisely: For any locally finite measure `μ` and nonnegative function `g` on a closed box `I`, the box integral of `g` with respect to `μ` is nonnegative.
|
BoxIntegral.HasIntegral.integrable
theorem BoxIntegral.HasIntegral.integrable :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
BoxIntegral.HasIntegral I l f vol y → BoxIntegral.Integrable I l f vol
This theorem states that for any function `f` from a real-valued vector to a normed add-commutative group `E` and any `vol` (which is a box-additive map from `ι` to the continuous linear map from `E` to a normed add-commutative group `F`), if `f` has an integral over a given box `I` according to a set of integration parameters `l`, that yields an element `y` of `F`, then `f` is integrable over box `I` with respect to the volume element `vol` and the integration parameters `l`. This holds for any given types `ι`, `E`, `F` and for any `I`, `l`, `f`, `vol`, `y` which satisfy the conditions described.
More concisely: If a real-valued function `f` over a box `I` has an integral `y` with respect to a box-additive volume map `vol` and integration parameters `l` in the sense of Lean 4, then `f` is integrable over `I` with respect to `vol` and `l`.
|
BoxIntegral.HasIntegral.tendsto
theorem BoxIntegral.HasIntegral.tendsto :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
BoxIntegral.HasIntegral I l f vol y →
Filter.Tendsto (BoxIntegral.integralSum f vol) (l.toFilteriUnion I ⊤) (nhds y)
The theorem `BoxIntegral.HasIntegral.tendsto` states that if a function `f` from a set of real numbers (specified by the Cartesian product of the box `I` with itself) to a normed additive commutative group `E` has a box integral `y` with respect to a volume form `vol` under a specified set of integration parameters `l`, then the sequence of box integral sums of `f` with respect to `vol` converges to `y` in the box `I`. In other words, the function `BoxIntegral.integralSum f vol` tends to `y` as we get closer to `I` in the sense of the filter `l.toFilteriUnion I ⊤` (which represents getting closer to `I` by taking smaller and smaller boxes). This is a reinterpretation of the definition of `BoxIntegral.HasIntegral` in terms of the limit concept `Filter.Tendsto`.
More concisely: If a real-valued function on a compact box with respect to a volume form has a box integral, then the sequence of box integral sums converges to the integral as the box size approaches zero.
|
BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet
theorem BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι}
{π : BoxIntegral.TaggedPrepartition I} [inst_4 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E}
{vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {c : NNReal} {ε : ℝ} [inst_5 : CompleteSpace F]
(h : BoxIntegral.Integrable I l f vol),
0 < ε →
l.MemBaseSet I c (h.convergenceR ε c) π →
dist (BoxIntegral.integralSum f vol π) (π.boxes.sum fun J => BoxIntegral.integral J l f vol) ≤ ε
The **Henstock-Sacks inequality** states that given a function `r : ℝⁿ → (0, ∞)` which ensures that the integral sum of a function `f` over any tagged partition of `I` subordinate to `r` deviates from the actual integral of `f` by no more than a real number `ε`, then for any tagged prepartition `π` also subordinate to `r`, the integral sum of `f` over this prepartition will differ from the integral of `f` over the part of `I` covered by `π` by at most `ε`.
In the actual implementation, the theorem `BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet` uses more specific terms: `BoxIntegral.Integrable.convergenceR` replaces a simple predicate assumption on `r`, and `BoxIntegral.IntegrationParams.MemBaseSet` is used instead of the phrase "subordinate to `r`", to account for additional characteristics like being a Henstock partition or having bounded distortion. This theorem belongs to a normed space over the reals, and it relates the distance between the integral sum of a function over a prepartition and the sum of integrals over the boxes of the prepartition to a real number `ε`, under certain conditions.
More concisely: Given a function `r : ℝⁿ → (0, ∞)` and an integrable function `f` on the real interval `I`, if the integral sum of `f` over any tagged prepartition `π` subordinate to `r` satisfies the condition `∥∫(π, f) - ∫(I, f)∥ ≤ ε`, then the integral sum of `f` over any sub-prepartition of `π` also satisfies `∥∫(π', f) - ∑(i, f(tₗₙ(i))) ∥ ≤ ε`, where `π'` is a sub-prepartition of `π` and `tₗₙ` is the tag function of `π`.
|
BoxIntegral.HasIntegral.of_mul
theorem BoxIntegral.HasIntegral.of_mul :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F}
(a : ℝ),
(∀ (ε : ℝ),
0 < ε →
∃ r,
(∀ (c : NNReal), l.RCond (r c)) ∧
∀ (c : NNReal) (π : BoxIntegral.TaggedPrepartition I),
l.MemBaseSet I c (r c) π → π.IsPartition → dist (BoxIntegral.integralSum f vol π) y ≤ a * ε) →
BoxIntegral.HasIntegral I l f vol y
This theorem states that for any real number `a` and a function `f` from a box in ℝⁿ to a normed add commutative group `E`, if you can find a real number `r` such that, for any non-negative real number `c` and any tagged pre-partition of the box `I`, if the tagged pre-partition belongs to the base set defined by the integration parameters `l`, the `r c`, and lies within `I`, and if it forms a partition, then the distance between the integral sum of the function `f` under the volume `vol` over the tagged pre-partition and an element `y` of another normed add commutative group `F` is less than or equal to `a` times any positive real number `ε`, then `f` has an integral over the box `I` with respect to the volume `vol` that equals `y` according to the integration parameters `l`. This theorem allows for more natural proofs of estimates of the form `a * ε` rather than `ε` on the right-hand side of the condition for `f` to have an integral.
More concisely: If a real-valued function `f` on a box in ℝⁿ with respect to a volume `vol` satisfies the condition that for any `ε > 0`, there exists an `r` such that the difference between the integral sum of `f` over any tagged pre-partition in the base set with respect to `vol` and any element `y` in another normed add commutative group `F` is less than or equal to `a * ε`, then `f` has an integral over the box equal to `y` with respect to `vol`.
|
BoxIntegral.Integrable.cauchy_map_integralSum_toFilteriUnion
theorem BoxIntegral.Integrable.cauchy_map_integralSum_toFilteriUnion :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
BoxIntegral.Integrable I l f vol →
∀ (π₀ : BoxIntegral.Prepartition I),
Cauchy (Filter.map (BoxIntegral.integralSum f vol) (l.toFilteriUnion I π₀))
For any given function `f` that is integrable on a certain box `I` along a given integration parameter `l`, the theorem states that for any fixed subset `s` of `I` that can be represented as a finite union of boxes, the sums of the integrals of `f` over tagged prepartitions that exactly cover `s` form a Cauchy sequence along `l`.
In other words, if we view the sums of the integrals as a sequence indexed by these prepartitions, this sequence is a Cauchy sequence. Here, a sequence is considered to be a Cauchy sequence if for any given positive tolerance, there is a point in the sequence beyond which all subsequent elements are pairwise within that tolerance. The "Cauchy sequence" here is captured by the topological notion of a Cauchy filter.
More concisely: For any integrable function `f` on a box `I` and any finite union of sub-boxes `s` of `I`, the sequence of integrals of `f` over tagged partitions that exactly cover `s` forms a Cauchy sequence with respect to the integration parameter.
|
BoxIntegral.hasIntegral_const
theorem BoxIntegral.hasIntegral_const :
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
{l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} (c : E),
BoxIntegral.HasIntegral I l (fun x => c) vol ((vol I) c)
This theorem states that for any given type `ι`, and any given normed add commutative groups `E` and `F` over the real numbers with `E` and `F` also being a normed space over the real numbers. If `I` is a box integral (a multi-dimensional generalization of an interval), `l` is some integration parameters, `vol` is a box additive map (linear maps that preserve addition) between `ι` and the continuous linear mappings from `E` to `F`, and `c` is an element of `E`, then the integral of the constant function `c` over the box `I` with respect to `vol` is equal to `vol` applied to `I` and `c`. In other words, the integral of a constant function over a box integral is simply the volume of the box times the constant.
More concisely: For any normed add commutative groups `E` and `F` over the real numbers, any type `ι`, any box integral `I` over `ι`, integration parameters `l`, a box additive map `vol` from `ι` to continuous linear mappings from `E` to `F`, and any `c` in `E`, the integral of the constant function `c` over `I` with respect to `vol` equals `vol(I)(c)`.
|