ae_eq_zero_of_forall_setIntegral_eq_zero

English

The ae-limit is ae-unique (variant): if the Tendsto conditions hold almost everywhere for two functions, they are ae-equal.

Русский

Ae-граница уникальна (вариант): если условия Tendsto почти везде выполняются для двух функций, они ae-равны.

LaTeX

$$$\\text{tendsto\_nhds\_unique}$ (вариант) implies $g =^{\\mu} h$$$

Lean4

theorem ae_eq_zero_of_forall_setIntegral_eq_zero (f : Lp E p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    (hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
    (hf_zero : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 :=
  AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero hf_int_finite hf_zero
    (Lp.finStronglyMeasurable _ hp_ne_zero hp_ne_top).aefinStronglyMeasurable

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