[Merged by Bors] - feat: measurability of uniqueElim and piFinsetUnion

Mathlib/Logic/Unique.lean

@@ -264,6 +264,10 @@ def uniqueElim [Unique ι] (x : α (default : ι)) (i : ι) : α i := by
 theorem uniqueElim_default {_ : Unique ι} (x : α (default : ι)) : uniqueElim x (default : ι) = x :=
   rfl
 
+@[simp]
+theorem uniqueElim_const {_ : Unique ι} (x : β) (i : ι) : uniqueElim (α := fun _ ↦ β) x i = x :=
+  rfl
+
 end Pi
 
 -- TODO: Mario turned this off as a simp lemma in Std, wanting to profile it.

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -764,8 +764,8 @@ theorem volume_measurePreserving_piCongrLeft (α : ι → Type*) (f : ι' ≃ ι
     MeasurePreserving (MeasurableEquiv.piCongrLeft α f) volume volume :=
   measurePreserving_piCongrLeft (fun _ ↦ volume) f
 
-theorem measurePreserving_sumPiEquivProdPi_symm {π : ι ⊕ ι' → Type*} [∀ i, MeasurableSpace (π i)]
-    (μ : ∀ i, Measure (π i)) [∀ i, SigmaFinite (μ i)] :
+theorem measurePreserving_sumPiEquivProdPi_symm {π : ι ⊕ ι' → Type*}
+    {m : ∀ i, MeasurableSpace (π i)} (μ : ∀ i, Measure (π i)) [∀ i, SigmaFinite (μ i)] :
     MeasurePreserving (MeasurableEquiv.sumPiEquivProdPi π).symm
       ((Measure.pi fun i => μ (.inl i)).prod (Measure.pi fun i => μ (.inr i))) (Measure.pi μ) where
   measurable := (MeasurableEquiv.sumPiEquivProdPi π).symm.measurable
@@ -780,7 +780,7 @@ theorem volume_measurePreserving_sumPiEquivProdPi_symm (π : ι ⊕ ι' → Type
     MeasurePreserving (MeasurableEquiv.sumPiEquivProdPi π).symm volume volume :=
   measurePreserving_sumPiEquivProdPi_symm (fun _ ↦ volume)
 
-theorem measurePreserving_sumPiEquivProdPi {π : ι ⊕ ι' → Type*} [∀ i, MeasurableSpace (π i)]
+theorem measurePreserving_sumPiEquivProdPi {π : ι ⊕ ι' → Type*} {_m : ∀ i, MeasurableSpace (π i)}
     (μ : ∀ i, Measure (π i)) [∀ i, SigmaFinite (μ i)] :
     MeasurePreserving (MeasurableEquiv.sumPiEquivProdPi π)
       (Measure.pi μ) ((Measure.pi fun i => μ (.inl i)).prod (Measure.pi fun i => μ (.inr i))) :=
@@ -810,16 +810,27 @@ theorem volume_preserving_piFinSuccAboveEquiv {n : ℕ} (α : Fin (n + 1) → Ty
   measurePreserving_piFinSuccAboveEquiv (fun _ => volume) i
 #align measure_theory.volume_preserving_pi_fin_succ_above_equiv MeasureTheory.volume_preserving_piFinSuccAboveEquiv
 
-theorem measurePreserving_funUnique {β : Type u} {m : MeasurableSpace β} (μ : Measure β)
+theorem measurePreserving_piUnique {π : ι → Type*} [Unique ι] {m : ∀ i, MeasurableSpace (π i)}
+    (μ : ∀ i, Measure (π i)) :
+    MeasurePreserving (MeasurableEquiv.piUnique π) (Measure.pi μ) (μ default) where
+  measurable := (MeasurableEquiv.piUnique π).measurable
+  map_eq := by
+    set e := MeasurableEquiv.piUnique π
+    have : (piPremeasure fun i => (μ i).toOuterMeasure) = Measure.map e.symm (μ default) := by
+      ext1 s
+      rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply]
+      congr 1; exact e.toEquiv.image_eq_preimage s
+    simp_rw [Measure.pi, OuterMeasure.pi, this, boundedBy_eq_self, toOuterMeasure_toMeasure,
+      MeasurableEquiv.map_map_symm]
+
+theorem volume_preserving_piUnique (π : ι → Type*) [Unique ι] [∀ i, MeasureSpace (π i)] :
+    MeasurePreserving (MeasurableEquiv.piUnique π) volume volume :=
+  measurePreserving_piUnique _
+
+theorem measurePreserving_funUnique {β : Type u} {_m : MeasurableSpace β} (μ : Measure β)
     (α : Type v) [Unique α] :
-    MeasurePreserving (MeasurableEquiv.funUnique α β) (Measure.pi fun _ : α => μ) μ := by
-  set e := MeasurableEquiv.funUnique α β
-  have : (piPremeasure fun _ : α => μ.toOuterMeasure) = Measure.map e.symm μ := by
-    ext1 s
-    rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply]
-    congr 1; exact e.toEquiv.image_eq_preimage s
-  simp only [Measure.pi, OuterMeasure.pi, this, boundedBy_measure, toOuterMeasure_toMeasure]
-  exact (e.symm.measurable.measurePreserving _).symm e.symm
+    MeasurePreserving (MeasurableEquiv.funUnique α β) (Measure.pi fun _ : α => μ) μ :=
+  measurePreserving_piUnique _
 #align measure_theory.measure_preserving_fun_unique MeasureTheory.measurePreserving_funUnique
 
 theorem volume_preserving_funUnique (α : Type u) (β : Type v) [Unique α] [MeasureSpace β] :
@@ -877,6 +888,20 @@ theorem volume_preserving_pi_empty {ι : Type u} (α : ι → Type v) [IsEmpty 
   measurePreserving_pi_empty fun _ => volume
 #align measure_theory.volume_preserving_pi_empty MeasureTheory.volume_preserving_pi_empty
 
+theorem measurePreserving_piFinsetUnion [DecidableEq ι] {s t : Finset ι} (h : Disjoint s t)
+    (μ : ∀ i, Measure (α i)) [∀ i, SigmaFinite (μ i)] :
+    MeasurePreserving (MeasurableEquiv.piFinsetUnion α h)
+      ((Measure.pi fun i : s ↦ μ i).prod (Measure.pi fun i : t ↦ μ i))
+      (Measure.pi fun i : ↥(s ∪ t) ↦ μ i) :=
+  let e := Equiv.Finset.union s t h
+  measurePreserving_piCongrLeft (fun i : ↥(s ∪ t) ↦ μ i) e |>.comp <|
+    measurePreserving_sumPiEquivProdPi_symm fun b ↦ μ (e b)
+
+theorem volume_preserving_piFinsetUnion (α : ι → Type*) [DecidableEq ι] {s t : Finset ι}
+    (h : Disjoint s t) [∀ i, MeasureSpace (α i)] [∀ i, SigmaFinite (volume : Measure (α i))] :
+    MeasurePreserving (MeasurableEquiv.piFinsetUnion α h) volume volume :=
+  measurePreserving_piFinsetUnion h (fun _ ↦ volume)
+
 end MeasurePreserving
 
 end MeasureTheory

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.IndicatorFunction
+import Mathlib.Data.Finset.Update
 import Mathlib.Data.Prod.TProd
 import Mathlib.GroupTheory.Coset
 import Mathlib.Logic.Equiv.Fin
@@ -921,6 +922,16 @@ theorem measurable_update'  {a : δ} [DecidableEq δ] :
     exact measurable_snd
   · exact measurable_pi_iff.1 measurable_fst _
 
+theorem measurable_uniqueElim [Unique δ] [∀ i, MeasurableSpace (π i)] :
+    Measurable (uniqueElim : π (default : δ) → ∀ i, π i) := by
+  simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]; exact measurable_id
+
+theorem measurable_updateFinset [DecidableEq δ] {s : Finset δ} {x : ∀ i, π i} :
+    Measurable (updateFinset x s) := by
+  simp_rw [updateFinset, measurable_pi_iff]
+  intro i
+  by_cases h : i ∈ s <;> simp [h, measurable_pi_apply]
+
 /-- The function `update f a : π a → Π a, π a` is always measurable.
   This doesn't require `f` to be measurable.
   This should not be confused with the statement that `update f a x` is measurable. -/
@@ -1630,12 +1641,23 @@ def piMeasurableEquivTProd [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h :
   measurable_invFun := measurable_tProd_elim' h
 #align measurable_equiv.pi_measurable_equiv_tprod MeasurableEquiv.piMeasurableEquivTProd
 
+variable (π) in
+/-- The measurable equivalence `(∀ i, π i) ≃ᵐ π ⋆` when the domain of `π` only contains `⋆` -/
+@[simps (config := .asFn)]
+def piUnique [Unique δ'] : (∀ i, π i) ≃ᵐ π default where
+  toFun := fun f => f default
+  invFun := uniqueElim
+  left_inv := fun f => funext fun i => by
+    cases Unique.eq_default i
+    rfl
+  right_inv := fun x => rfl
+  measurable_toFun := measurable_pi_apply _
+  measurable_invFun := measurable_uniqueElim
+
 /-- If `α` has a unique term, then the type of function `α → β` is measurably equivalent to `β`. -/
 @[simps! (config := { fullyApplied := false })]
-def funUnique (α β : Type*) [Unique α] [MeasurableSpace β] : (α → β) ≃ᵐ β where
-  toEquiv := Equiv.funUnique α β
-  measurable_toFun := measurable_pi_apply _
-  measurable_invFun := measurable_pi_iff.2 fun _ => measurable_id
+def funUnique (α β : Type*) [Unique α] [MeasurableSpace β] : (α → β) ≃ᵐ β :=
+  MeasurableEquiv.piUnique _
 #align measurable_equiv.fun_unique MeasurableEquiv.funUnique
 
 /-- The space `Π i : Fin 2, α i` is measurably equivalent to `α 0 × α 1`. -/
@@ -1695,6 +1717,14 @@ theorem coe_sumPiEquivProdPi (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace
 theorem coe_sumPiEquivProdPi_symm (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace (α i)] :
     ⇑(MeasurableEquiv.sumPiEquivProdPi α).symm = (Equiv.sumPiEquivProdPi α).symm := by rfl
 
+/-- The measurable equivalence `(∀ i : s, π i) × (∀ i : t, π i) ≃ᵐ (∀ i : s ∪ t, π i)`
+  for disjoint finsets `s` and `t`. `Equiv.piFinsetUnion` as a measurable equivalence. -/
+def piFinsetUnion [DecidableEq δ'] {s t : Finset δ'} (h : Disjoint s t) :
+    ((∀ i : s, π i) × ∀ i : t, π i) ≃ᵐ ∀ i : (s ∪ t : Finset δ'), π i :=
+  let e := Finset.union s t h
+  MeasurableEquiv.sumPiEquivProdPi (fun b ↦ π (e b)) |>.symm.trans <|
+    .piCongrLeft (fun i : ↥(s ∪ t) ↦ π i) e
+
 /-- If `s` is a measurable set in a measurable space, that space is equivalent
 to the sum of `s` and `sᶜ`.-/
 def sumCompl {s : Set α} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) :