English
If a measurable function f is integrable on s and f(x) ≠ 0 on s, then restricting μ to toMeasurable μ s equals restricting to s.
Русский
Если функция f измерима и интегрируема на s и не обнуляется на s, ограничение μ на toMeasurable μ s совпадает с ограничением на s.
LaTeX
$$hf ∈ IntegrableOn f s μ ∧ ∀ x ∈ s, ∥f x∥ ≠ 0 ⇒ μ.restrict (toMeasurable μ s) = μ.restrict s$$
Lean4
/-- If a function is integrable on a set `s` and nonzero there, then the measurable hull of `s` is
well behaved: the restriction of the measure to `toMeasurable μ s` coincides with its restriction
to `s`. -/
theorem restrict_toMeasurable {f : α → ε'} (hf : IntegrableOn f s μ) (h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0) :
μ.restrict (toMeasurable μ s) = μ.restrict s :=
by
rcases exists_seq_strictAnti_tendsto' ENNReal.zero_lt_top with ⟨u, _, u_pos, u_lim⟩
let v n := toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖ₑ}
have A : ∀ n, μ (s ∩ v n) ≠ ∞ := by
intro n
rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]
exact (hf.measure_enorm_ge_lt_top (u_pos n).1 (u_pos n).2.ne).ne
apply Measure.restrict_toMeasurable_of_cover _ A
intro x hx
obtain ⟨n, hn⟩ : ∃ n, u n < ‖f x‖ₑ := ((tendsto_order.1 u_lim).2 _ (pos_of_ne_zero (h's x hx))).exists
exact
mem_iUnion.2
⟨n, subset_toMeasurable _ _ hn.le⟩
-- TODO: investigate generalising this section to e-seminormed monoids
