feat(measure_theory): ι → α ≃ᵐ α if [unique ι] (#9353)

* define versions of `equiv.fun_unique` for `order_iso` and
  `measurable_equiv`;
* use the latter to relate integrals over (sets in) `ι → α` and `α`,
  where `ι` is a type with an unique element.

src/measure_theory/constructions/pi.lean

@@ -328,6 +328,21 @@ begin
   exact λ i, measurable_set_closed_ball
 end
 
+lemma pi_unique_eq_map {β : Type*} {m : measurable_space β} (μ : measure β) (α : Type*) [unique α] :
+  measure.pi (λ a : α, μ) = map (measurable_equiv.fun_unique α β).symm μ :=
+begin
+  set e := measurable_equiv.fun_unique α β,
+  have : pi_premeasure (λ _ : α, μ.to_outer_measure) = map e.symm μ,
+  { ext1 s,
+    rw [pi_premeasure, fintype.prod_unique, to_outer_measure_apply, e.symm.map_apply],
+    congr' 1, exact e.to_equiv.image_eq_preimage s },
+  simp only [measure.pi, outer_measure.pi, this, bounded_by_measure, to_outer_measure_to_measure],
+end
+
+lemma map_fun_unique {α β : Type*} [unique α] {m : measurable_space β} (μ : measure β) :
+  map (measurable_equiv.fun_unique α β) (measure.pi $ λ _, μ) = μ :=
+(measurable_equiv.fun_unique α β).map_apply_eq_iff_map_symm_apply_eq.2 (pi_unique_eq_map μ _).symm
+
 variable {μ}
 
 /-- `measure.pi μ` has finite spanning sets in rectangles of finite spanning sets. -/
@@ -567,4 +582,52 @@ lemma volume_pi_closed_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (v
   volume (metric.closed_ball x r) = ∏ i, volume (metric.closed_ball (x i) r) :=
 measure.pi_closed_ball _ _ hr
 
+/-!
+### Integral over `ι → α` with `[unique ι]`
+
+In this section we prove some lemmas that relate integrals over `ι → β`, where `ι` is a type with
+unique element (e.g., `unit` or `fin 1`) and integrals over `β`.
+-/
+
+variables {β E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E]
+  [topological_space.second_countable_topology E] [borel_space E] [complete_space E]
+
+lemma integral_fun_unique_pi (ι) [unique ι] {m : measurable_space β} (μ : measure β)
+  (f : (ι → β) → E) :
+  ∫ y, f y ∂(measure.pi (λ _, μ)) = ∫ x, f (λ _, x) ∂μ :=
+by rw [measure.pi_unique_eq_map μ ι, integral_map_equiv]; refl
+
+lemma integral_fun_unique_pi' (ι : Type*) [unique ι] {m : measurable_space β} (μ : measure β)
+  (f : β → E) :
+  ∫ y : ι → β, f (y (default ι)) ∂(measure.pi (λ _, μ)) = ∫ x, f x ∂μ :=
+integral_fun_unique_pi ι μ _
+
+lemma integral_fun_unique (ι : Type*) [unique ι] [measure_space β] (f : (ι → β) → E) :
+  ∫ y, f y = ∫ x, f (λ _, x) :=
+integral_fun_unique_pi ι volume f
+
+lemma integral_fun_unique' (ι : Type*) [unique ι] [measure_space β] (f : β → E) :
+  ∫ y : ι → β, f (y (default ι)) = ∫ x, f x :=
+integral_fun_unique_pi' ι volume f
+
+lemma set_integral_fun_unique_pi (ι : Type*) [unique ι] {m : measurable_space β} (μ : measure β)
+  (f : (ι → β) → E) (s : set (ι → β)) :
+  ∫ y in s, f y ∂(measure.pi (λ _, μ)) = ∫ x in const ι ⁻¹' s, f (λ _, x) ∂μ :=
+by rw [measure.pi_unique_eq_map μ ι, set_integral_map_equiv]; refl
+
+lemma set_integral_fun_unique_pi' (ι : Type*) [unique ι] {m : measurable_space β} (μ : measure β)
+  (f : β → E) (s : set β) :
+  ∫ y : ι → β in function.eval (default ι) ⁻¹' s, f (y (default ι)) ∂(measure.pi (λ _, μ)) =
+    ∫ x in s, f x ∂μ :=
+by erw [set_integral_fun_unique_pi, (equiv.fun_unique ι β).symm_preimage_preimage]
+
+lemma set_integral_fun_unique (ι : Type*) [unique ι] [measure_space β] (f : (ι → β) → E)
+  (s : set (ι → β)) :
+  ∫ y in s, f y = ∫ x in const ι ⁻¹' s, f (λ _, x) :=
+by convert set_integral_fun_unique_pi ι volume f s
+
+lemma set_integral_fun_unique' (ι : Type*) [unique ι] [measure_space β] (f : β → E) (s : set β) :
+  ∫ y : ι → β in @function.eval ι (λ _, β) (default ι) ⁻¹' s, f (y (default ι)) = ∫ x in s, f x :=
+by convert set_integral_fun_unique_pi' ι volume f s
+
 end measure_theory

src/measure_theory/measurable_space.lean

@@ -953,6 +953,13 @@ noncomputable def pi_measurable_equiv_tprod {l : list δ'} (hnd : l.nodup) (h :
   measurable_to_fun := measurable_tprod_mk l,
   measurable_inv_fun := measurable_tprod_elim' h }
 
+/-- If `α` has a unique term, then the type of function `α → β` is measurably equivalent to `β`. -/
+@[simps {fully_applied := ff}] def fun_unique (α β : Type*) [unique α] [measurable_space β] :
+  (α → β) ≃ᵐ β :=
+{ to_equiv := equiv.fun_unique α β,
+  measurable_to_fun := measurable_pi_apply _,
+  measurable_inv_fun := measurable_pi_iff.2 $ λ b, measurable_id }
+
 end measurable_equiv
 
 namespace filter

src/order/rel_iso.lean

@@ -683,6 +683,15 @@ def set.univ : (set.univ : set α) ≃o α :=
 { to_equiv := equiv.set.univ α,
   map_rel_iff' := λ x y, iff.rfl }
 
+/-- Order isomorphism between `α → β` and `β`, where `α` has a unique element. -/
+@[simps to_equiv apply] def fun_unique (α β : Type*) [unique α] [preorder β] :
+  (α → β) ≃o β :=
+{ to_equiv := equiv.fun_unique α β,
+  map_rel_iff' := λ f g, by simp [pi.le_def, unique.forall_iff] }
+
+@[simp] lemma fun_unique_symm_apply {α β : Type*} [unique α] [preorder β] :
+  ((fun_unique α β).symm : β → α → β) = function.const α := rfl
+
 end order_iso
 
 namespace equiv