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
for L1 functions by extending the integral on simple functions. See the file
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
for the integral of functions
and corresponding API.
Main definitions #
The Bochner integral is defined through the extension process described in the file
Mathlib/MeasureTheory/Integral/SetToL1.lean
, which follows these steps:
Define the integral of the indicator of a set. This is
weightedSMul μ s x = μ.real s * x
.weightedSMul μ
is shown to be linear in the valuex
andDominatedFinMeasAdditive
(defined in the fileMathlib/MeasureTheory/Integral/SetToL1.lean
) 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.
Notations #
α →ₛ E
: simple functions (defined inMathlib/MeasureTheory/Function/SimpleFunc.lean
)α →₁[μ] E
: functions in L1 space, i.e., equivalence classes of integrable functions (defined inMathlib/MeasureTheory/Function/LpSpace/Basic.lean
)α →₁ₛ[μ] E
: simple functions in L1 space, i.e., equivalence classes of integrable simple functions (defined inMathlib/MeasureTheory/Function/SimpleFuncDense
)
We also define notations for integral on a set, which are described in the file
Mathlib/MeasureTheory/Integral/SetIntegral.lean
.
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 => μ.real s • x
. The extension
of that set function through setToL1
gives the Bochner integral of L1 functions.
Equations
- MeasureTheory.weightedSMul μ s = μ.real s • 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, μ.real (f ⁻¹' {x}) • 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 ℝ.
Instances For
The Bochner integral in L1 space