The density of a set upstairs, seen on the base of a measure-preserving map

Let f : Ω' → Ω push a measure ν forward to a σ-finite measure μ, and let s ⊆ Ω' be a set upstairs. The part of ν carried by s pushes forward to a measure ≤ μ, so it has a Radon–Nikodym density with respect to μ taking values in [0, 1]. That density is mapRestrictDensity f ν μ s, and it is characterised by

∫ a, mapRestrictDensity f ν μ s a * g a ∂μ = ∫ x in s, g (f x) ∂ν

for every μ-a.e. strongly measurable g : Ω → ℝ (integral_mapRestrictDensity_mul). This Radon–Nikodym identity holds for arbitrary s. When s is measurable, the density has the additional probabilistic reading of the conditional probability of s given f: composing it with f gives a version of ν[s.indicator 1 | comap f]. Nothing here needs that reading, so the conditional-expectation machinery is not used; the elementary Radon–Nikodym route is enough.

Truncation is deliberate. The definition applies min 1 to the Radon–Nikodym derivative so that the [0, 1] bounds hold everywhere, not merely almost everywhere. Consumers pair this function against a kernel and need a strict pointwise bound to feed an extremal argument; the truncation is invisible to every integral statement below, because it changes the derivative only on a μ-null set (mapRestrictDensity_ae_eq_rnDeriv). The private product-carrier regression below confirms that the density can be a genuinely fractional multiple of an indicator, rather than always an indicator itself.

Main definitions

• TauCeti.MeasureTheory.mapRestrictDensity — the [0, 1]-valued density on the base of the part of ν carried by a set upstairs.

Main results

• TauCeti.MeasureTheory.integral_mapRestrictDensity_mul — the characterising identity: integrating against the density downstairs computes the integral over the set upstairs. No measurability of the set is needed.
• TauCeti.MeasureTheory.mapRestrictDensity_ae_eq_rnDeriv — the truncation is a.e. invisible.
• TauCeti.MeasureTheory.mapRestrictDensity_mem_Icc — the density lies in [0, 1] everywhere.
• TauCeti.MeasureTheory.integral_mapRestrictDensity — the density integrates to the measure of the set, the case g = 1.
• TauCeti.MeasureTheory.mapRestrictDensity_congr_set — the density depends on the set upstairs only through its ν-a.e. class; this equality is exact, not almost everywhere.
• TauCeti.MeasureTheory.mapRestrictDensity_preimage and TauCeti.MeasureTheory.mapRestrictDensity_univ — on a preimage the density collapses μ-almost everywhere to an indicator, so the construction extends the trivial case.
• TauCeti.MeasureTheory.isFiniteMeasure_of_measurePreserving — an auxiliary fact transferring finiteness from the source to the target of a measure-preserving map.

References

• Mathlib's MeasureTheory.toReal_rnDeriv_map identifies the Radon–Nikodym derivative of a pushforward with a conditional expectation; it is the abstract form of the reading above and is not needed for any statement here.

noncomputable def TauCeti.MeasureTheory.mapRestrictDensity {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (f : Ω' → Ω) (ν : MeasureTheory.Measure Ω') (μ : MeasureTheory.Measure Ω) (s : Set Ω') (a : Ω) : ℝ

The density on the base of the part of ν carried by s: the Radon–Nikodym derivative of (ν.restrict s).map f with respect to μ, truncated to [0, 1].

When f pushes ν forward to μ the truncation is a.e. invisible (mapRestrictDensity_ae_eq_rnDeriv) and the function is characterised by integral_mapRestrictDensity_mul. The measures are explicit arguments because neither is determined by the others: μ is not forced to be ν.map f by the type.

Equations

• TauCeti.MeasureTheory.mapRestrictDensity f ν μ s a = min 1 ((MeasureTheory.Measure.map f (ν.restrict s)).rnDeriv μ a).toReal

theorem TauCeti.MeasureTheory.mapRestrictDensity_def {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (f : Ω' → Ω) (ν : MeasureTheory.Measure Ω') (μ : MeasureTheory.Measure Ω) (s : Set Ω') (a : Ω) : mapRestrictDensity f ν μ s a = min 1 ((MeasureTheory.Measure.map f (ν.restrict s)).rnDeriv μ a).toReal

The defining formula of mapRestrictDensity.

theorem TauCeti.MeasureTheory.measurable_mapRestrictDensity {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (f : Ω' → Ω) (ν : MeasureTheory.Measure Ω') (μ : MeasureTheory.Measure Ω) (s : Set Ω') : Measurable (mapRestrictDensity f ν μ s)

The density is measurable, being a truncated Radon–Nikodym derivative.

theorem TauCeti.MeasureTheory.mapRestrictDensity_mem_Icc {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (f : Ω' → Ω) (ν : MeasureTheory.Measure Ω') (μ : MeasureTheory.Measure Ω) (s : Set Ω') (a : Ω) : mapRestrictDensity f ν μ s a ∈ Set.Icc 0 1

The density is [0, 1]-valued everywhere. The upper bound is what the truncation in the definition buys; both bounds are packaged together, in the form the extremal arguments of the cut-norm theory consume, and the two halves are .1 and .2.

theorem TauCeti.MeasureTheory.mapRestrictDensity_congr_set {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {ν : MeasureTheory.Measure Ω'} (f : Ω' → Ω) (μ : MeasureTheory.Measure Ω) {s t : Set Ω'} (h : s =ᵐ[ν] t) : mapRestrictDensity f ν μ s = mapRestrictDensity f ν μ t

The density depends on the set upstairs only through its ν-a.e. class. Replacing s by an a.e. equal set does not change the function at all, since it does not change ν.restrict s.

theorem TauCeti.MeasureTheory.isFiniteMeasure_of_measurePreserving {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} {f : Ω' → Ω} [MeasureTheory.IsFiniteMeasure ν] (hf : MeasureTheory.MeasurePreserving f ν μ) : MeasureTheory.IsFiniteMeasure μ

A finite source measure makes the target of a measure-preserving map finite.

theorem TauCeti.MeasureTheory.mapRestrictDensity_ae_eq_rnDeriv {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} {f : Ω' → Ω} [MeasureTheory.SigmaFinite μ] (hf : MeasureTheory.MeasurePreserving f ν μ) (s : Set Ω') : mapRestrictDensity f ν μ s =ᵐ[μ] fun (a : Ω) => ((MeasureTheory.Measure.map f (ν.restrict s)).rnDeriv μ a).toReal

The truncation in mapRestrictDensity is a.e. invisible. The underlying Radon–Nikodym derivative is already at most 1 almost everywhere, because the measure it differentiates is below μ.

theorem TauCeti.MeasureTheory.integral_mapRestrictDensity_mul {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} {f : Ω' → Ω} [MeasureTheory.SigmaFinite μ] (hf : MeasureTheory.MeasurePreserving f ν μ) (s : Set Ω') {g : Ω → ℝ} (hg : MeasureTheory.AEStronglyMeasurable g μ) : ∫ (a : Ω), mapRestrictDensity f ν μ s a * g a ∂μ = ∫ (x : Ω') in s, g (f x) ∂ν

The characterising identity of mapRestrictDensity. Integrating a function on the base against the density computes its integral, composed with f, over the set upstairs.

The set is arbitrary: Measure.restrict and every step of the computation are insensitive to its measurability.

theorem TauCeti.MeasureTheory.integral_mapRestrictDensity {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} {f : Ω' → Ω} [MeasureTheory.SigmaFinite μ] (hf : MeasureTheory.MeasurePreserving f ν μ) (s : Set Ω') : ∫ (a : Ω), mapRestrictDensity f ν μ s a ∂μ = ν.real s

The density integrates to the measure of the set it came from: the case g = 1 of integral_mapRestrictDensity_mul.

theorem TauCeti.MeasureTheory.mapRestrictDensity_preimage {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} {f : Ω' → Ω} [MeasureTheory.SigmaFinite μ] (hf : MeasureTheory.MeasurePreserving f ν μ) {t : Set Ω} (ht : MeasurableSet t) : mapRestrictDensity f ν μ (f ⁻¹' t) =ᵐ[μ] t.indicator 1

On a preimage the density is μ-almost everywhere an indicator. Nothing is lost when the set upstairs is already cut out by a set on the base, so mapRestrictDensity extends the trivial case rather than replacing it.

The conclusion is only μ-a.e., as it must be: the Radon–Nikodym derivative is itself defined only up to a μ-null set.

theorem TauCeti.MeasureTheory.mapRestrictDensity_univ {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} {f : Ω' → Ω} [MeasureTheory.SigmaFinite μ] (hf : MeasureTheory.MeasurePreserving f ν μ) : mapRestrictDensity f ν μ Set.univ =ᵐ[μ] 1

The whole carrier upstairs has density 1 μ-almost everywhere.