Bochner integral #
The Bochner integral extends the definition of the Lebesgue integral to functions that map from a measure space into a Banach space (complete normed vector space). It is constructed here by extending the integral on simple functions.
Main definitions #
The Bochner integral is defined through the extension process described in the file SetToL1
,
which follows these steps:
Define the integral of the indicator of a set. This is
weightedSMul μ s x = (μ s).toReal * x
.weightedSMul μ
is shown to be linear in the valuex
andDominatedFinMeasAdditive
(defined in the fileSetToL1
) with respect to the sets
.Define the integral on simple functions of the type
SimpleFunc α E
(notation :α →ₛ E
) whereE
is a real normed space. (SeeSimpleFunc.integral
for details.)Transfer this definition to define the integral on
L1.simpleFunc α E
(notation :α →₁ₛ[μ] E
), seeL1.simpleFunc.integral
. Show that this integral is a continuous linear map fromα →₁ₛ[μ] E
toE
.Define the Bochner integral on L1 functions by extending the integral on integrable simple functions
α →₁ₛ[μ] E
usingContinuousLinearMap.extend
and the fact that the embedding ofα →₁ₛ[μ] E
intoα →₁[μ] E
is dense.Define the Bochner integral on functions as the Bochner integral of its equivalence class in L1 space, if it is in L1, and 0 otherwise.
The result of that construction is ∫ a, f a ∂μ
, which is definitionally equal to
setToFun (dominatedFinMeasAdditive_weightedSMul μ) f
. Some basic properties of the integral
(like linearity) are particular cases of the properties of setToFun
(which are described in the
file SetToL1
).
Main statements #
- Basic properties of the Bochner integral on functions of type
α → E
, whereα
is a measure space andE
is a real normed space.
integral_zero
:∫ 0 ∂μ = 0
integral_add
:∫ x, f x + g x ∂μ = ∫ x, f ∂μ + ∫ x, g x ∂μ
integral_neg
:∫ x, - f x ∂μ = - ∫ x, f x ∂μ
integral_sub
:∫ x, f x - g x ∂μ = ∫ x, f x ∂μ - ∫ x, g x ∂μ
integral_smul
:∫ x, r • f x ∂μ = r • ∫ x, f x ∂μ
integral_congr_ae
:f =ᵐ[μ] g → ∫ x, f x ∂μ = ∫ x, g x ∂μ
norm_integral_le_integral_norm
:‖∫ x, f x ∂μ‖ ≤ ∫ x, ‖f x‖ ∂μ
- Basic properties of the Bochner integral on functions of type
α → ℝ
, whereα
is a measure space.
integral_nonneg_of_ae
:0 ≤ᵐ[μ] f → 0 ≤ ∫ x, f x ∂μ
integral_nonpos_of_ae
:f ≤ᵐ[μ] 0 → ∫ x, f x ∂μ ≤ 0
integral_mono_ae
:f ≤ᵐ[μ] g → ∫ x, f x ∂μ ≤ ∫ x, g x ∂μ
integral_nonneg
:0 ≤ f → 0 ≤ ∫ x, f x ∂μ
integral_nonpos
:f ≤ 0 → ∫ x, f x ∂μ ≤ 0
integral_mono
:f ≤ᵐ[μ] g → ∫ x, f x ∂μ ≤ ∫ x, g x ∂μ
- Propositions connecting the Bochner integral with the integral on
ℝ≥0∞
-valued functions, which is calledlintegral
and has the notation∫⁻
.
integral_eq_lintegral_pos_part_sub_lintegral_neg_part
:∫ x, f x ∂μ = ∫⁻ x, f⁺ x ∂μ - ∫⁻ x, f⁻ x ∂μ
, wheref⁺
is the positive part off
andf⁻
is the negative part off
.integral_eq_lintegral_of_nonneg_ae
:0 ≤ᵐ[μ] f → ∫ x, f x ∂μ = ∫⁻ x, f x ∂μ
(In the file
DominatedConvergence
)tendsto_integral_of_dominated_convergence
: the Lebesgue dominated convergence theorem(In the file
SetIntegral
) integration commutes with continuous linear maps.
ContinuousLinearMap.integral_comp_comm
LinearIsometry.integral_comp_comm
Notes #
Some tips on how to prove a proposition if the API for the Bochner integral is not enough so that you need to unfold the definition of the Bochner integral and go back to simple functions.
One method is to use the theorem Integrable.induction
in the file SimpleFuncDenseLp
(or one
of the related results, like Lp.induction
for functions in Lp
), which allows you to prove
something for an arbitrary integrable function.
Another method is using the following steps.
See integral_eq_lintegral_pos_part_sub_lintegral_neg_part
for a complicated example, which proves
that ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻
, with the first integral sign being the Bochner integral of a real-valued
function f : α → ℝ
, and second and third integral sign being the integral on ℝ≥0∞
-valued
functions (called lintegral
). The proof of integral_eq_lintegral_pos_part_sub_lintegral_neg_part
is scattered in sections with the name posPart
.
Here are the usual steps of proving that a property p
, say ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻
, holds for all
functions :
First go to the
L¹
space.For example, if you see
ENNReal.toReal (∫⁻ a, ENNReal.ofReal <| ‖f a‖)
, that is the norm off
inL¹
space. Rewrite usingL1.norm_of_fun_eq_lintegral_norm
.Show that the set
{f ∈ L¹ | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}
is closed inL¹
usingisClosed_eq
.Show that the property holds for all simple functions
s
inL¹
space.Typically, you need to convert various notions to their
SimpleFunc
counterpart, using lemmas likeL1.integral_coe_eq_integral
.Since simple functions are dense in
L¹
,
univ = closure {s simple}
= closure {s simple | ∫ s = ∫⁻ s⁺ - ∫⁻ s⁻} : the property holds for all simple functions
⊆ closure {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}
= {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} : closure of a closed set is itself
Use isClosed_property
or DenseRange.induction_on
for this argument.
Notations #
α →ₛ E
: simple functions (defined inMeasureTheory/Integration
)α →₁[μ] E
: functions in L1 space, i.e., equivalence classes of integrable functions (defined inMeasureTheory/LpSpace
)α →₁ₛ[μ] E
: simple functions in L1 space, i.e., equivalence classes of integrable simple functions (defined inMeasureTheory/SimpleFuncDense
)∫ a, f a ∂μ
: integral off
with respect to a measureμ
∫ a, f a
: integral off
with respect tovolume
, the default measure on the ambient type
We also define notations for integral on a set, which are described in the file
MeasureTheory/SetIntegral
.
Note : ₛ
is typed using \_s
. Sometimes it shows as a box if the font is missing.
Tags #
Bochner integral, simple function, function space, Lebesgue dominated convergence theorem
Given a set s
, return the continuous linear map fun x => (μ s).toReal • x
. The extension
of that set function through setToL1
gives the Bochner integral of L1 functions.
Equations
- MeasureTheory.weightedSMul μ s = (μ s).toReal • ContinuousLinearMap.id ℝ F
Instances For
Positive part of a simple function.
Equations
- f.posPart = MeasureTheory.SimpleFunc.map (fun (b : E) => max b 0) f
Instances For
Negative part of a simple function.
Instances For
The Bochner integral of simple functions #
Define the Bochner integral of simple functions of the type α →ₛ β
where β
is a normed group,
and prove basic property of this integral.
Bochner integral of simple functions whose codomain is a real NormedSpace
.
This is equal to ∑ x ∈ f.range, (μ (f ⁻¹' {x})).toReal • x
(see integral_eq
).
Equations
Instances For
The Bochner integral is equal to a sum over any set that includes f.range
(except 0
).
Calculate the integral of g ∘ f : α →ₛ F
, where f
is an integrable function from α
to E
and g
is a function from E
to F
. We require g 0 = 0
so that g ∘ f
is integrable.
SimpleFunc.integral
and SimpleFunc.lintegral
agree when the integrand has type
α →ₛ ℝ≥0∞
. But since ℝ≥0∞
is not a NormedSpace
, we need some form of coercion.
See integral_eq_lintegral
for a simpler version.
SimpleFunc.bintegral
and SimpleFunc.integral
agree when the integrand has type
α →ₛ ℝ≥0∞
. But since ℝ≥0∞
is not a NormedSpace
, we need some form of coercion.
Positive part of a simple function in L1 space.
Equations
Instances For
Negative part of a simple function in L1 space.
Instances For
The Bochner integral of L1
#
Define the Bochner integral on α →₁ₛ[μ] E
by extension from the simple functions α →₁ₛ[μ] E
,
and prove basic properties of this integral.
The Bochner integral over simple functions in L1 space.
Equations
Instances For
The Bochner integral over simple functions in L1 space as a continuous linear map.
Equations
- MeasureTheory.L1.SimpleFunc.integralCLM' α E 𝕜 μ = { toFun := MeasureTheory.L1.SimpleFunc.integral, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯
Instances For
The Bochner integral over simple functions in L1 space as a continuous linear map over ℝ.
Equations
Instances For
The Bochner integral in L1 space as a continuous linear map.
Equations
- MeasureTheory.L1.integralCLM' 𝕜 = (MeasureTheory.L1.SimpleFunc.integralCLM' α E 𝕜 μ).extend (MeasureTheory.Lp.simpleFunc.coeToLp α E 𝕜) ⋯ ⋯
Instances For
The Bochner integral in L1 space as a continuous linear map over ℝ.
Equations
- MeasureTheory.L1.integralCLM = MeasureTheory.L1.integralCLM' ℝ
Instances For
The Bochner integral in L1 space
Equations
Instances For
The Bochner integral on functions #
Define the Bochner integral on functions generally to be the L1
Bochner integral, for integrable
functions, and 0 otherwise; prove its basic properties.
The Bochner integral
Equations
Instances For
In the notation for integrals, an expression like ∫ x, g ‖x‖ ∂μ
will not be parsed correctly,
and needs parentheses. We do not set the binding power of r
to 0
, because then
∫ x, f x = 0
will be parsed incorrectly.
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Bochner integral
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Bochner integral
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Bochner integral
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Bochner integral
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If f
has finite integral, then ∫ x in s, f x ∂μ
is absolutely continuous in s
: it tends
to zero as μ s
tends to zero.
Alias of MeasureTheory.HasFiniteIntegral.tendsto_setIntegral_nhds_zero
.
If f
has finite integral, then ∫ x in s, f x ∂μ
is absolutely continuous in s
: it tends
to zero as μ s
tends to zero.
If f
is integrable, then ∫ x in s, f x ∂μ
is absolutely continuous in s
: it tends
to zero as μ s
tends to zero.
Alias of MeasureTheory.Integrable.tendsto_setIntegral_nhds_zero
.
If f
is integrable, then ∫ x in s, f x ∂μ
is absolutely continuous in s
: it tends
to zero as μ s
tends to zero.
If F i → f
in L1
, then ∫ x, F i x ∂μ → ∫ x, f x ∂μ
.
If F i → f
in L1
, then ∫ x, F i x ∂μ → ∫ x, f x ∂μ
.
If F i → f
in L1
, then ∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ
.
Alias of MeasureTheory.tendsto_setIntegral_of_L1
.
If F i → f
in L1
, then ∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ
.
If F i → f
in L1
, then ∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ
.
Alias of MeasureTheory.tendsto_setIntegral_of_L1'
.
If F i → f
in L1
, then ∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ
.
The Bochner integral of a real-valued function f : α → ℝ
is the difference between the
integral of the positive part of f
and the integral of the negative part of f
.
Monotone convergence theorem for real-valued functions and Bochner integrals
Monotone convergence theorem for real-valued functions and Bochner integrals
If a monotone sequence of functions has an upper bound and the sequence of integrals of these functions tends to the integral of the upper bound, then the sequence of functions converges almost everywhere to the upper bound.
If an antitone sequence of functions has a lower bound and the sequence of integrals of these functions tends to the integral of the lower bound, then the sequence of functions converges almost everywhere to the lower bound.
Alias of MeasureTheory.setIntegral_dirac'
.
Alias of MeasureTheory.setIntegral_dirac
.
Markov's inequality also known as Chebyshev's first inequality.
Hölder's inequality for the integral of a product of norms. The integral of the product of two
norms of functions is bounded by the product of their ℒp
and ℒq
seminorms when p
and q
are
conjugate exponents.
Hölder's inequality for functions α → ℝ
. The integral of the product of two nonnegative
functions is bounded by the product of their ℒp
and ℒq
seminorms when p
and q
are conjugate
exponents.
Simple function seen as simple function of a larger MeasurableSpace
.
Equations
- MeasureTheory.SimpleFunc.toLargerSpace hm f = { toFun := f.toFun, measurableSet_fiber' := ⋯, finite_range' := ⋯ }
Instances For
Alias of MeasureTheory.eLpNorm_one_le_of_le
.
Alias of MeasureTheory.eLpNorm_one_le_of_le'
.
Positivity extension for integrals.
This extension only proves non-negativity, strict positivity is more delicate for integration and requires more assumptions.