English
For identically distributed f and g, the measures of preimages under measurable sets agree.
Русский
Для идентично распределенных f и g меры множества прообразов по измеримым множествам совпадают.
LaTeX
$$$\forall s, MeasurableSet s, μ(f^{-1}(s)) = ν(g^{-1}(s))$$$
Lean4
theorem integral_eq [NormedAddCommGroup γ] [NormedSpace ℝ γ] [BorelSpace γ] (h : IdentDistrib f g μ ν) :
∫ x, f x ∂μ = ∫ x, g x ∂ν := by
by_cases hf : AEStronglyMeasurable f μ
· have A : AEStronglyMeasurable id (Measure.map f μ) :=
by
rw [aestronglyMeasurable_iff_aemeasurable_separable]
rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
refine ⟨aemeasurable_id, ⟨closure t, t_sep.closure, ?_⟩⟩
rw [ae_map_iff h.aemeasurable_fst]
· filter_upwards [ht] with x hx using subset_closure hx
· exact isClosed_closure.measurableSet
change ∫ x, id (f x) ∂μ = ∫ x, id (g x) ∂ν
rw [← integral_map h.aemeasurable_fst A]
rw [h.map_eq] at A
rw [← integral_map h.aemeasurable_snd A, h.map_eq]
· rw [integral_non_aestronglyMeasurable hf]
rw [h.aestronglyMeasurable_iff] at hf
rw [integral_non_aestronglyMeasurable hf]
