Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.tendsto_setIntegral_of_L1

∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {ι : Type u_7} (f : X → E),
  MeasureTheory.AEStronglyMeasurable f μ.variation →
    ∀ {F_1 : ι → X → E} {l : Filter ι},
      (∀ᶠ (i : ι) in l, μ.Integrable (F_1 i)) →
        Filter.Tendsto (fun i => ∫⁻ (x : X), ‖F_1 i x - f x‖ₑ ∂μ.variation) l (nhds 0) →
          ∀ (s : Set X),
            Filter.Tendsto (fun i => ∫ᵛ (x : X) in s, F_1 i x ∂[B; μ]) l (nhds ∫ᵛ (x : X) in s, f x ∂[B; μ])

If F i → f in L1, then ∫ᵛ x in s, F i x ∂[B; μ] → ∫ᵛ x in s, f x ∂[B; μ].

Defined in

Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Cited by

1 results in Mathlib

Foundations

Depth 246 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNormedSpaceNormedSpaceNormedSpace