MeasureTheory.tendsto_setToFun_of_L1
theorem MeasureTheory.tendsto_setToFun_of_L1 :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{ι : Type u_7} (f : α → E),
MeasureTheory.Integrable f μ →
∀ {fs : ι → α → E} {l : Filter ι},
(∀ᶠ (i : ι) in l, MeasureTheory.Integrable (fs i) μ) →
Filter.Tendsto (fun i => ∫⁻ (x : α), ↑‖fs i x - f x‖₊ ∂μ) l (nhds 0) →
Filter.Tendsto (fun i => MeasureTheory.setToFun μ T hT (fs i)) l
(nhds (MeasureTheory.setToFun μ T hT f))
The theorem `MeasureTheory.tendsto_setToFun_of_L1` states that for a set function `T` that is finitely additive and dominated by a measure `μ` multiplied by a real constant `C`, if a function `f` is integrable with respect to `μ`, and if for some sequence (indexed by type `ι`) of functions `fs`, each `fs i` is almost everywhere integrable with respect to `μ` and the sequence of their L1 norms (i.e., the integral of the absolute differences between `fs i` and `f` over the domain `α`) tends to zero, then the sequence of the set-to-function transformations `setToFun μ T hT (fs i)` converges in the sense of filters to `setToFun μ T hT f`.
Informally, this is expressing a sort of continuity property for the `setToFun` transformation under L1 convergence of a sequence of functions to a limit function.
More concisely: If a finitely additive set function T is dominated by a measure μ multiplied by a constant C, and a function f is μ-integrable with respect to T, then for any sequence (fs i) of almost everywhere μ-integrable functions that converge to f in L1 norm, the set-to-function transformations (setToFun μ T hT (fs i)) converge to setToFun μ T hT f.
|
MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure
theorem MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α}
{μ μ' : MeasureTheory.Measure α} (T : Set α → E →L[ℝ] F),
(∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0) →
MeasureTheory.FinMeasAdditive μ T →
μ.AbsolutelyContinuous μ' →
∀ (f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)) (f' : ↥(MeasureTheory.Lp.simpleFunc E 1 μ')),
μ.ae.EventuallyEq ↑↑↑f ↑↑↑f' →
MeasureTheory.L1.SimpleFunc.setToL1S T f = MeasureTheory.L1.SimpleFunc.setToL1S T f'
The theorem `MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure` states that, for any measurable space `α` and normed additively commutative groups `E` and `F` over the real numbers, if we have two measures `μ` and `μ'` over `α`, a function `T` from the set `α` to the continuous linear maps from `E` to `F`, and if for any measurable set `s`, `T` applied to `s` is zero whenever measure `μ` of `s` is zero, and `T` is finitely additively measureable on `μ`, and `μ` is absolutely continuous with respect to `μ'`, then for any function `f` in the subspace of Lp (with p=1) of equivalence classes of integrable simple functions under measure `μ`, and `f'` under measure `μ'`, that are almost everywhere equal according to `μ`, the extension of `T` to `(α →₁ₛ[μ] E) → F` applied to `f` is equal to it applied to `f'`. In other words, swapping the measure `μ` with `μ'` in `setToL1S` does not change its outcome when conditions on `T` and the relation between `μ` and `μ'` are met, even though `f` and `f'` might belong to different types.
More concisely: If measures `μ` and `μ'` are absolutely continuous, `T` is a finitely additive, measure zero preserving, continuous linear map from measurable sets to the space of continuous linear maps from `E` to `F`, and `f` and `f'` are almost everywhere equal integrable simple functions under measures `μ` and `μ'` respectively, then `T(f) = T(f')`.
|
MeasureTheory.tendsto_setToFun_of_dominated_convergence
theorem MeasureTheory.tendsto_setToFun_of_dominated_convergence :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{fs : ℕ → α → E} {f : α → E} (bound : α → ℝ),
(∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fs n) μ) →
MeasureTheory.Integrable bound μ →
(∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) →
(∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => fs n a) Filter.atTop (nhds (f a))) →
Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT (fs n)) Filter.atTop
(nhds (MeasureTheory.setToFun μ T hT f))
The theorem `MeasureTheory.tendsto_setToFun_of_dominated_convergence` is a version of the Lebesgue Dominated Convergence Theorem in the context of sequence of functions. It states that if we have a sequence of functions (`fs`) that are almost everywhere strongly measurable with respect to a measure `μ` and a bound function (`bound`) that is integrable with respect to `μ`, such that the norm of each function in the sequence at each point is almost everywhere less than or equal to the value of the `bound` function at that point. Further, if for almost all points, the function values of the sequence converge to the value of a function `f` as the index goes to infinity, then the image of the sequence under `setToFun` (a function associated with the measure `μ`, a function `T` and a real number `C`) also converges to the image of `f` under the `setToFun`.
More concisely: If `(fs: ℝ^(μ) → ℝ)` is a sequence of almost everywhere strongly measurable functions, `bound : ℝ^(μ) → ℝ` is integrable, and for almost all `x`, `|fs x| ≤ bound x`, with `fs x` converging to `f(x)` almost everywhere, then `setToFun (μ, T, C) (fs)` converges to `setToFun (μ, T, C) (f)` in `ℝ^(μ)`.
|
MeasureTheory.SimpleFunc.setToSimpleFunc_congr
theorem MeasureTheory.SimpleFunc.setToSimpleFunc_congr :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F),
(∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0) →
MeasureTheory.FinMeasAdditive μ T →
∀ {f g : MeasureTheory.SimpleFunc α E},
MeasureTheory.Integrable (↑f) μ →
μ.ae.EventuallyEq ↑f ↑g →
MeasureTheory.SimpleFunc.setToSimpleFunc T f = MeasureTheory.SimpleFunc.setToSimpleFunc T g
The theorem `MeasureTheory.SimpleFunc.setToSimpleFunc_congr` states that given a measurable space `α`, a normed additively commutative group `E`, a normed additively commutative group `F`, a measure `μ` on `α`, and a function `T` from subsets of `α` to continuous linear real-valued maps from `E` to `F`, if `T` is zero on all measurable sets of measure zero and `T` is finitely additive on measurable sets with finite measure, then for any two simple (step) functions `f` and `g` from `α` to `E` that are integrable with respect to `μ`, if `f` and `g` are almost everywhere equal with respect to the measure `μ`, then the extension of `T` to simple functions applied to `f` equals the extension of `T` to simple functions applied to `g`.
More concisely: If `T` is a finitely additive, measure-zero preserving continuous linear map from subsets of a measure space to the space of continuous linear maps between two normed additive commutative groups, and `f` and `g` are integrable simple functions that are almost everywhere equal, then `T(f) = T(g)`.
|
MeasureTheory.L1.SimpleFunc.setToL1S_add
theorem MeasureTheory.L1.SimpleFunc.setToL1S_add :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
(T : Set α → E →L[ℝ] F),
(∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0) →
MeasureTheory.FinMeasAdditive μ T →
∀ (f g : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)),
MeasureTheory.L1.SimpleFunc.setToL1S T (f + g) =
MeasureTheory.L1.SimpleFunc.setToL1S T f + MeasureTheory.L1.SimpleFunc.setToL1S T g
The theorem `MeasureTheory.L1.SimpleFunc.setToL1S_add` states that for a given measure space `α`, types `E` and `F` equipped with normed add commutative group structures, and also where `E` is a real normed space and `F` is a normed space over the real numbers, if we have a function `T` that maps sets of `α` to continuous linear maps from `E` to `F`, and if `T` has the property that it maps any measurable set with measure zero to the zero function, and `T` is `FinMeasAdditive` (i.e., for any two disjoint measurable sets of finite measure, the value of `T` on their union is the sum of its values on each set), then for any two functions `f` and `g` in the subspace of Lp (with p = 1) consisting of equivalence classes of an integrable simple function, the value of the extension of `T` to this subspace at the sum of `f` and `g` is equal to the sum of its values at `f` and `g` separately. This is essentially saying that the extension of `T` to this specific subspace is linear.
More concisely: For a measurable function T from measurable sets of a measure space to continuous linear maps between real normed spaces, satisfying the property of mapping measure zero sets to zero functions and being additive on disjoint sets of finite measure, the extended T is a linear operator on the subspace of L1 functions consisting of equivalence classes of integrable simple functions.
|
MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence
theorem MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
{ι : Type u_7} {l : Filter ι} [inst_5 : l.IsCountablyGenerated] {fs : ι → α → E} {f : α → E} (bound : α → ℝ),
(∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (fs n) μ) →
(∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) →
MeasureTheory.Integrable bound μ →
(∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => fs n a) l (nhds (f a))) →
Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT (fs n)) l
(nhds (MeasureTheory.setToFun μ T hT f))
This theorem is a version of the Lebesgue Dominated Convergence Theorem for filters with a countable basis. In the setting of measure theory, given a measure `μ` and a set function `T` which is finitely additive and dominated by the measure (up to a multiplicative constant `C`), the theorem establishes conditions under which we can switch the limit and the integral. More specifically, it states that if we have a sequence of functions `fs` (indexed over some type `ι` with a countably generated filter `l`) which are almost everywhere strongly measurable with respect to `μ` and are almost everywhere dominated by a certain function `bound`, and if the function `bound` is integrable with respect to `μ`, and if for almost all `a`, the sequence `fs n a` tends to `f a`, then the sequence of integrals of `fs n` with respect to `T` and `μ` tends to the integral of `f` with respect to `T` and `μ`.
More concisely: Given a finitely additive, countably dominated measure `μ`, if a sequence `fs` of almost everywhere strongly measurable functions, almost everywhere dominated by an integrable `bound`, converges almost everywhere to a function `f`, then the integrals of `fs n` with respect to `μ` converge to the integral of `f` with respect to `μ`.
|
MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top
theorem MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : AddCommMonoid β]
{T : Set α → β} {μ' : MeasureTheory.Measure α},
(∀ (s : Set α), MeasurableSet s → ↑↑μ s = ⊤ → ↑↑μ' s = ⊤) →
MeasureTheory.FinMeasAdditive μ T → MeasureTheory.FinMeasAdditive μ' T
The theorem `MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top` states that for any type `α` equipped with a measurable space structure `m`, a measure `μ`, a type `β` equipped with an additive commutative monoid structure, a function `T` from sets of `α` to `β`, and another measure `μ'`, if for every measurable set `s` the condition that the measure `μ` of `s` being infinite implies the measure `μ'` of `s` being infinite holds, then the finiteness and additivity property of `T` with respect to `μ` implies the same property for `T` with respect to `μ'`. This property of `T` is known as `FinMeasAdditive`, and it states that for any two disjoint measurable sets `s` and `t` with finite measure, the value of `T` on the union of `s` and `t` equals the sum of the values of `T` on `s` and `t`.
More concisely: If for all measurable sets `s` with infinite measure under `μ`, the same holds for `μ'`, then a finitely additive `μ`-measurable function `T` from sets of `α` to an additive commutative monoid `β` is also `μ'`-finitely additive.
|
MeasureTheory.SimpleFunc.map_setToSimpleFunc
theorem MeasureTheory.SimpleFunc.map_setToSimpleFunc :
∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} {G : Type u_5} [inst : NormedAddCommGroup F]
[inst_1 : NormedSpace ℝ F] [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F']
[inst_4 : NormedAddCommGroup G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set α → F →L[ℝ] F'),
MeasureTheory.FinMeasAdditive μ T →
∀ {f : MeasureTheory.SimpleFunc α G},
MeasureTheory.Integrable (↑f) μ →
∀ {g : G → F},
g 0 = 0 →
MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.map g f) =
f.range.sum fun x => (T (↑f ⁻¹' {x})) (g x)
This theorem states that for all types `α`, `F`, `F'`, `G`, with `F`, `F'`, and `G` being normed additive commutative groups, and for any measurable space `m` of type `α` and a measure `μ` of this space, if we have a function `T` from the set `α` to the linear space of `F` and `F'` that is finite measure additive with respect to the measure `μ`, then for any simple function `f` from `α` to `G` that is integrable with respect to `μ`, and for any function `g` from `G` to `F` where `g 0 = 0`, the function `T` applied to the simple function obtained by mapping `g` onto `f` is equal to the sum (over the range of `f`) of `T` applied to the preimage of `x` under `f` and `g x`. In mathematical terms, this theorem is stating that the mapping and summation operations commute under certain conditions.
More concisely: For measurable spaces `α`, `F`, `F'`, `G` with normed additive commutative groups `F`, `F'`, `G`, given a measure `μ` on `α`, a finite measure additive function `T` from `α` to the linear space of `F` and `F'`, and a simple, integrable function `f` from `α` to `G`, the function `T` applied to the simple function `g ∘ f` is equal to the sum of `T` applied to `f⁻¹(x)` and `g(x)` over the range of `f`.
|
MeasureTheory.continuous_L1_toL1
theorem MeasureTheory.continuous_L1_toL1 :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m : MeasurableSpace α}
{μ μ' : MeasureTheory.Measure α} (c' : ENNReal) (hc' : c' ≠ ⊤) (hμ'_le : μ' ≤ c' • μ),
Continuous fun f => MeasureTheory.Integrable.toL1 ↑↑f ⋯
This theorem states that for a measurable space `α` and a type `G` that forms a normed additively commutative group, given two measures `μ` and `μ'` on `α` and an extended nonnegative real number `c'` that is not infinity, if `μ'` is less than or equal to `c'` times `μ`, then the function that maps each integrable function `f` from `α` to `G` with respect to the measure `μ` to an integrable function with respect to the measure `μ'`, is a continuous function. In mathematical terms, this theorem ensures the continuity of transformation of integrable functions under measure scaling when the scaling factor is finite.
More concisely: Given measurable spaces `α`, a normed additively commutative group `G`, measurable functions `μ` and `μ'` on `α`, and a finite non-negative real number `c'`, if `μ' ≤ c' * μ` and `f : α → G` is integrable with respect to `μ`, then the function mapping `f` to its integral with respect to `μ'` is continuous.
|
MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero
theorem MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_8} [inst : NormedAddCommGroup β]
{T : Set α → β} {C : ℝ},
MeasureTheory.DominatedFinMeasAdditive μ T C → ∀ {s : Set α}, MeasurableSet s → ↑↑μ s = 0 → T s = 0
This theorem states that for a given type `α`, a measure space `m` over `α`, a measure `μ` on `α`, a type `β` which forms a normed additive commutative group, a set function `T` from `α` to `β`, and a real number `C`, if `T` is a `DominatedFinMeasAdditive` function with respect to `μ` and `C`, then for any measurable set `s` such that the measure of `s` under `μ` is zero, the application of `T` to `s` will yield the zero element of `β`. In essence, this theorem says that a `DominatedFinMeasAdditive` function maps zero-measure sets to the zero element in the target normed additive commutative group.
More concisely: If `T` is a `DominatedFinMeasAdditive` function from a measure space `(α, m)` to a normed additive commutative group `(β, +, ∥⋅∥)` with dominating measure `μ` and constant `C`, then `T(s) = ∥0∥` for any measurable set `s` with `μ(s) = 0`.
|
MeasureTheory.DominatedFinMeasAdditive.of_measure_le
theorem MeasureTheory.DominatedFinMeasAdditive.of_measure_le :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7}
[inst : SeminormedAddCommGroup β] {T : Set α → β} {C : ℝ} {μ' : MeasureTheory.Measure α},
μ ≤ μ' → MeasureTheory.DominatedFinMeasAdditive μ T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive μ' T C
This theorem states that, given a set function `T` from a set `α` to a seminormed additive commutative group `β`, if `μ` and `μ'` are measures on `α` such that `μ` is less than or equal to `μ'`, and `T` is a dominated and finite measure additive with respect to `μ` with a non-negative constant `C`, then `T` is also dominated and finite measure additive with respect to `μ'` with the same constant `C`. Here, a dominated and finite measure additive function is one where the norm of the function on any measurable set is less than or equal to the product of a constant and the measure of the set, and the function satisfies the conditions of finite measure additivity.
More concisely: Given a set function `T` from a set `α` to a seminormed additive commutative group `β`, if `T` is dominated and finite measure additive with respect to a measure `μ` with constant `C` and `μ` is less than or equal to `μ'`, then `T` is dominated and finite measure additive with respect to `μ'` with the same constant `C`.
|
MeasureTheory.setToFun_congr_ae
theorem MeasureTheory.setToFun_congr_ae :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} {f g : α → E}
(hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
μ.ae.EventuallyEq f g → MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T hT g
This theorem, `MeasureTheory.setToFun_congr_ae`, states that for any types `α`, `E`, and `F`, given that `E` and `F` form normed additively commutative groups and are also normed spaces over the real numbers, and that `F` is a complete space. If we also have a measurable space `α` and a measure `μ` on it, a function `T` from the set of `α` to the space of bounded linear maps from `E` to `F`, and real number `C`, then for any two functions `f` and `g` from `α` to `E`, if `T` is a dominated finitely additive measure with respect to `μ` and `C`, and `f` is almost everywhere equal to `g` with respect to the measure `μ`, then applying the `setToFun` function to `f` and `g` with these settings will yield the same result.
In other words, if two functions are almost everywhere equal with respect to a certain measure, the function that maps sets to bounded linear maps treats them equivalently under a dominated finitely additive measure.
More concisely: If `α` is a measurable space, `E` and `F` are normed additively commutative groups and complete normed spaces over the real numbers, `μ` is a measure on `α`, `T` is a dominated finitely additive measure from `α` to the bounded linear maps from `E` to `F`, and `f` and `g` are almost everywhere equal `α`-measurable functions from `α` to `E`, then `setToFun(f)` and `setToFun(g)` are equal as elements of the space of functions from `α` to the space of bounded linear maps from `E` to `F`.
|