Conditional measures are densities

cond_eq_withDensity: conditioning on an event is reweighting by the density (μ s)⁻¹ on s and 0 off it — an exact measure equality with no side conditions beyond measurability. The Radon-Nikodym facts (rnDeriv_cond, rnDeriv_cond_ae_const) are its corollaries. [UPSTREAM] candidates. Mathlib has no withDensity or rnDeriv characterization of cond in either direction; its Probability/ConditionalProbability.lean imports only measure typeclasses, so the realistic upstream shape is a new leaf holding this file's three lemmas (importing ConditionalProbability + WithDensity + Decomposition.Lebesgue, the pattern of WithDensityFinite.lean), unless review pulls cond_eq_withDensity alone into ConditionalProbability.lean at the cost of one import.

theorem ProbabilityTheory.cond_eq_withDensity {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s : Set Ω} (hs : MeasurableSet s) : μ[|s] = μ.withDensity (s.indicator fun (x : Ω) => (μ s)⁻¹)

The conditional measure μ[|s] is μ with density (μ s)⁻¹ on s and 0 off it.

theorem ProbabilityTheory.rnDeriv_cond {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s : Set Ω} [MeasureTheory.SigmaFinite μ] (hs : MeasurableSet s) : μ[|s].rnDeriv μ =ᵐ[μ] s.indicator fun (x : Ω) => (μ s)⁻¹

The Radon-Nikodym derivative of the conditional measure μ[|s] with respect to μ is (μ s)⁻¹ on s and 0 off it.

theorem ProbabilityTheory.rnDeriv_cond_ae_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s : Set Ω} [MeasureTheory.SigmaFinite μ] (hs : MeasurableSet s) : μ[|s].rnDeriv μ =ᵐ[μ[|s]] fun (x : Ω) => (μ s)⁻¹

On its own event, the conditional measure's density is the constant (μ s)⁻¹.