ae_le_const_iff_forall_gt_measure_zero

English

If f,g are AEMeasurable and for all finite-measure sets s we have ∫_s f ≤ ∫_s g, then f ≤ a.e. g.

Русский

Пусть f,g – AEMеасемабльны и для всех множеств s с конечной мерой имеем ∫_s f ≤ ∫_s g, тогда f ≤ a.e. g.

LaTeX

$$$$ f \le^{\mathrm{ae}}_{\mu} g $$$$

Lean4

theorem ae_le_const_iff_forall_gt_measure_zero {β} [LinearOrder β] [TopologicalSpace β] [OrderTopology β]
    [FirstCountableTopology β] {μ : Measure α} (f : α → β) (c : β) :
    (∀ᵐ x ∂μ, f x ≤ c) ↔ ∀ b, c < b → μ {x | b ≤ f x} = 0 :=
  ae_const_le_iff_forall_lt_measure_zero (β := βᵒᵈ) _ _

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