Convergence of integrals of bounded operator fields #
Bounded operator fields converging almost everywhere preserve convergence of integrated
pairings with velocities converging in L¹. Separating the changes of field and velocity
avoids a pointwise bound on the approximating velocities.
theorem
MeasureTheory.tendsto_integral_clm_apply_of_integral_norm_sub
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{μ : Measure α}
{ωn : ℕ → α → E →L[ℝ] F}
{ω : α → E →L[ℝ] F}
{vn : ℕ → α → E}
{v : α → E}
{C : ℝ}
(hωn : ∀ (n : ℕ), AEStronglyMeasurable (ωn n) μ)
(hω : AEStronglyMeasurable ω μ)
(hboundn : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖ωn n x‖ ≤ C)
(hbound : ∀ᵐ (x : α) ∂μ, ‖ω x‖ ≤ C)
(hωconv : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => ωn n x) Filter.atTop (nhds (ω x)))
(hvn : ∀ (n : ℕ), Integrable (vn n) μ)
(hv : Integrable v μ)
(hvconv : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), ‖vn n x - v x‖ ∂μ) Filter.atTop (nhds 0))
:
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), (ωn n x) (vn n x) ∂μ) Filter.atTop (nhds (∫ (x : α), (ω x) (v x) ∂μ))
Bounded operator fields converging almost everywhere can be paired with velocities
converging in L¹. This gives convergence of the actual Bochner integrals.
theorem
MeasureTheory.tendsto_integral_mul_of_integral_abs_sub
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{wn : ℕ → α → ℝ}
{w R : α → ℝ}
{C : ℝ}
(hwn : ∀ (n : ℕ), Integrable (wn n) μ)
(hw : Integrable w μ)
(hR : AEStronglyMeasurable R μ)
(hbound : ∀ᵐ (x : α) ∂μ, |R x| ≤ C)
(hconv : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), |wn n x - w x| ∂μ) Filter.atTop (nhds 0))
:
Multiplying L¹-convergent real functions by a fixed bounded measurable function
preserves convergence of their actual integrals.