MeasureTheory.set_integral_eq_of_subset_of_forall_diff_eq_zero
theorem MeasureTheory.set_integral_eq_of_subset_of_forall_diff_eq_zero :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
MeasurableSet t → s ⊆ t → (∀ x ∈ t \ s, f x = 0) → ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
The theorem `MeasureTheory.set_integral_eq_of_subset_of_forall_diff_eq_zero` states that if we have a function `f` from a type `X` to a normed additively commutative group `E` over the real numbers, and `s` and `t` are sets of `X` such that `s` is a subset of `t` and `f` vanishes on the difference between `t` and `s` (i.e., `f` equals zero for all elements in `t` not in `s`), then the integral of `f` over `t` with respect to a measure `μ` is equal to the integral of `f` over `s` with the same measure, provided that `t` is a measurable set.
More concisely: If `s` is a measurable subset of `X`, `t` is a measurable set containing `s` such that `f(x) = 0` for all `x in t \ s`, then `∫(f dt) = ∫(f ds)`.
|
MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict
theorem MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {ι : Type u_5} [inst_1 : Countable ι]
{μ : MeasureTheory.Measure X} [inst_2 : NormedAddCommGroup E] [inst_3 : TopologicalSpace X]
[inst_4 : BorelSpace X] [inst_5 : TopologicalSpace.MetrizableSpace X]
[inst_6 : MeasureTheory.IsLocallyFiniteMeasure μ] {f : C(X, E)} {s : ι → TopologicalSpace.Compacts X},
(Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (↑↑μ ↑(s i)).toReal) →
MeasureTheory.IntegrableOn (⇑f) (⋃ i, ↑(s i)) μ
This theorem states that if `s` is a countable family of compact sets in a topological space, `f` is a continuous function, and the sequence of the product of the norm of `f` restricted to each `s i` and the measure of `s i` is summable (i.e., its infinite sum exists), then `f` is integrable on the union of the sets `s i`. Here, a function is integrable on a set if it is almost everywhere strongly measurable on that set and the integral of its pointwise norm over the set is less than infinity.
More concisely: If `s` is a countable family of compact sets in a topological space, `f` is a continuous function, and the series $\sum\limits_{i}\lVert f\rVert_{s\_i}\mu(s\_i)$ converges, then `f` is integrable on the union of the sets `s\_i`.
|
Filter.Tendsto.integral_sub_linear_isLittleO_ae
theorem Filter.Tendsto.integral_sub_linear_isLittleO_ae :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {ι : Type u_5} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] [inst_3 : CompleteSpace E] {μ : MeasureTheory.Measure X} {l : Filter X}
[inst_4 : l.IsMeasurablyGenerated] {f : X → E} {b : E},
Filter.Tendsto f (l ⊓ μ.ae) (nhds b) →
StronglyMeasurableAtFilter f l μ →
μ.FiniteAtFilter l →
∀ {s : ι → Set X} {li : Filter ι},
Filter.Tendsto s li l.smallSets →
∀ (m : optParam (ι → ℝ) fun i => (↑↑μ (s i)).toReal),
autoParam (li.EventuallyEq (fun i => (↑↑μ (s i)).toReal) m) _auto✝ →
(fun i => ∫ (x : X) in s i, f x ∂μ - m i • b) =o[li] m
This is the Fundamental Theorem of Calculus for set integrals. Given a measure `μ` that is finite at a filter `l`, and a function `f` which is measurable and has a finite limit `b` at the infimum of `l` and `μ.ae`, the integral of `f` over a set `s i` with respect to `μ` is equal to the measure of `s i` times `b` plus a little-o term, as `s i` tends to the small sets of `l` along some filter `li`. Here, the measure of `s i` is regarded as a ℝ≥0∞ number, and its real part is used in the statement. Sometimes a formula, denoted by `m`, may exist for the real part of the measure of `s i`, which can be supplied as an optional argument. If not provided, the real part of the measure of `s i` is used as `m i` in the output.
This theorem is useful in verifying the behavior of integrals under certain conditions.
More concisely: The Fundamental Theorem of Calculus for set integrals states that for a finite measure `μ` at filter `l`, measurable function `f` with finite limit `b` at `l`'s infimum, and set `si` in `l`, the integral of `f` over `si` is approximately equal to the product of `si`'s measure and `b` as `si` approaches null sets in `l`.
|
MeasureTheory.integral_indicator
theorem MeasureTheory.integral_indicator :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
MeasurableSet s → ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ
This theorem, `MeasureTheory.integral_indicator`, states that for any given function `f` from a set `X` to a normed additive commutative group `E`, and any measurable set `s` of `X` with respect to a measure `μ`, if `s` is a measurable set, then the integral of the indicator function of `s` with respect to `f` over the entire set `X` is equal to the integral of `f` over the set `s` restricted by `μ`. In mathematical terms, this is saying that $\int_X 1_s(x) f(x) dμ = \int_s f(x) dμ$, where $1_s$ is the indicator function of `s`.
More concisely: For any measurable set `s` in the measurable space `(X, μ)` and any integrable function `f` from `X` to a normed additive commutative group `E`, $\int\_X 1\_s(x) f(x) d\mu = \int\_s f(x) d\mu$, where $1\_s$ is the indicator function of `s`.
|
ContinuousWithinAt.integral_sub_linear_isLittleO_ae
theorem ContinuousWithinAt.integral_sub_linear_isLittleO_ae :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {ι : Type u_5} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] [inst_3 : CompleteSpace E] [inst_4 : TopologicalSpace X]
[inst_5 : OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_6 : MeasureTheory.IsLocallyFiniteMeasure μ]
{x : X} {t : Set X} {f : X → E},
ContinuousWithinAt f t x →
MeasurableSet t →
StronglyMeasurableAtFilter f (nhdsWithin x t) μ →
∀ {s : ι → Set X} {li : Filter ι},
Filter.Tendsto s li (nhdsWithin x t).smallSets →
∀ (m : optParam (ι → ℝ) fun i => (↑↑μ (s i)).toReal),
autoParam (li.EventuallyEq (fun i => (↑↑μ (s i)).toReal) m) _auto✝ →
(fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m
This theorem is a version of the Fundamental Theorem of Calculus for set integrals with respect to the "neighborhood within" filter. It states that if `μ` is a locally finite measure and `f` is a function that is almost everywhere measurable and continuous at some point `a` within a measurable set `t`, then the integral of `f` over the set `s i`, subtracted by the product of `m i` and `f a`, tends to zero as `i` goes to infinity, provided that the set `s i` tends to the small sets of the neighborhood of `a` within `t` along the filter `li`. Here, `m` is an optional function often representing a good formula for the real part of the measure of the set `s i`, and by default is equal to the real part of the measure of the set `s i`. The theorem requires that `m` is eventually equal to the real part of the measure of the set `s i` along the filter `li`, which is ensured by an automatic parameter `autoParam`.
More concisely: If `μ` is a locally finite measure, `f` is almost everywhere measurable and continuous at some point `a` in the measurable set `t`, and `mi` tends to the real part of the measure of `si` along the filter `li` as `i` goes to infinity, then `∫(si, f) - m(si) * f(a)` tends to 0.
|
MeasureTheory.set_integral_mono_ae_restrict
theorem MeasureTheory.set_integral_mono_ae_restrict :
∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {f g : X → ℝ} {s : Set X},
MeasureTheory.IntegrableOn f s μ →
MeasureTheory.IntegrableOn g s μ →
(μ.restrict s).ae.EventuallyLE f g → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
This theorem, `MeasureTheory.set_integral_mono_ae_restrict`, states that for any given measurable space `X`, a measure `μ` on this space, two real-valued functions `f` and `g` on `X`, and a set `s` of `X`, if both `f` and `g` are integrable on the set `s` with respect to the measure `μ` and if the function `f` is almost everywhere less than or equal to `g` with respect to the measure `μ` restricted on set `s`, then the integral of `f` over the set `s` with respect to the measure `μ` is less than or equal to the integral of `g` over the set `s` with respect to the measure `μ`. In simple terms, if `f` is generally smaller or equal to `g` everywhere on `s`, then the integral of `f` over `s` is no larger than the integral of `g` over `s`.
More concisely: If `f` and `g` are integrable functions on a measurable set `s` with `f(x) ≤ g(x)` almost everywhere in `s`, then `∫(f dμ) ≤ ∫(g dμ)` for the measures `μ` on the measurable space `X`.
|
MeasureTheory.integral_add_compl
theorem MeasureTheory.integral_add_compl :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
MeasurableSet s →
MeasureTheory.Integrable f μ → ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ
The theorem `MeasureTheory.integral_add_compl` states that for any measurable space `X`, any normed additive commutative group `E`, any function `f` from `X` to `E`, any set `s` in `X`, and any measure `μ` on `X`: if `s` is a measurable set and `f` is integrable with respect to `μ`, then the integral of `f` over `s` with respect to `μ` plus the integral of `f` over the complement of `s` with respect to `μ` equals the integral of `f` over `X` with respect to `μ`. In mathematical notation, this can be written as:
\[\int_{s} f \, d\mu + \int_{s^c} f \, d\mu = \int_{X} f \, d\mu \]
This theorem emphasizes the idea that the integral over the whole space can be decomposed into the integral over a subset and its complement.
More concisely: For any measurable space X, normed additive commutative group E, measurable set s, integrable function f from X to E, and measure μ on X, we have ∫s f dμ + ∫s^c f dμ = ∫X f dμ.
|
MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero
theorem MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
MeasureTheory.NullMeasurableSet t μ →
s ⊆ t → (∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0) → ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
The theorem `MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero` states that for a given function `f` from a measurable space `X` to a normed add commutative group `E`, along with two sets `s` and `t` in `X` and a measure `μ` on `X`, if `t` is a null-measurable set, `s` is a subset of `t`, and `f` is almost everywhere zero on the set difference `t \ s`, then the integral of `f` over `t` with respect to `μ` is equal to the integral of `f` over `s` with respect to `μ`. In other words, the measure of the difference between the sets `t` and `s` where `f` does not vanish is null, hence the integrals of `f` over `t` and `s` coincide.
More concisely: If `s` is a subset of null-measurable set `t` in a measurable space `X` and function `f` from `X` to a normed add commutative group `E` is almost everywhere zero on `t \ s`, then the integral of `f` over `t` equals the integral of `f` over `s`.
|
continuousOn_integral_of_compact_support
theorem continuousOn_integral_of_compact_support :
∀ {X : Type u_1} {Y : Type u_2} {E : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : MeasurableSpace Y] [inst_3 : OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y}
[inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℝ E] {f : X → Y → E} {s : Set X} {k : Set Y}
[inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ],
IsCompact k →
ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ) →
(∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0) → ContinuousOn (fun x => ∫ (y : Y), f x y ∂μ) s
This theorem states that for a parameterized integral of the form `x ↦ ∫ y, f x y`, where `f` is a function that is continuous and uniformly vanishes outside a compact set `k`, the integral function depends continuously on `x`. This is under the conditions that `f` is continuous on the product of the set `s` and the universal set, and for any `p` in `s` and any `y` not in `k`, `f p y` is equal to zero. The spaces `X` and `Y` are topological, `Y` is measurable, `μ` is a measure on `Y` finite on compact sets, and `E` is a normed additive commutative group which is also a real normed space.
More concisely: If `f` is a continuous, compactly supported function on a product of topological spaces `X × Y`, where `Y` is measurable with a finite measure `μ` on compact sets, and `f(x, y) = 0` for all `y` not in a compact set `k` and all `x` in `X`, then the function `x ↦ ∫ y, f x y` is continuous on `X`.
|
MeasureTheory.set_integral_mono_set
theorem MeasureTheory.set_integral_mono_set :
∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {f : X → ℝ} {s t : Set X},
MeasureTheory.IntegrableOn f t μ →
(μ.restrict t).ae.EventuallyLE 0 f → μ.ae.EventuallyLE s t → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in t, f x ∂μ
This theorem states that for any measurable space `X`, any measure `μ` on `X`, and any real-valued function `f` defined on `X`, if `f` is integrable on a set `t` with respect to `μ`, and `f` is non-negative almost everywhere in the restriction of `μ` to `t`, and if a set `s` is almost everywhere a subset of `t` with respect to `μ`, then the integral of `f` over `s` with respect to `μ` is less than or equal to the integral of `f` over `t` with respect to `μ`. In other words, if a function is non-negative and integrable on a set, the integral over any subset of that set is less than or equal to the integral over the set.
More concisely: If `f` is a non-negative integrable function on measurable set `t` with respect to measure `μ`, and `s` is almost everywhere a subset of `t`, then the integral of `f` over `s` is less than or equal to the integral of `f` over `t`.
|
MeasureTheory.set_integral_eq_integral_of_forall_compl_eq_zero
theorem MeasureTheory.set_integral_eq_integral_of_forall_compl_eq_zero :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
(∀ x ∉ s, f x = 0) → ∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
This theorem, referred to as an alias of `MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero`, establishes an equivalence in the field of Measure Theory. Specifically, it states that for any type `X` endowed with a measurable structure, an additively commutative normed group `E`, and a real normed space `E`, if a function `f` from `X` to `E` vanishes on the complement of a set `s` of type `X` (i.e., `f(x) = 0` for all `x` not in `s`), then the integral of `f` over set `s` with respect to a measure `μ` is equal to the integral of `f` over the entire space of `X` with respect to the same measure `μ`.
More concisely: If a measurable function from a measurable space to a real normed space vanishes outside a set of measure zero, then its integral over that set is equal to its integral over the entire measurable space.
|
MeasurableEmbedding.set_integral_map
theorem MeasurableEmbedding.set_integral_map :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure X} {Y : Type u_5} {x : MeasurableSpace Y} {f : X → Y},
MeasurableEmbedding f →
∀ (g : Y → E) (s : Set Y),
∫ (y : Y) in s, g y ∂MeasureTheory.Measure.map f μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ
This theorem states that for any two types `X` and `Y`, if `X` is a measurable space and `E` is a normed group over the real numbers, then given a measure `μ` on `X`, any measurable embedding function `f` from `X` to `Y`, and any function `g` from `Y` to `E`, the integral of `g` over a set `s` in `Y` with respect to the measure induced by `f` is equal to the integral of the composed function `g ∘ f` over the preimage of `s` under `f` with respect to the measure `μ`. This theorem thus links the integration of a function over a set in the codomain of a measurable embedding to the integration over the preimage of the set in the domain.
More concisely: For any measurable spaces X and Y, normed group E over the real numbers, measure μ on X, measurable embedding f : X → Y, and function g : Y → E, the integral of g over a set s in Y with respect to the measure induced by f is equal to the integral of g ∘ f over the preimage of s under f with respect to μ.
|
MeasureTheory.set_integral_congr_ae
theorem MeasureTheory.set_integral_congr_ae :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f g : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
MeasurableSet s → (∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x) → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
The theorem `MeasureTheory.set_integral_congr_ae` states that for any measure space `X` and any normed additive commutative group `E` that is also a normed space over the reals, given two functions `f` and `g` from `X` to `E`, a set `s` in `X` that is measurable, and a measure `μ` on `X`, if almost every element `x` in `s` with respect to measure `μ` satisfies `f x = g x`, then the integral of `f` over the set `s` with respect to measure `μ` equals to the integral of `g` over the same set with respect to the same measure. In other words, if `f` and `g` are equal almost everywhere on a measurable set `s`, then their integrals over `s` are the same.
More concisely: If two real-valued functions on a measurable set of a measure space are equal almost everywhere with respect to a given measure, then they have equal integrals over that set with respect to that measure.
|
MeasureTheory.set_integral_nonneg_of_ae_restrict
theorem MeasureTheory.set_integral_nonneg_of_ae_restrict :
∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
(μ.restrict s).ae.EventuallyLE 0 f → 0 ≤ ∫ (x : X) in s, f x ∂μ
The theorem `MeasureTheory.set_integral_nonneg_of_ae_restrict` states that for any measurable space `X`, given a measure `μ` on `X`, a real-valued function `f` on `X`, and a set `s` of `X`, if the function `f` is nonnegative almost everywhere with respect to the measure `μ` restricted to the set `s`, then the Lebesgue integral of `f` over the set `s` with respect to the measure `μ` is also nonnegative. In other words, if a function is almost everywhere nonnegative when limited to a certain set, the integral over that set will be nonnegative as well.
More concisely: If a measurable function is almost everywhere nonnegative on a set with respect to a measure, then the Lebesgue integral of the function over that set with respect to the measure is nonnegative.
|
MeasureTheory.set_integral_eq_integral_of_ae_compl_eq_zero
theorem MeasureTheory.set_integral_eq_integral_of_ae_compl_eq_zero :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
(∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0) → ∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
This theorem, `MeasureTheory.set_integral_eq_integral_of_ae_compl_eq_zero`, states that for any measurable space `X` and normed add commutative group `E` that also is a normed space over the real numbers, given a function `f` from `X` to `E`, a set `s` of elements from `X`, and a measure `μ` on `X`, if the function `f` equals zero almost everywhere on the complement of `s` (denoted by `sᶜ`) with respect to the measure `μ`, then the integral of `f` over the set `s` is equal to the integral of `f` over the whole space `X`. In other words, if `f` is zero almost everywhere outside `s`, the integral of `f` on `s` coincides with its integral on the whole space.
More concisely: If a measurable function `f` from a measurable space `(X, μ)` to a normed add commutative group `E` over the real numbers has zero integral over the complement of a set `s` with respect to `μ`, then the integral of `f` over `s` equals the integral of `f` over the whole space `X`.
|
MeasureTheory.MeasurePreserving.set_integral_image_emb
theorem MeasureTheory.MeasurePreserving.set_integral_image_emb :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {μ : MeasureTheory.Measure X} {Y : Type u_5} {x : MeasurableSpace Y} {f : X → Y}
{ν : MeasureTheory.Measure Y},
MeasureTheory.MeasurePreserving f μ ν →
MeasurableEmbedding f → ∀ (g : Y → E) (s : Set X), ∫ (y : Y) in f '' s, g y ∂ν = ∫ (x : X) in s, g (f x) ∂μ
This theorem, `MeasureTheory.MeasurePreserving.set_integral_image_emb`, establishes a result in measure theory and integration theory. It states that given two types X and Y with measurable spaces and a function `f` from X to Y, if `f` preserves the measure μ on X under the measure ν on Y and `f` is a measurable embedding, then for any function `g` from Y to a normed additively commutative group E and any set `s` of X, the integral of `g` over the image of `s` under `f` with respect to the measure ν equals the integral of `g ∘ f` over `s` with respect to the measure μ. That is, the measures and the integrals are preserved under the function `f`.
More concisely: Given measurable spaces (X, μ) and (Y, ν), a measurable embedding and measure-preserving function f : X → Y, and a function g : Y → an additively commutative group E, the integral of g over the image of a set s ⊆ X under f with respect to ν equals the integral of g ∘ f over s with respect to μ.
|
MeasureTheory.norm_Lp_toLp_restrict_le
theorem MeasureTheory.norm_Lp_toLp_restrict_le :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure X} (s : Set X) (f : ↥(MeasureTheory.Lp E p μ)),
‖MeasureTheory.Memℒp.toLp ↑↑f ⋯‖ ≤ ‖f‖
The theorem `MeasureTheory.norm_Lp_toLp_restrict_le` states that for any measurable space `X`, normed additive commutative group `E`, extended nonnegative real number `p`, measure `μ` on `X`, set `s` of `X`, and function `f` in the `Lp` space, the norm of the function `f` when restricted to the set `s` and transformed to `Lp` space (through the process `(Lp.memℒp f).restrict s).toLp f`) is less than or equal to the norm of `f`. This essentially asserts that the process of restricting a function to a subset and converting the function to `Lp` space does not increase the `Lp` norm of the function, thereby showing that the map is non-expansive.
More concisely: For any measurable space X, normed additive commutative group E, extended nonnegative real number p, measure μ on X, set s of X, and function f in the Lp space, the norm of (Lp.memℒp f).restrict s).toLp f is less than or equal to the norm of f.
|
MeasureTheory.set_integral_pos_iff_support_of_nonneg_ae
theorem MeasureTheory.set_integral_pos_iff_support_of_nonneg_ae :
∀ {X : Type u_1} [inst : MeasurableSpace X] {s : Set X} {μ : MeasureTheory.Measure X} {f : X → ℝ},
(μ.restrict s).ae.EventuallyLE 0 f →
MeasureTheory.IntegrableOn f s μ → (0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < ↑↑μ (Function.support f ∩ s))
This theorem states that for a measurable space X, a given set `s` in X, a measure `μ` on X, and a real-valued function `f` defined on X, if `f` is non-negative almost everywhere on the restriction of `μ` to `s`, and `f` is integrable on `s` with respect to `μ`, then the integral of `f` over `s` is greater than zero if and only if the measure of the intersection of the support of `f` and `s` is greater than zero.
The support of `f` is defined as the set of points `x` such that `f(x) ≠ 0`. Intuitively, the theorem links the positivity of the integral of a function over a set to the measure of the region where the function is non-zero.
More concisely: For a measurable space X, a measurable set s, a measure μ, a non-negative integrable function f on X, the integral of f over s is positive if and only if the measure of the support of f intersecting s is positive.
|
MeasureTheory.set_integral_const
theorem MeasureTheory.set_integral_const :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {s : Set X} {μ : MeasureTheory.Measure X} [inst_3 : CompleteSpace E] (c : E),
∫ (x : X) in s, c ∂μ = (↑↑μ s).toReal • c
The theorem `MeasureTheory.set_integral_const` states that for any type `X` with a measurable space structure, any normed additively commutative group `E` which is also a real normed space, any set `s` of type `X`, any measure `μ` defined on `X`, and any element `c` of `E`, the integral of the constant function `c` over the set `s` with respect to the measure `μ` is equal to the measure of `s` (converted to real) scaled by `c`. This means, when you integrate a constant over a set, the result is the size (measure) of the set times the constant.
More concisely: For any measurable space (X, Σ, μ), normed additively commutative group E over the reals, set s ∈ Σ, and constant c ∈ E, ∫s(x) dc = μ(s) * c.
|
MeasureTheory.Lp_toLp_restrict_smul
theorem MeasureTheory.Lp_toLp_restrict_smul :
∀ {X : Type u_1} {F : Type u_4} [inst : MeasurableSpace X] {𝕜 : Type u_5} [inst_1 : NormedField 𝕜]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {p : ENNReal} {μ : MeasureTheory.Measure X} (c : 𝕜)
(f : ↥(MeasureTheory.Lp F p μ)) (s : Set X),
MeasureTheory.Memℒp.toLp ↑↑(c • f) ⋯ = c • MeasureTheory.Memℒp.toLp ↑↑f ⋯
The theorem `MeasureTheory.Lp_toLp_restrict_smul` states that for a function `f` belonging to the Lp space (denoted as `Lp E p μ`), we can define an element of `Lp E p (μ.restrict s)` using `(Lp.memℒp f).restrict s).toLp f`. This definition commutes with scalar multiplication. In more specific terms, for any measurable space `X`, normed field `𝕜`, normed add commutative group `F`, normed space `𝕜 F`, p as an extended nonnegative real number, a measure `μ` on `X`, a scalar `c` of type `𝕜`, a function `f` in `Lp F p μ`, and a set `s` of `X`, the Lp norm of the scaled function `c • f` restricted to `s` is the same as `c` times the Lp norm of the function `f` restricted to `s`.
More concisely: For any measurable space X, normed field 𝕜, normed add commutative group F, normed space 𝕜F over a measure space (X, μ), extended nonnegative real number p, and functions f in Lp(F, μp) and c in 𝕜, the Lp norm of c • f restricted to a set s is equal to |c| * (the Lp norm of f restricted to s).
|
MeasureTheory.Lp_toLp_restrict_add
theorem MeasureTheory.Lp_toLp_restrict_add :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure X} (f g : ↥(MeasureTheory.Lp E p μ)) (s : Set X),
MeasureTheory.Memℒp.toLp ↑↑(f + g) ⋯ = MeasureTheory.Memℒp.toLp ↑↑f ⋯ + MeasureTheory.Memℒp.toLp ↑↑g ⋯
The theorem `MeasureTheory.Lp_toLp_restrict_add` states that for any space `X` with a measurable structure and for any normed commutative group `E`, for any extended nonnegative real number `p` and for any measure `μ` on the space `X`, given two members `f` and `g` of the `Lp` space, and for any set `s` in `X`, the `Lp` element corresponding to the sum of `f` and `g` restricted to the set `s` is equal to the sum of the `Lp` elements corresponding to `f` and `g` each restricted to the set `s` separately. In other words, it asserts that the process of restricting functions to a set and then taking the `Lp` class commutes with addition.
More concisely: For any measurable space (X, Σ, μ), normed commutative group E, extended nonnegative real number p, and Lp(X, E, μ)-functions f and g, the restriction of their sum to any set S in X is equal to the sum of their restrictions to S in the Lp sense.
|
MeasureTheory.integral_univ
theorem MeasureTheory.integral_univ :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f : X → E} {μ : MeasureTheory.Measure X},
∫ (x : X) in Set.univ, f x ∂μ = ∫ (x : X), f x ∂μ
This theorem, `MeasureTheory.integral_univ`, states that for any type `X` endowed with a measurable space structure, any type `E` endowed with a normed additive commutative group structure and a normed space structure over the field of real numbers, any function `f` from `X` to `E`, and any measure `μ` on `X`, the integral of `f` over the entire set of `X` (i.e., `Set.univ`) with respect to the measure `μ` is equal to the integral of `f` over `X` with respect to `μ`. In simple terms, it asserts that the integral of a function over the whole space is the same, regardless of whether we explicitly specify that the domain of integration is the whole space or leave the domain implicit.
More concisely: For any measurable space `(X, Σ, μ)`, normed additive commutative group `(E, +)` with a real norm `|.|`, and measurable function `f : X → E`, the integral of `f` over the whole space `X` is equal to the integral over `X` with respect to `μ`. In symbols, `∫(f : X → E) dμ = ∫(f : X → E) d(μ \(|\) Set.univ)`.
|
MeasureTheory.integrable_of_summable_norm_restrict
theorem MeasureTheory.integrable_of_summable_norm_restrict :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {ι : Type u_5} [inst_1 : Countable ι]
{μ : MeasureTheory.Measure X} [inst_2 : NormedAddCommGroup E] [inst_3 : TopologicalSpace X]
[inst_4 : BorelSpace X] [inst_5 : TopologicalSpace.MetrizableSpace X]
[inst_6 : MeasureTheory.IsLocallyFiniteMeasure μ] {f : C(X, E)} {s : ι → TopologicalSpace.Compacts X},
(Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (↑↑μ ↑(s i)).toReal) →
⋃ i, ↑(s i) = Set.univ → MeasureTheory.Integrable (⇑f) μ
The theorem states that, given a countable family of compact sets `s` that covers the entire space `X`, if `f` is a continuous function and the sequence formed by multiplying the norm of the function restricted to each compact set `s i` by the measure of `s i` is summable, then the function `f` is integrable with respect to the measure `μ`. In other words, the function `f` is measurable and the integral over all `X` of the norm of `f` with respect to `μ` is finite. This condition of integrability is a key concept in measure theory and analysis, as it allows us to perform many operations and transformations on the function `f`.
More concisely: Given a countable family of compact sets covering a space X, if a continuous function f has its norm restricted to each set multiplied by the set's measure summable, then f is integrable with respect to the measure μ.
|
ContinuousLinearMap.integral_comp_comm
theorem ContinuousLinearMap.integral_comp_comm :
∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X}
{𝕜 : Type u_5} [inst_1 : RCLike 𝕜] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
[inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace ℝ F] [inst_7 : CompleteSpace F]
[inst_8 : NormedSpace ℝ E] [inst_9 : CompleteSpace E] (L : E →L[𝕜] F) {φ : X → E},
MeasureTheory.Integrable φ μ → ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
The theorem `ContinuousLinearMap.integral_comp_comm` states that for any measurable space `X`, normed addcomm groups `E` and `F`, a measure `μ` on `X`, a RCLike `𝕜`, normed spaces over `𝕜` for `E` and `F`, normed spaces over ℝ for `E` and `F` (which are complete spaces), and a continuous linear map `L` from `E` to `F`, if a function `φ` from `X` to `E` is integrable with respect to `μ`, then the integral over `X` of the function obtained by applying `L` to `φ(x)` is equal to the result of applying `L` to the integral over `X` of `φ(x)`.
In mathematical notation, this theorem states that if `φ : X → E` is integrable, then `∫ (L ∘ φ) dμ = L (∫ φ dμ)`.
More concisely: The theorem asserts that for a measurable space `(X, μ)`, normed addcomm groups `E` and `F` over a RCLike `𝕜`, a continuous linear map `L : E → F`, and an integrable function `φ : X → E`, the integral of their composition `(L ∘ φ)` equals `L` applied to the integral of `φ`, i.e., `∫ (L ∘ φ) dμ = L (∫ φ dμ)`.
|
ContinuousOn.integral_sub_linear_isLittleO_ae
theorem ContinuousOn.integral_sub_linear_isLittleO_ae :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {ι : Type u_5} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] [inst_3 : CompleteSpace E] [inst_4 : TopologicalSpace X]
[inst_5 : OpensMeasurableSpace X] [inst_6 : SecondCountableTopologyEither X E] {μ : MeasureTheory.Measure X}
[inst_7 : MeasureTheory.IsLocallyFiniteMeasure μ] {x : X} {t : Set X} {f : X → E},
ContinuousOn f t →
x ∈ t →
MeasurableSet t →
∀ {s : ι → Set X} {li : Filter ι},
Filter.Tendsto s li (nhdsWithin x t).smallSets →
∀ (m : optParam (ι → ℝ) fun i => (↑↑μ (s i)).toReal),
autoParam (li.EventuallyEq (fun i => (↑↑μ (s i)).toReal) m) _auto✝ →
(fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m
This theorem, often referred to as the Fundamental Theorem of Calculus for set integrals in the `nhdsWithin` context, states that given a locally finite measure `μ`, a function `f` that is continuous on a measurable set `t`, and `a` which is an element of `t`, then the integral of `f` over a sequence of sets `s i` equals `μ (s i) • f a` plus a term that is little o of `μ (s i)` when `s i` tends to the small sets in the neighborhood of `a` within `t`.
In the statement of the theorem, `μ (s i)` is a non-negative real number, so we use its real part `(μ (s i)).toReal` in the actual statement. The theorem can receive an optional argument `m` which is a formula for `(μ (s i)).toReal`, and a proof that the real part of `μ (s i)` is eventually equal to `m` along a filter `li`. If these arguments are not provided, the theorem uses `m i = (μ (s i)).toReal` in the output.
In summary, the theorem relates the integral of a function over a sequence of sets to the measure of these sets times the function's value at a point, with an error that tends to zero.
More concisely: Given a locally finite measure `μ`, a continuous function `f` on a measurable set `t`, and an element `a` in `t`, the integral of `f` over a sequence of sets `s i` approaching `t` around `a` is equal to `μ (s i) * f a + o(μ (s i))`.
|
MeasureTheory.set_integral_congr_set_ae
theorem MeasureTheory.set_integral_congr_set_ae :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
μ.ae.EventuallyEq s t → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ
This theorem, `MeasureTheory.set_integral_congr_set_ae`, states that for any types `X` and `E`, given a measurable space on `X`, a normed additive commutative group on `E`, and a normed space over the reals for `E`; for any function `f` from `X` to `E`, and any two sets `s` and `t` of `X`, and a measure `μ` on `X`; if the sets `s` and `t` are equal almost everywhere with respect to measure `μ` (meaning, the set of points where `s` and `t` differ has measure zero), then the integral of `f` over the set `s` with respect to measure `μ` is equal to the integral of `f` over the set `t` with respect to measure `μ`. In other words, changing the values of a function on a set of measure zero does not change its integral.
More concisely: If two sets have measure zero difference in a measurable space, then the integral of a measurable function over one set equals the integral over the other.
|
MeasureTheory.integral_union
theorem MeasureTheory.integral_union :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
Disjoint s t →
MeasurableSet t →
MeasureTheory.IntegrableOn f s μ →
MeasureTheory.IntegrableOn f t μ →
∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ
The theorem `MeasureTheory.integral_union` states that for any two disjoint measurable sets `s` and `t` in a given measurable space `X` and any function `f` from `X` to a normed additive commutative group `E` (which is also a normed space over the real numbers), if `f` is integrable on both `s` and `t` with respect to a given measure `μ`, then the integral of `f` over the union of `s` and `t` is equal to the sum of the integral of `f` over `s` and the integral of `f` over `t`. In mathematical terms, this can be written as:
∀ s, t ⊂ X, f : X → E, μ : Measure,
If s ∩ t = ∅, f is μ-integrable on s and t, then ∫ₛ ∪ t f dμ = ∫ₛ f dμ + ∫ₜ f dμ.
More concisely: If two disjoint measurable sets `s` and `t` in a measurable space `X` and a function `f` from `X` to a normed additive commutative group `E`, integrable over `s` and `t` with respect to a measure `μ`, then the integral of `f` over their union equals the sum of the integrals over `s` and `t`.
|
integral_ofReal
theorem integral_ofReal :
∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_5} [inst_1 : RCLike 𝕜]
{f : X → ℝ}, ∫ (x : X), ↑(f x) ∂μ = ↑(∫ (x : X), f x ∂μ)
The theorem `integral_ofReal` states that for any measurable space `X` with measure `μ`, and any real-valued function `f` on `X`, the integral of the complex extension of `f` (denoted by `↑(f x)`) with respect to `μ` is the same as the complex extension of the integral of `f` with respect to `μ`. In other words, taking the integral and extending to complex numbers commute with each other.
More concisely: For any measurable space (X, μ) and measurable real-valued function f on X, the complex integrals ∫(↑(fx) dμ) = ↑(∫(fx) dμ).
|
MeasureTheory.set_integral_congr
theorem MeasureTheory.set_integral_congr :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] {f g : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
MeasurableSet s → Set.EqOn f g s → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
The theorem `MeasureTheory.set_integral_congr` states that for any measurable space `X` and any normed additively commutative group `E` that is also a normed space over the real numbers, given two functions `f` and `g` from `X` to `E`, a set `s` of `X`, and a measure `μ` on `X`, if the set `s` is measurable and the functions `f` and `g` are equal on the set `s`, then the integral of the function `f` with respect to the measure `μ` over the set `s` is equal to the integral of the function `g` with respect to the measure `μ` over the set `s`. In other words, it asserts the equality of integrals of two functions over a measurable set, when the functions coincide on that set.
More concisely: If `X` is a measurable space, `E` is a normed additively commutative group and normed space over the real numbers, `f` and `g` are measurable functions from `X` to `E`, `s` is a measurable subset of `X`, and `f` equals `g` on `s`, then the integrals of `f` and `g` with respect to a measure `μ` on `X` over `s` are equal.
|
MeasureTheory.set_integral_mono_ae
theorem MeasureTheory.set_integral_mono_ae :
∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {f g : X → ℝ} {s : Set X},
MeasureTheory.IntegrableOn f s μ →
MeasureTheory.IntegrableOn g s μ → μ.ae.EventuallyLE f g → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
This theorem states that for any set `s` of a type `X` that is a measurable space, given a measure `μ` on `X` and two real-valued functions `f` and `g` defined on `X`, if both `f` and `g` are integrable over the set `s` with respect to the measure `μ`, and if the function `f` is less than or equal to the function `g` almost everywhere with respect to the measure `μ`, then the integral of `f` over the set `s` with respect to the measure `μ` is less than or equal to the integral of `g` over the same set with respect to the same measure. This is a statement about the monotonicity of the integral in terms of the functions being integrated, under certain conditions.
More concisely: If `μ` is a measure on the measurable space `(X, Σ)`, `s ∈ Σ` is a set, `f` and `g` are integrable real-valued functions on `s` with `f ≤ g` almost everywhere on `s`, then `∫(f ds) ≤ ∫(g ds)`.
|
ContinuousAt.integral_sub_linear_isLittleO_ae
theorem ContinuousAt.integral_sub_linear_isLittleO_ae :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {ι : Type u_5} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ℝ E] [inst_3 : CompleteSpace E] [inst_4 : TopologicalSpace X]
[inst_5 : OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_6 : MeasureTheory.IsLocallyFiniteMeasure μ]
{x : X} {f : X → E},
ContinuousAt f x →
StronglyMeasurableAtFilter f (nhds x) μ →
∀ {s : ι → Set X} {li : Filter ι},
Filter.Tendsto s li (nhds x).smallSets →
∀ (m : optParam (ι → ℝ) fun i => (↑↑μ (s i)).toReal),
autoParam (li.EventuallyEq (fun i => (↑↑μ (s i)).toReal) m) _auto✝ →
(fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m
This theorem, known as the Fundamental Theorem of Calculus for set integrals in the neighborhood version, posits that if we have a locally finite measure `μ` and a function `f` which is almost everywhere measurable and continuous at a point `a`, then the integral of `f` over a set `s` with respect to `μ` is equal to `μ (s i) • f a + o(μ (s i))` as `s` tends to `(𝓝 a).smallSets` along a filter `li`. As `μ (s i)` is a number belonging to `ℝ≥0∞`, we utilize `(μ (s i)).toReal` in the actual theorem statement.
The theorem is also flexible to optionally accept an argument `m`, which is a formula for `(μ (s i)).toReal` and a proof that `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. In absence of these arguments, `m i = (μ (s i)).toReal` is used in the output.
More concisely: If `μ` is a locally finite measure, `f` is almost everywhere measurable and continuous at `a`, and `s` is a set in the neighborhood of `a`, then the integral of `f` with respect to `μ` over `s` is equal to `μ(s)^(1/1!) * f(a) + o(μ(s))` as `μ(s)` tends to zero.
|