Source indexedtheorem · leanprover/lean4:v4.33.0-rc1

MeasureTheory.Measure.map_of_pi

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:907 to 921

Source documentation

Move to Mathlib?

Exact Lean statement

@[simp]
theorem MeasureTheory.Measure.map_of_pi {ι : Type*} [Fintype ι]
    {α : ι → Type*} [∀ i, MeasurableSpace (α i)]
    {β : ι → Type*} [∀ i, MeasurableSpace (β i)]
    (μ : ∀ i, Measure (α i)) [∀ i, IsProbabilityMeasure (μ i)]
    {f : ∀ i, α i → β i} (hf : ∀ i, Measurable (f i)) :
  map (fun x i => f i (x i)) (.pi μ) =
    Measure.pi (fun i => map (f i) (μ i))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp]theorem MeasureTheory.Measure.map_of_pi {ι : Type*} [Fintype ι]    {α : ι → Type*} [∀ i, MeasurableSpace (α i)]    {β : ι → Type*} [∀ i, MeasurableSpace (β i)]    (μ : ∀ i, Measure (α i)) [∀ i, IsProbabilityMeasure (μ i)]    {f : ∀ i, α i → β i} (hf : ∀ i, Measurable (f i)) :  map (fun x i => f i (x i)) (.pi μ) =    Measure.pi (fun i => map (f i) (μ i)) := by    symm; apply pi_eq; intro E hE    rw [map_apply (by fun_prop) (.univ_pi hE)]    have : (fun x i ↦ f i (x i)) ⁻¹' Set.univ.pi E = Set.univ.pi (fun i ↦ (f i)⁻¹' (E i)) := by      aesop    simp only [this, pi_pi_set, Set.mem_univ, Finset.filter_true]    congr! with i _    rw [map_apply (by fun_prop) (hE i)]