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)⁻¹.

Evaluation lemmas for conditionals

Bounds and real-valued forms of cond at an event. [UPSTREAM] candidates alongside the density characterization above.

theorem ProbabilityTheory.cond_apply_le_one {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {s : Set Ω} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (e : Set Ω) : μ[e | s] ≤ 1

Values of a conditional of a finite measure never exceed 1.

theorem ProbabilityTheory.cond_apply_ne_top {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {s : Set Ω} [MeasureTheory.IsFiniteMeasure μ] (hs : MeasurableSet s) (e : Set Ω) : μ[e | s] ≠ ⊤

Conditional values are finite for finite measures.

theorem ProbabilityTheory.cond_eq_one_of_subset {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {s : Set Ω} [MeasureTheory.IsFiniteMeasure μ] {e : Set Ω} (hs : MeasurableSet s) (hsub : s ⊆ e) (hne : μ s ≠ 0) : μ[e | s] = 1

Conditioning gives probability 1 to any superset of the conditioning event.

theorem ProbabilityTheory.cond_real_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {s : Set Ω} (hs : MeasurableSet s) (e : Set Ω) : μ[e | s].toReal = (μ (s ∩ e)).toReal / (μ s).toReal

The conditional as a ratio of real-valued masses.

theorem ProbabilityTheory.real_total {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {h : Set Ω} (hm : MeasurableSet h) (e : Set Ω) : (μ (h ∩ e)).toReal + (μ (hᶜ ∩ e)).toReal = (μ e).toReal

Total probability in real-valued form: a measurable conditioning event splits any event's mass.

theorem ProbabilityTheory.measure_apply_fintype {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [Fintype Ω] [MeasurableSingletonClass Ω] (e : Set Ω) [DecidablePred fun (x : Ω) => x ∈ e] : μ e = ∑ w : Ω with w ∈ e, μ {w}

In a finite discrete space, an event's mass is the sum of its atoms' masses (the register of Mathlib.Probability.Decision.Risk.Countable).

theorem ProbabilityTheory.count_apply_fintype {Ω : Type u_1} [MeasurableSpace Ω] [Fintype Ω] [MeasurableSingletonClass Ω] (e : Set Ω) [DecidablePred fun (x : Ω) => x ∈ e] : MeasureTheory.Measure.count e = ↑{x : Ω | x ∈ e}.card

The counting measure of an event in a finite discrete space is the number of its atoms. Loop-safe as a simp rewrite (the right-hand side contains no measure application).