feat(measure/pi): prove extensionality for measure.pi (#6304)

* If two measures in a finitary product are equal on cubes with measurable sides (or with sides in a set generating the corresponding sigma-algebra), then the measures are equal.
* Add `sigma_finite` instance for `measure.pi`
* Some basic lemmas about sets (more specifically `Union` and `set.pi`)
* rename `measurable_set.pi_univ` -> `measurable_set.univ_pi` (`pi univ t` is called `univ_pi` consistently in `set/basic`, but it's not always consistent elsewhere)
* rename `[bs]?Union_prod` -> `[bs]?Union_prod_const`



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/data/equiv/encodable/basic.lean

@@ -31,6 +31,10 @@ open encodable
 theorem encode_injective [encodable α] : function.injective (@encode α _)
 | x y e := option.some.inj $ by rw [← encodek, e, encodek]
 
+lemma surjective_decode_iget (α : Type*) [encodable α] [inhabited α] :
+  surjective (λ n, (encodable.decode α n).iget) :=
+λ x, ⟨encodable.encode x, by simp_rw [encodable.encodek]⟩
+
 /- This is not set as an instance because this is usually not the best way
   to infer decidability. -/
 def decidable_eq_of_encodable (α) [encodable α] : decidable_eq α

src/data/nat/pairing.lean

@@ -7,7 +7,7 @@ Elegant pairing function.
 -/
 import data.nat.sqrt
 import data.set.lattice
-open prod decidable
+open prod decidable function
 
 namespace nat
 
@@ -49,6 +49,9 @@ begin
     simp [unpair, ae, not_lt_zero, add_assoc] }
 end
 
+lemma surjective_unpair : surjective unpair :=
+λ ⟨m, n⟩, ⟨mkpair m n, unpair_mkpair m n⟩
+
 theorem unpair_lt {n : ℕ} (n1 : 1 ≤ n) : (unpair n).1 < n :=
 let s := sqrt n in begin
   simp [unpair], change sqrt n with s,
@@ -103,15 +106,12 @@ begin
 end
 
 end nat
+open nat
 
 namespace set
 
 lemma Union_unpair_prod {α β} {s : ℕ → set α} {t : ℕ → set β} :
   (⋃ n : ℕ, (s n.unpair.fst).prod (t n.unpair.snd)) = (⋃ n, s n).prod (⋃ n, t n) :=
-begin
-  ext, simp only [mem_Union, mem_prod], split,
-  { rintro ⟨n, h1n, h2n⟩, exact ⟨⟨_, h1n⟩, _, h2n⟩ },
-  { rintro ⟨⟨n, hn⟩, m, hm⟩, use n.mkpair m, simp [hn, hm] }
-end
+by { rw [← Union_prod], convert surjective_unpair.Union_comp _, refl }
 
 end set

src/data/set/basic.lean

@@ -2198,6 +2198,14 @@ end
   (λ f : Π i, α i, f i) '' pi univ t = t i :=
 eval_image_pi (mem_univ i) ht
 
+lemma eval_preimage {ι} {α : ι → Type*} {i : ι} {s : set (α i)} :
+  eval i ⁻¹' s = pi univ (update (λ i, univ) i s) :=
+by { ext x, simp [@forall_update_iff _ (λ i, set (α i)) _ _ _ _ (λ i' y, x i' ∈ y)] }
+
+lemma eval_preimage' {ι} {α : ι → Type*} {i : ι} {s : set (α i)} :
+  eval i ⁻¹' s = pi {i} (update (λ i, univ) i s) :=
+by { ext, simp }
+
 lemma update_preimage_pi {i : ι} {f : Π i, α i} (hi : i ∈ s)
   (hf : ∀ j ∈ s, j ≠ i → f j ∈ t j) : (update f i) ⁻¹' s.pi t = t i :=
 begin
@@ -2215,6 +2223,10 @@ update_preimage_pi (mem_univ i) (λ j _, hf j)
 lemma subset_pi_eval_image (s : set ι) (u : set (Π i, α i)) : u ⊆ pi s (λ i, eval i '' u) :=
 λ f hf i hi, ⟨f, hf, rfl⟩
 
+lemma univ_pi_ite (s : set ι) (t : Π i, set (α i)) :
+  pi univ (λ i, if i ∈ s then t i else univ) = s.pi t :=
+by { ext, simp_rw [mem_univ_pi], apply forall_congr, intro i, split_ifs; simp [h] }
+
 end pi
 
 /-! ### Lemmas about `inclusion`, the injection of subtypes induced by `⊆` -/

src/data/set/lattice.lean

@@ -12,8 +12,8 @@ import order.directed
 
 open function tactic set auto
 
-universes u v w x y
-variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {ι' : Sort y}
+universes u v
+variables {α β γ : Type*} {ι ι' ι₂ : Sort*}
 
 namespace set
 
@@ -132,6 +132,14 @@ set.subset_Inter $ λ j, let ⟨i, hi⟩ := h j in Inter_subset_of_subset i hi
 lemma Inter_set_of (P : ι → α → Prop) : (⋂ i, {x : α | P i x }) = {x : α | ∀ i, P i x} :=
 by { ext, simp }
 
+lemma Union_congr {f : ι → set α} {g : ι₂ → set α} (h : ι → ι₂)
+  (h1 : surjective h) (h2 : ∀ x, g (h x) = f x) : (⋃ x, f x) = ⋃ y, g y :=
+supr_congr h h1 h2
+
+lemma Inter_congr {f : ι → set α} {g : ι₂ → set α} (h : ι → ι₂)
+  (h1 : surjective h) (h2 : ∀ x, g (h x) = f x) : (⋂ x, f x) = ⋂ y, g y :=
+infi_congr h h1 h2
+
 theorem Union_const [nonempty ι] (s : set β) : (⋃ i:ι, s) = s := supr_const
 
 theorem Inter_const [nonempty ι] (s : set β) : (⋂ i:ι, s) = s := infi_const
@@ -201,7 +209,7 @@ theorem diff_Inter (s : set β) (t : ι → set β) :
   s \ (⋂ i, t i) = ⋃ i, s \ t i :=
 by rw [diff_eq, compl_Inter, inter_Union]; refl
 
-lemma directed_on_Union {r} {ι : Sort v} {f : ι → set α} (hd : directed (⊆) f)
+lemma directed_on_Union {r} {f : ι → set α} (hd : directed (⊆) f)
   (h : ∀x, directed_on r (f x)) : directed_on r (⋃x, f x) :=
 by simp only [directed_on, exists_prop, mem_Union, exists_imp_distrib]; exact
 assume a₁ b₁ fb₁ a₂ b₂ fb₂,
@@ -550,14 +558,14 @@ sUnion_subset $ assume t' ht', subset_sUnion_of_mem $ h ht'
 lemma Union_subset_Union {s t : ι → set α} (h : ∀i, s i ⊆ t i) : (⋃i, s i) ⊆ (⋃i, t i) :=
 @supr_le_supr (set α) ι _ s t h
 
-lemma Union_subset_Union2 {ι₂ : Sort*} {s : ι → set α} {t : ι₂ → set α} (h : ∀i, ∃j, s i ⊆ t j) :
+lemma Union_subset_Union2 {s : ι → set α} {t : ι₂ → set α} (h : ∀i, ∃j, s i ⊆ t j) :
   (⋃i, s i) ⊆ (⋃i, t i) :=
 @supr_le_supr2 (set α) ι ι₂ _ s t h
 
-lemma Union_subset_Union_const {ι₂ : Sort x} {s : set α} (h : ι → ι₂) : (⋃ i:ι, s) ⊆ (⋃ j:ι₂, s) :=
+lemma Union_subset_Union_const {s : set α} (h : ι → ι₂) : (⋃ i:ι, s) ⊆ (⋃ j:ι₂, s) :=
 @supr_le_supr_const (set α) ι ι₂ _ s h
 
-@[simp] lemma Union_of_singleton (α : Type u) : (⋃(x : α), {x}) = @set.univ α :=
+@[simp] lemma Union_of_singleton (α : Type*) : (⋃(x : α), {x}) = @set.univ α :=
 ext $ λ x, ⟨λ h, ⟨⟩, λ h, ⟨{x}, ⟨⟨x, rfl⟩, mem_singleton x⟩⟩⟩
 
 @[simp] lemma Union_of_singleton_coe (s : set α) :
@@ -925,7 +933,7 @@ section preimage
 
 theorem monotone_preimage {f : α → β} : monotone (preimage f) := assume a b h, preimage_mono h
 
-@[simp] theorem preimage_Union {ι : Sort w} {f : α → β} {s : ι → set β} :
+@[simp] theorem preimage_Union {ι : Sort*} {f : α → β} {s : ι → set β} :
   preimage f (⋃i, s i) = (⋃i, preimage f (s i)) :=
 set.ext $ by simp [preimage]
 
@@ -971,16 +979,20 @@ by simp_rw [prod_Union]
 lemma prod_sUnion {s : set α} {C : set (set β)} : s.prod (⋃₀ C) = ⋃₀ ((λ t, s.prod t) '' C) :=
 by { simp only [sUnion_eq_bUnion, prod_bUnion, bUnion_image] }
 
-lemma Union_prod {ι} {s : ι → set α} {t : set β} : (⋃ i, s i).prod t = ⋃ i, (s i).prod t :=
+lemma Union_prod_const {ι} {s : ι → set α} {t : set β} : (⋃ i, s i).prod t = ⋃ i, (s i).prod t :=
 by { ext, simp }
 
-lemma bUnion_prod {ι} {u : set ι} {s : ι → set α} {t : set β} :
+lemma bUnion_prod_const {ι} {u : set ι} {s : ι → set α} {t : set β} :
   (⋃ i ∈ u, s i).prod t = ⋃ i ∈ u, (s i).prod t :=
-by simp_rw [Union_prod]
+by simp_rw [Union_prod_const]
 
-lemma sUnion_prod {C : set (set α)} {t : set β} :
+lemma sUnion_prod_const {C : set (set α)} {t : set β} :
   (⋃₀ C).prod t = ⋃₀ ((λ s : set α, s.prod t) '' C) :=
-by { simp only [sUnion_eq_bUnion, bUnion_prod, bUnion_image] }
+by { simp only [sUnion_eq_bUnion, bUnion_prod_const, bUnion_image] }
+
+lemma Union_prod {ι α β} (s : ι → set α) (t : ι → set β) :
+  (⋃ (x : ι × ι), (s x.1).prod (t x.2)) = (⋃ (i : ι), s i).prod (⋃ (i : ι), t i) :=
+by { ext, simp }
 
 lemma Union_prod_of_monotone [semilattice_sup α] {s : α → set β} {t : α → set γ}
   (hs : monotone s) (ht : monotone t) : (⋃ x, (s x).prod (t x)) = (⋃ x, (s x)).prod (⋃ x, (t x)) :=
@@ -1092,6 +1104,9 @@ lemma pi_def (i : set α) (s : Πa, set (π a)) :
   pi i s = (⋂ a ∈ i, eval a ⁻¹' s a) :=
 by { ext, simp }
 
+lemma univ_pi_eq_Inter (t : Π i, set (π i)) : pi univ t = ⋂ i, eval i ⁻¹' t i :=
+by simp only [pi_def, Inter_pos, mem_univ]
+
 lemma pi_diff_pi_subset (i : set α) (s t : Πa, set (π a)) :
   pi i s \ pi i t ⊆ ⋃ a ∈ i, (eval a ⁻¹' (s a \ t a)) :=
 begin
@@ -1101,10 +1116,28 @@ begin
   exact hx.2 _ ha (hx.1 _ ha)
 end
 
+lemma Union_univ_pi (t : Π i, ι → set (π i)) :
+  (⋃ (x : α → ι), pi univ (λ i, t i (x i))) = pi univ (λ i, ⋃ (j : ι), t i j) :=
+by { ext, simp [classical.skolem] }
+
 end pi
 
 end set
 
+namespace function
+namespace surjective
+
+lemma Union_comp {f : ι → ι₂} (hf : surjective f) (g : ι₂ → set α) :
+  (⋃ x, g (f x)) = ⋃ y, g y :=
+hf.supr_comp g
+
+lemma Inter_comp {f : ι → ι₂} (hf : surjective f) (g : ι₂ → set α) :
+  (⋂ x, g (f x)) = ⋂ y, g y :=
+hf.infi_comp g
+
+end surjective
+end function
+
 /-! ### Disjoint sets -/
 
 section disjoint

src/measure_theory/measurable_space.lean

@@ -783,7 +783,7 @@ lemma measurable_set.pi {s : set δ} {t : Π i : δ, set (π i)} (hs : countable
   measurable_set (s.pi t) :=
 by { rw [pi_def], exact measurable_set.bInter hs (λ i hi, measurable_pi_apply _ (ht i hi)) }
 
-lemma measurable_set.pi_univ [encodable δ] {t : Π i : δ, set (π i)}
+lemma measurable_set.univ_pi [encodable δ] {t : Π i : δ, set (π i)}
   (ht : ∀ i, measurable_set (t i)) : measurable_set (pi univ t) :=
 measurable_set.pi (countable_encodable _) (λ i _, ht i)
 
@@ -810,6 +810,10 @@ lemma measurable_set.pi_fintype [fintype δ] {s : set δ} {t : Π i, set (π i)}
   (ht : ∀ i ∈ s, measurable_set (t i)) : measurable_set (pi s t) :=
 measurable_set.pi (countable_encodable _) ht
 
+lemma measurable_set.univ_pi_fintype [fintype δ] {t : Π i, set (π i)}
+  (ht : ∀ i, measurable_set (t i)) : measurable_set (pi univ t) :=
+measurable_set.pi_fintype (λ i _, ht i)
+
 end fintype
 end pi