Almost-everywhere vanishing outside the topological support

If the topological support tsupport f of a function f : α → β is contained in a set s, then f vanishes everywhere on the open set (tsupport f)ᶜ, which contains sᶜ and is measurable in any OpensMeasurableSpace. Consequently f =ᵐ[μ.restrict sᶜ] 0 without any measurability assumption on s or f.

The file also records the total mass of a rescaled restriction, and that normalized restrictions to sets of positive mass, scaled by the smallest mass over their number, sum to at most the measure.

Main results

• MeasureTheory.Measure.smul_restrict_univ: (s • μ.restrict A) univ = s * μ A.
• MeasureTheory.Measure.smul_sum_inv_smul_restrict_le: the normalized restrictions of a measure to finitely many sets, scaled by the smallest mass over their number, sum to at most the measure.
• MeasureTheory.ae_restrict_compl_eq_zero_of_tsupport_subset: if tsupport f ⊆ s, then f =ᵐ[μ.restrict sᶜ] 0.

theorem MeasureTheory.ae_restrict_compl_eq_zero_of_tsupport_subset {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [Zero β] {μ : Measure α} {s : Set α} {f : α → β} (hf : tsupport f ⊆ s) : f =ᵐ[μ.restrict sᶜ] 0

A function whose topological support lies in s vanishes almost everywhere on sᶜ.

theorem MeasureTheory.Measure.smul_restrict_univ {α : Type u_1} [MeasurableSpace α] (s : ENNReal) (μ : Measure α) (A : Set α) : (s • μ.restrict A) Set.univ = s * μ A

The total mass of the restriction to A of a measure, rescaled by s.

theorem MeasureTheory.Measure.smul_sum_inv_smul_restrict_le {α : Type u_1} [MeasurableSpace α] {π : Measure α} {n : ℕ} {W : Fin n → Set α} {j : Fin n} (hj : ∀ (i : Fin n), π (W j) ≤ π (W i)) : ((π (W j) / ↑n) • sum fun (i : Fin n) => (π (W i))⁻¹ • π.restrict (W i)) ≤ π

Scaling the normalized restrictions (π (W i))⁻¹ • π.restrict (W i) of a measure π by π (W j) / n, where W j has minimal mass, and summing over i : Fin n stays below π.