tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure

English

If μ is a finite measure and A_i are measurable with indicators tending pointwise to the indicator of A, then μ(A_i) → μ(A).

Русский

Если μ — конечная мера и A_i измеримы, индикаторы которых сходятся точечно к индикатору A, то μ(A_i) сходится к μ(A).

LaTeX

$$$ \mathrm{Tendsto}\ i \mapsto \mu(A_i)\; L\; \mathcal{N}(\mu(A)) \,\text{ under finiteness assumptions}$$$

Lean4

/-- If `μ` is a finite measure and the indicators of measurable sets `Aᵢ` tend pointwise
almost everywhere to the indicator of a measurable set `A`, then the measures `μ Aᵢ` tend to
the measure `μ A`. -/
theorem tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure {μ : Measure α} [IsFiniteMeasure μ]
    (A_mble : MeasurableSet A) (As_mble : ∀ i, MeasurableSet (As i)) (h_lim : ∀ᵐ x ∂μ, ∀ᶠ i in L, x ∈ As i ↔ x ∈ A) :
    Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A)) :=
  tendsto_measure_of_ae_tendsto_indicator L A_mble As_mble MeasurableSet.univ (measure_ne_top μ univ)
    (Eventually.of_forall (fun i ↦ subset_univ (As i))) h_lim

Похожие утверждения