BoxIntegral.HasIntegral.congr_ae
theorem BoxIntegral.HasIntegral.congr_ae :
∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
{l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {y : E} {f g : (ι → ℝ) → E}
{μ : MeasureTheory.Measure (ι → ℝ)} [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul y →
(μ.restrict ↑I).ae.EventuallyEq f g →
l.bRiemann = false → BoxIntegral.HasIntegral I l g μ.toBoxAdditive.toSMul y
This theorem states that if a function `f` has an integral `y` on a box `I` with respect to a locally finite measure `μ`, and there is another function `g` which is almost everywhere equal to `f` on `I`, then `g` also has the same integral `y` on `I`. This is under the condition that the parameter `l.bRiemann` is false, which indicates that the Riemann condition is not satisfied, therefore the integral is being calculated using the Lebesgue or more general method.
This theorem is critical in measure theory and integration, where it is often necessary to replace a function by another function that is equal almost everywhere.
More concisely: If functions `f` and `g` are equal almost everywhere on a measurable set `I` with respect to a locally finite measure `μ`, and `f` has an integral `y` on `I`, then `g` also has the same integral `y` on `I` under the condition that the Riemann integral is not used (`l.bRiemann = false`).
|
BoxIntegral.hasIntegralIndicatorConst
theorem BoxIntegral.hasIntegralIndicatorConst :
∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
(l : BoxIntegral.IntegrationParams),
l.bRiemann = false →
∀ {s : Set (ι → ℝ)},
MeasurableSet s →
∀ (I : BoxIntegral.Box ι) (y : E) (μ : MeasureTheory.Measure (ι → ℝ))
[inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
BoxIntegral.HasIntegral I l (s.indicator fun x => y) μ.toBoxAdditive.toSMul ((↑↑μ (s ∩ ↑I)).toReal • y)
This theorem states that the indicator function of a measurable set is McShane integrable with respect to any locally-finite measure. Given an integration parameter 'l' that is not of B-Riemann type, a measurable set 's', a box 'I', a value 'y', and a locally-finite measure 'μ', the integral of the indicator function of 's' with respect to 'μ' over the box 'I' is equal to the measure of the intersection of 's' and 'I' multiplied by 'y'. The integrability is considered in context of the McShane definition of integral, which is a more general form of integral than the Riemann integral, and is especially suited for handling functions that are discontinuous on a set of measure zero.
More concisely: The indicator function of a measurable set is McShane integrable with respect to any locally-finite measure, and their integral over a box equals the measure of the set-box intersection multiplied by the constant.
|
MeasureTheory.SimpleFunc.hasBoxIntegral
theorem MeasureTheory.SimpleFunc.hasBoxIntegral :
∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
(f : MeasureTheory.SimpleFunc (ι → ℝ) E) (μ : MeasureTheory.Measure (ι → ℝ))
[inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams),
l.bRiemann = false →
BoxIntegral.HasIntegral I l (↑f) μ.toBoxAdditive.toSMul (MeasureTheory.SimpleFunc.integral (μ.restrict ↑I) f)
The theorem `MeasureTheory.SimpleFunc.hasBoxIntegral` states that for any simple function `f` whose domain is a finite dimensional real vector space and whose codomain is a normed commutative additive group `E`, and for any locally finite measure `μ`, the McShane integral of this function exists with respect to the measure. Specifically, it states that given any box `I` and any integration parameters `l` such that the Riemann condition for `l` is not satisfied (`l.bRiemann = false`), `f` has an integral (in the sense of Box integrals), and this integral is equal to the Bochner integral of the function `f` restricted to the box `I` and weighted by the measure `μ`.
More concisely: For any simple function `f` with finite dimensional domain and normed commutative additive group codomain, and any locally finite measure `μ`, if the Riemann condition for some integration parameters is not satisfied, then the function `f` has a Box integral equal to its Bochner integral over any box with respect to the measure `μ`.
|
MeasureTheory.SimpleFunc.box_integral_eq_integral
theorem MeasureTheory.SimpleFunc.box_integral_eq_integral :
∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
(f : MeasureTheory.SimpleFunc (ι → ℝ) E) (μ : MeasureTheory.Measure (ι → ℝ))
[inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams),
l.bRiemann = false →
BoxIntegral.integral I l (↑f) μ.toBoxAdditive.toSMul = MeasureTheory.SimpleFunc.integral (μ.restrict ↑I) f
This theorem states that for a simple function, its McShane (also known as Henstock or `⊥`) box integral is equal to its integral in the sense of `MeasureTheory.SimpleFunc.integral`. Specifically, given a function `f`, a measure `μ`, a box `I`, and integration parameters `l` where `l.bRiemann` is `false`, the integral of `f` over box `I` with respect to measure `μ`, under the parameters `l`, is equal to the integral of `f` restricted to box `I`, as defined by `MeasureTheory.SimpleFunc.integral`.
More concisely: For a simple function `f` and a measure `μ`, the McShane integral of `f` over a box `I` with respect to `μ` and integration parameters `l` where `l.bRiemann` is false, equals the `MeasureTheory.SimpleFunc.integral` of `f` restricted to `I`.
|
MeasureTheory.IntegrableOn.hasBoxIntegral
theorem MeasureTheory.IntegrableOn.hasBoxIntegral :
∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
[inst_3 : CompleteSpace E] {f : (ι → ℝ) → E} {μ : MeasureTheory.Measure (ι → ℝ)}
[inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ] {I : BoxIntegral.Box ι},
MeasureTheory.IntegrableOn f (↑I) μ →
∀ (l : BoxIntegral.IntegrationParams),
l.bRiemann = false → BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
This theorem states that, if a function `f : ℝⁿ → E` is Bochner integrable with respect to a locally finite measure `μ` on a rectangular box `I`, then it is also McShane integrable on `I` with the same integral. Here, `f` maps from an n-dimensional real space to a normed additive commutative group `E`. The rectangular box `I` is defined in the n-dimensional space, and `μ` is a measure in this space which is locally finite. The integrability of `f` is defined in terms of the Bochner integral, and the theorem asserts that under these conditions, `f` is also integrable in the McShane sense, and the two integrals coincide. The McShane integrability is defined with respect to a given set of integration parameters `l` for which the Riemann condition is not satisfied.
More concisely: If a Bochner integrable function from an n-dimensional real space to a normed additive commutative group with respect to a locally finite measure on a rectangular box satisfies the Riemann condition for a given set of parameters, then it is also McShane integrable with the same integral value.
|
BoxIntegral.HasIntegral.of_aeEq_zero
theorem BoxIntegral.HasIntegral.of_aeEq_zero :
∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
{l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {f : (ι → ℝ) → E} {μ : MeasureTheory.Measure (ι → ℝ)}
[inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
(μ.restrict ↑I).ae.EventuallyEq f 0 →
l.bRiemann = false → BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul 0
This theorem states that, given a function `f` which is almost everywhere equal to zero on a rectangular box `I`, the McShane integral of `f` over `I` is zero. This holds under the conditions that the measure `μ` is locally finite and is restricted to `I`, and that the Riemann integrability condition is false in the integration parameters `l`. The McShane integral is a generalization of the Lebesgue integral that can handle more complex functions and irregular domains.
More concisely: Given a function `f` almost everywhere equal to zero on a rectangular box `I` with respect to a locally finite measure `μ`, the McShane integral of `f` over `I` is zero when the Riemann integrability condition is not met.
|