Pushing a weighted measure forward

A weight travels with the measure it weights: along a measurable equivalence e, the image of μ.withDensity f is the image of μ weighted by f ∘ e.symm. Mathlib has this only for the special case of a Radon–Nikodym derivative, in MeasurableEmbedding.map_withDensity_rnDeriv.

Combined with a rescaling law for the measure itself, such as MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar on a finite-dimensional real normed space, this gives the change-of-variables formula for a density under an invertible affine map. That is the shape a location–scale family needs: it turns a density for the standard member of the family into a density for every other member.

A map that is injective only on part of the line admits the same change of variables there, at the price of restricting Lebesgue measure to that part and inserting the absolute derivative into the weight. The substitution x = t ^ 2 on the positive half-line is the case a square-root law needs.

Finally, a weight exp ∘ g whose exponent is bounded above almost everywhere keeps a finite measure finite.

Main statements

• MeasurableEquiv.map_withDensity: the image of a weighted measure along a measurable equivalence is the image measure weighted by the transported weight.
• TauCeti.Probability.map_abs_withDensity: the image of a weighted Lebesgue measure under absolute value has the folded density.
• MeasureTheory.Measure.map_withDensity_eq_withDensity: a pointwise factorization of one weight through a map whose Jacobian identity is already known transports that weight to the image.
• MeasureTheory.Measure.map_withDensity_comp: the image of a measure weighted by a pulled-back weight is the image measure weighted by that weight.
• MeasurableEmbedding.map_withDensity_comp: the same along a measurable embedding, with no measurability of the weight.
• MeasureTheory.Measure.map_add_right_withDensity: translating a weighted right-invariant measure translates the weight.
• MeasureTheory.Measure.map_affine_withDensity: the image of a weighted Haar measure under an invertible affine map is that Haar measure weighted by the substituted density, rescaled by the constant Jacobian factor.
• MeasureTheory.Measure.rnDeriv_map_affine: the Radon–Nikodym derivative of an affine image is obtained by the same substitution and Jacobian factor.
• MeasureTheory.Measure.support_withDensity_eq: weighting a measure by an almost-everywhere nonzero density preserves its topological support.
• MeasureTheory.Measure.support_withDensity_eq_closure_of_subset: a density positive on an open set and zero off its closure has topological support equal to that closure.
• MeasureTheory.Measure.support_withDensity_eq_closure: the special case where the function support is exactly the open set.
• MeasureTheory.Measure.support_withDensity_ofReal: a continuous nonnegative real density has the same topological support as the measure it defines.
• MeasureTheory.absolutelyContinuous_withDensity_ofReal: a measure is absolutely continuous with respect to itself weighted by an almost-everywhere positive real density.
• MeasureTheory.continuous_eq_of_withDensity_ofReal_eq: continuous nonnegative real densities presenting the same weighted measure are equal pointwise.
• MeasureTheory.isFiniteMeasure_withDensity_ofReal_exp: a finite measure weighted by exp ∘ g, with g bounded above almost everywhere, is finite.
• TauCeti.MeasureTheory.map_withDensity_abs_deriv_mul: the change of variables on the real line along a map injective and differentiable on a measurable set.
• TauCeti.MeasureTheory.map_sq_withDensity_restrict_Ioi: its instance for squaring on the positive half-line.

theorem MeasurableEquiv.map_withDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (μ : MeasureTheory.Measure α) (f : α → ENNReal) : MeasureTheory.Measure.map (⇑e) (μ.withDensity f) = (MeasureTheory.Measure.map (⇑e) μ).withDensity fun (y : β) => f (e.symm y)

A weight travels with the measure it weights. Pushing μ.withDensity f forward along a measurable equivalence e gives the pushforward of μ weighted by f ∘ e.symm. The weight f is arbitrary; no measurability of it is required.

theorem TauCeti.Probability.map_abs_withDensity {f : ℝ → ENNReal} (hf : Measurable f) : MeasureTheory.Measure.map (fun (x : ℝ) => |x|) (MeasureTheory.volume.withDensity f) = MeasureTheory.volume.withDensity ((Set.Ioi 0).indicator fun (x : ℝ) => f x + f (-x))

The folded density. If μ has density f with respect to Lebesgue measure, then the folded law has density f x + f (-x) on the positive half-line and 0 elsewhere.

theorem MeasureTheory.Measure.support_withDensity_eq {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} {f : X → ENNReal} (hf : AEMeasurable f μ) (hf_ne_zero : ∀ᵐ (x : X) ∂μ, f x ≠ 0) : (μ.withDensity f).support = μ.support

Weighting a measure by an almost-everywhere nonzero density preserves its topological support.

theorem MeasureTheory.Measure.support_withDensity_eq_closure_of_subset {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [μ.IsOpenPosMeasure] {f : X → ENNReal} {U : Set X} (hf : Measurable f) (hU : IsOpen U) (hU_support : U ⊆ Function.support f) (hsupport_closure : Function.support f ⊆ closure U) : (μ.withDensity f).support = closure U

If a measurable density is positive on an open set and zero off its closure, then its weighted measure has topological support equal to that closure, provided the reference measure is positive on nonempty open sets.

This form allows the density to take arbitrary values on the boundary.

theorem MeasureTheory.Measure.support_withDensity_eq_closure {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [μ.IsOpenPosMeasure] {f : X → ENNReal} {U : Set X} (hf : Measurable f) (hU : IsOpen U) (hsupp : Function.support f = U) : (μ.withDensity f).support = closure U

If a measurable density is positive exactly on an open set, then its weighted measure has topological support equal to the closure of that set, provided the reference measure is positive on nonempty open sets.

theorem MeasureTheory.Measure.support_withDensity_ofReal {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : Measure X} [μ.IsOpenPosMeasure] {f : X → ℝ} (hf : Continuous f) (hf0 : 0 ≤ f) : (μ.withDensity fun (x : X) => ENNReal.ofReal (f x)).support = tsupport f

The support of a measure with continuous nonnegative real density is the topological support of that density, provided the reference measure is positive on nonempty open sets.

theorem MeasureTheory.Measure.map_withDensity_eq_withDensity {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {f : α → β} {jac h : α → ENNReal} {g : β → ENNReal} (hf : Measurable f) (hjac : Measurable jac) (hg : Measurable g) (hmap : map f (μ.withDensity jac) = ν) (hh : ∀ᵐ (z : α) ∂μ, jac z * g (f z) = h z) : map f (μ.withDensity h) = ν.withDensity g

A Jacobian identity transports a weight. Suppose f carries μ weighted by jac to ν, which is the Jacobian formula for f when μ and ν are the restrictions of a Haar measure to the two regions f maps onto each other. If a weight h upstairs factors almost everywhere as jac times a weight g downstairs, then f carries μ.withDensity h to ν.withDensity g: the change of variables for measures upgrades to one for densities.

This is the step that turns a pointwise density computation into an identity of measures, so the work in an application is the factorization hypothesis alone.

theorem MeasureTheory.Measure.map_withDensity_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {f : α → β} {g : β → ENNReal} (hf : Measurable f) (hg : Measurable g) : map f (μ.withDensity (g ∘ f)) = (map f μ).withDensity g

A pulled-back weight is pushed forward. The image under a measurable f of μ weighted by g ∘ f is the image of μ weighted by g. This is the case of map_withDensity_eq_withDensity with trivial Jacobian.

theorem MeasurableEmbedding.map_withDensity_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → β} (hf : MeasurableEmbedding f) (g : β → ENNReal) : MeasureTheory.Measure.map f (μ.withDensity (g ∘ f)) = (MeasureTheory.Measure.map f μ).withDensity g

A pulled-back weight is pushed forward along a measurable embedding. Unlike map_withDensity_comp, no measurability of the weight g is needed.

@[simp]

theorem MeasureTheory.Measure.map_add_right_withDensity {G : Type u_3} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddRightInvariant] (f : G → ENNReal) (y : G) : map (fun (x : G) => x + y) (μ.withDensity f) = μ.withDensity fun (x : G) => f (x - y)

Translating a weighted invariant measure translates its weight. If μ is invariant under right translation, then pushing μ.withDensity f forward along x ↦ x + y gives μ weighted by x ↦ f (x - y). This is how the location parameter of a location family on the line moves under translation.

theorem MeasureTheory.Measure.map_affine_withDensity {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (A : E ≃L[ℝ] E) (c : E) (g : E → ENNReal) : map (fun (x : E) => c + A x) (μ.withDensity g) = μ.withDensity fun (y : E) => ENNReal.ofReal |(LinearMap.det ↑↑A)⁻¹| * g (A.symm (y - c))

Change of variables for a density under an invertible affine map. The image of μ.withDensity g under x ↦ c + A x is μ weighted by the substituted density y ↦ g (A⁻¹ (y - c)), scaled by the constant Jacobian factor |det A|⁻¹.

theorem MeasureTheory.Measure.rnDeriv_map_affine {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (A : E ≃L[ℝ] E) (c : E) (ν : Measure E) [SFinite ν] : (map (fun (x : E) => c + A x) ν).rnDeriv μ =ᵐ[μ] fun (y : E) => ENNReal.ofReal |(LinearMap.det ↑↑A)⁻¹| * ν.rnDeriv μ (A.symm (y - c))

Radon–Nikodym derivative under an invertible affine map. The derivative of the image of an s-finite measure under x ↦ c + A x, relative to an additive Haar measure, is obtained by substituting the inverse affine map and multiplying by the reciprocal absolute determinant.

theorem MeasureTheory.absolutelyContinuous_withDensity_ofReal {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {w : α → ℝ} (hwm : AEMeasurable w μ) (hwpos : ∀ᵐ (x : α) ∂μ, 0 < w x) : μ.AbsolutelyContinuous (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))

A measure is absolutely continuous with respect to itself weighted by an almost-everywhere positive real density: the weight ENNReal.ofReal ∘ w vanishes only on a null set, so weighting destroys no null sets.

theorem MeasureTheory.continuous_eq_of_withDensity_ofReal_eq {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {ν : Measure X} [SigmaFinite ν] [ν.IsOpenPosMeasure] {p q : X → ℝ} (hp : Continuous p) (hq : Continuous q) (hp0 : 0 ≤ p) (hq0 : 0 ≤ q) (h : (ν.withDensity fun (x : X) => ENNReal.ofReal (p x)) = ν.withDensity fun (x : X) => ENNReal.ofReal (q x)) : p = q

Continuous nonnegative real densities that present the same measure are equal pointwise.

theorem MeasureTheory.isFiniteMeasure_withDensity_ofReal_exp {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] {g : α → ℝ} {M : ℝ} (hgM : ∀ᵐ (x : α) ∂μ, g x ≤ M) : IsFiniteMeasure (μ.withDensity fun (x : α) => ENNReal.ofReal (Real.exp (g x)))

A measure with log-density bounded above almost everywhere against a finite measure is finite.

theorem TauCeti.MeasureTheory.map_withDensity_abs_deriv_mul {s : Set ℝ} {φ φ' : ℝ → ℝ} {f : ℝ → ENNReal} (hs : MeasurableSet s) (hφ' : ∀ x ∈ s, HasDerivWithinAt φ (φ' x) s x) (hinj : Set.InjOn φ s) : MeasureTheory.Measure.map φ ((MeasureTheory.volume.restrict s).withDensity fun (t : ℝ) => ENNReal.ofReal |φ' t| * f (φ t)) = (MeasureTheory.volume.restrict (φ '' s)).withDensity f

Change of variables for a weighted Lebesgue measure on the real line. If φ is injective and differentiable on a measurable set s, then weighting Lebesgue measure on s by |φ' t| * f (φ t) and pushing forward along φ gives Lebesgue measure on the image φ '' s weighted by f.

This is the measure-level form of Mathlib's MeasureTheory.lintegral_image_eq_lintegral_abs_deriv_mul, and it carries a weight where MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar has none: that theorem is the case f = 1. Unlike MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul, it does not ask φ to be injective off s, which is what a substitution on a half-line needs. The weight f is arbitrary; no measurability of it is required.

theorem TauCeti.MeasureTheory.map_sq_withDensity_restrict_Ioi (f : ℝ → ENNReal) : MeasureTheory.Measure.map (fun (t : ℝ) => t ^ 2) ((MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (2 * t) * f (t ^ 2)) = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity f

The substitution x = t ^ 2 on the positive half-line. Weighting Lebesgue measure on Ioi 0 by 2 * t * f (t ^ 2) and pushing forward along squaring gives Lebesgue measure on Ioi 0 weighted by f.