Set integral bounds from closed subsets

On a pseudometrizable space, a bound ‖∫ x in F, f x ∂μ‖ₑ ≤ ∫⁻ x in F, k x ∂μ on every closed subset F of a measurable set B on which f is integrable extends to B itself. The proof approximates B from inside by a closed set, for the finite and hence weakly regular measure with density ‖f‖ₑ on B. When B lies in a compact set, its closed subsets are compact, so bounds on compact sets extend to measurable subsets of compact sets.

Main statements

• TauCeti.enorm_setIntegral_le_of_forall_isClosed_subset: the bound on closed subsets of B gives the bound on B.

theorem TauCeti.enorm_setIntegral_le_of_forall_isClosed_subset {X : Type u_1} {G : Type u_2} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [MeasurableSpace X] [BorelSpace X] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : MeasureTheory.Measure X} {f : X → G} {k : X → ENNReal} {B : Set X} (hf : MeasureTheory.IntegrableOn f B μ) (hB : MeasurableSet B) (hF : ∀ F ⊆ B, IsClosed F → ‖∫ (x : X) in F, f x ∂μ‖ₑ ≤ ∫⁻ (x : X) in F, k x ∂μ) : ‖∫ (x : X) in B, f x ∂μ‖ₑ ≤ ∫⁻ (x : X) in B, k x ∂μ

Inner regularity of set integral bounds. On a pseudometrizable space, if ‖∫ x in F, f x ∂μ‖ₑ ≤ ∫⁻ x in F, k x ∂μ for every closed subset F of a measurable set B on which f is integrable, then the same bound holds on B.