From 8713c0bd9a4a0ed3ee8769d23ceaa11a70620158 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 9 Mar 2021 16:22:20 +0000 Subject: [PATCH] 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 --- src/data/equiv/encodable/basic.lean | 4 + src/data/nat/pairing.lean | 12 +- src/data/set/basic.lean | 12 ++ src/data/set/lattice.lean | 57 ++++++-- src/measure_theory/measurable_space.lean | 6 +- src/measure_theory/pi.lean | 157 +++++++++++++++++++++-- src/measure_theory/prod.lean | 6 +- 7 files changed, 218 insertions(+), 36 deletions(-) diff --git a/src/data/equiv/encodable/basic.lean b/src/data/equiv/encodable/basic.lean index 55f93cca2b9ea..874cee4c4b32c 100644 --- a/src/data/equiv/encodable/basic.lean +++ b/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 α diff --git a/src/data/nat/pairing.lean b/src/data/nat/pairing.lean index ad2116b53a050..0386401596632 100644 --- a/src/data/nat/pairing.lean +++ b/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 diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean index 7c082454cbec5..1bfd1639c5534 100644 --- a/src/data/set/basic.lean +++ b/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 `⊆` -/ diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean index 7dc7b52d9b189..74590a322a25a 100644 --- a/src/data/set/lattice.lean +++ b/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 diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean index 79ea54d99bf65..26a1becfe4763 100644 --- a/src/measure_theory/measurable_space.lean +++ b/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 diff --git a/src/measure_theory/pi.lean b/src/measure_theory/pi.lean index 90ba72e5ebf67..cf603a02b8cbe 100644 --- a/src/measure_theory/pi.lean +++ b/src/measure_theory/pi.lean @@ -20,7 +20,7 @@ In this file we define and prove properties about finite products of measures We define `measure_theory.outer_measure.pi`, the product of finitely many outer measures, as the maximal outer measure `n` with the property that `n (pi univ s) ≤ ∏ i, m i (s i)`, -where `pi univ s` is the product of the sets `{ s i | i : ι }`. +where `pi univ s` is the product of the sets `{s i | i : ι}`. We then show that this induces a product of measures, called `measure_theory.measure.pi`. For a collection of σ-finite measures `μ` and a collection of measurable sets `s` we show that @@ -44,12 +44,87 @@ finitary product measure -/ noncomputable theory -open function set measure_theory.outer_measure filter +open function set measure_theory.outer_measure filter measurable_space encodable open_locale classical big_operators topological_space ennreal +variables {ι ι' : Type*} {α : ι → Type*} + +/-! We start with some measurability properties -/ + +/-- Boxes formed by π-systems form a π-system. -/ +lemma is_pi_system.pi {C : Π i, set (set (α i))} (hC : ∀ i, is_pi_system (C i)) : + is_pi_system (pi univ '' pi univ C) := +begin + rintro _ _ ⟨s₁, hs₁, rfl⟩ ⟨s₂, hs₂, rfl⟩ hst, + rw [← pi_inter_distrib] at hst ⊢, rw [univ_pi_nonempty_iff] at hst, + exact mem_image_of_mem _ (λ i _, hC i _ _ (hs₁ i (mem_univ i)) (hs₂ i (mem_univ i)) (hst i)) +end + +/-- Boxes form a π-system. -/ +lemma is_pi_system_pi [Π i, measurable_space (α i)] : + is_pi_system (pi univ '' pi univ (λ i, {s : set (α i) | measurable_set s})) := +is_pi_system.pi (λ i, is_pi_system_measurable_set) + +variables [fintype ι] [fintype ι'] + +/-- Boxes of countably spanning sets are countably spanning. -/ +lemma is_countably_spanning.pi {C : Π i, set (set (α i))} + (hC : ∀ i, is_countably_spanning (C i)) : + is_countably_spanning (pi univ '' pi univ C) := +begin + choose s h1s h2s using hC, + haveI := fintype.encodable ι, + let e : ℕ → (ι → ℕ) := λ n, (decode (ι → ℕ) n).iget, + refine ⟨λ n, pi univ (λ i, s i (e n i)), λ n, mem_image_of_mem _ (λ i _, h1s i _), _⟩, + simp_rw [(surjective_decode_iget (ι → ℕ)).Union_comp (λ x, pi univ (λ i, s i (x i))), + Union_univ_pi s, h2s, pi_univ] +end + +/-- The product of generated σ-algebras is the one generated by boxes, if both generating sets + are countably spanning. -/ +lemma generate_from_pi_eq {C : Π i, set (set (α i))} + (hC : ∀ i, is_countably_spanning (C i)) : + @measurable_space.pi _ _ (λ i, generate_from (C i)) = generate_from (pi univ '' pi univ C) := +begin + haveI := fintype.encodable ι, + apply le_antisymm, + { refine supr_le _, intro i, rw [comap_generate_from], + apply generate_from_le, rintro _ ⟨s, hs, rfl⟩, dsimp, + choose t h1t h2t using hC, + simp_rw [eval_preimage, ← h2t], + rw [← @Union_const _ ℕ _ s], + have : (pi univ (update (λ (i' : ι), Union (t i')) i (⋃ (i' : ℕ), s))) = + (pi univ (λ k, ⋃ j : ℕ, @update ι (λ i', set (α i')) _ (λ i', t i' j) i s k)), + { ext, simp_rw [mem_univ_pi], apply forall_congr, intro i', + by_cases (i' = i), { subst h, simp }, { rw [← ne.def] at h, simp [h] }}, + rw [this, ← Union_univ_pi], + apply measurable_set.Union, + intro n, apply measurable_set_generate_from, + apply mem_image_of_mem, intros j _, dsimp only, + by_cases h: j = i, subst h, rwa [update_same], rw [update_noteq h], apply h1t }, + { apply generate_from_le, rintro _ ⟨s, hs, rfl⟩, + rw [univ_pi_eq_Inter], apply measurable_set.Inter, intro i, apply measurable_pi_apply, + exact measurable_set_generate_from (hs i (mem_univ i)) } +end + +/-- If `C` and `D` generate the σ-algebras on `α` resp. `β`, then rectangles formed by `C` and `D` + generate the σ-algebra on `α × β`. -/ +lemma generate_from_eq_pi [h : Π i, measurable_space (α i)] + {C : Π i, set (set (α i))} (hC : ∀ i, generate_from (C i) = h i) + (h2C : ∀ i, is_countably_spanning (C i)) : + generate_from (pi univ '' pi univ C) = measurable_space.pi := +by rw [← funext hC, generate_from_pi_eq h2C] + +/-- The product σ-algebra is generated from boxes, i.e. `s.prod t` for sets `s : set α` and + `t : set β`. -/ +lemma generate_from_pi [Π i, measurable_space (α i)] : + generate_from (pi univ '' pi univ (λ i, { s : set (α i) | measurable_set s})) = + measurable_space.pi := +generate_from_eq_pi (λ i, generate_from_measurable_set) (λ i, is_countably_spanning_measurable_set) + namespace measure_theory -variables {ι : Type*} [fintype ι] {α : ι → Type*} {m : Π i, outer_measure (α i)} +variables {m : Π i, outer_measure (α i)} /-- An upper bound for the measure in a finite product space. It is defined to by taking the image of the set under all projections, and taking the product @@ -68,7 +143,7 @@ begin cases (pi univ s).eq_empty_or_nonempty with h h, { rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩, have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩, - simpa [h, finset.card_univ, zero_pow (fintype.card_pos_iff.mpr _inst_2), + simpa [h, finset.card_univ, zero_pow (fintype.card_pos_iff.mpr ‹_›), @eq_comm _ (0 : ℝ≥0∞), finset.prod_eq_zero_iff] }, { simp [h] } end @@ -86,7 +161,7 @@ namespace outer_measure /-- `outer_measure.pi m` is the finite product of the outer measures `{m i | i : ι}`. It is defined to be the maximal outer measure `n` with the property that `n (pi univ s) ≤ ∏ i, m i (s i)`, where `pi univ s` is the product of the sets - `{ s i | i : ι }`. -/ + `{s i | i : ι}`. -/ protected def pi (m : Π i, outer_measure (α i)) : outer_measure (Π i, α i) := bounded_by (pi_premeasure m) @@ -164,13 +239,13 @@ variables [encodable ι] equivalence `measurable_equiv.pi_measurable_equiv_tprod`. The definition `measure_theory.measure.pi` should be used instead of this one. -/ def pi' : measure (Π i, α i) := -measure.map (tprod.elim' encodable.mem_sorted_univ) (measure.tprod (encodable.sorted_univ ι) μ) +measure.map (tprod.elim' mem_sorted_univ) (measure.tprod (sorted_univ ι) μ) lemma pi'_pi [∀ i, sigma_finite (μ i)] {s : Π i, set (α i)} (hs : ∀ i, measurable_set (s i)) : pi' μ (pi univ s) = ∏ i, μ i (s i) := begin - have hl := λ i : ι, encodable.mem_sorted_univ i, - have hnd := @encodable.sorted_univ_nodup ι _ _, + have hl := λ i : ι, mem_sorted_univ i, + have hnd := @sorted_univ_nodup ι _ _, rw [pi', map_apply (measurable_tprod_elim' hl) (measurable_set.pi_fintype (λ i _, hs i)), elim_preimage_pi hnd, tprod_tprod _ μ hs, ← list.prod_to_finset _ hnd], congr' with i, simp [hl] @@ -179,8 +254,8 @@ end lemma pi'_pi_le [∀ i, sigma_finite (μ i)] {s : Π i, set (α i)} : pi' μ (pi univ s) ≤ ∏ i, μ i (s i) := begin - have hl := λ i : ι, encodable.mem_sorted_univ i, - have hnd := @encodable.sorted_univ_nodup ι _ _, + have hl := λ i : ι, mem_sorted_univ i, + have hnd := @sorted_univ_nodup ι _ _, apply ((pi_measurable_equiv_tprod hnd hl).symm.map_apply (pi univ s)).trans_le, dsimp only [pi_measurable_equiv_tprod, tprod.pi_equiv_tprod, coe_symm_mk, equiv.coe_fn_symm_mk], rw [elim_preimage_pi hnd], @@ -212,15 +287,13 @@ end @[irreducible] protected def pi : measure (Π i, α i) := to_measure (outer_measure.pi (λ i, (μ i).to_outer_measure)) (pi_caratheodory μ) -variables [∀ i, sigma_finite (μ i)] - -lemma pi_pi (s : Π i, set (α i)) (hs : ∀ i, measurable_set (s i)) : +lemma pi_pi [∀ i, sigma_finite (μ i)] (s : Π i, set (α i)) (hs : ∀ i, measurable_set (s i)) : measure.pi μ (pi univ s) = ∏ i, μ i (s i) := begin refine le_antisymm _ _, { rw [measure.pi, to_measure_apply _ _ (measurable_set.pi_fintype (λ i _, hs i))], apply outer_measure.pi_pi_le }, - { haveI : encodable ι := encodable.fintype.encodable ι, + { haveI : encodable ι := fintype.encodable ι, rw [← pi'_pi μ hs], simp_rw [← pi'_pi μ hs, measure.pi, to_measure_apply _ _ (measurable_set.pi_fintype (λ i _, hs i)), ← to_outer_measure_apply], @@ -233,6 +306,62 @@ begin exact pi'_pi_le μ } end +variable {μ} + +/-- `μ.prod ν` has finite spanning sets in rectangles of finite spanning sets. -/ +def finite_spanning_sets_in.pi {C : Π i, set (set (α i))} + (hμ : ∀ i, (μ i).finite_spanning_sets_in (C i)) (hC : ∀ i (s ∈ C i), measurable_set s) : + (measure.pi μ).finite_spanning_sets_in (pi univ '' pi univ C) := +begin + haveI := λ i, (hμ i).sigma_finite (hC i), + haveI := fintype.encodable ι, + let e : ℕ → (ι → ℕ) := λ n, (decode (ι → ℕ) n).iget, + refine ⟨λ n, pi univ (λ i, (hμ i).set (e n i)), λ n, _, λ n, _, _⟩, + { refine mem_image_of_mem _ (λ i _, (hμ i).set_mem _) }, + { simp_rw [pi_pi μ (λ i, (hμ i).set (e n i)) (λ i, hC i _ ((hμ i).set_mem _))], + exact ennreal.prod_lt_top (λ i _, (hμ i).finite _) }, + { simp_rw [(surjective_decode_iget (ι → ℕ)).Union_comp (λ x, pi univ (λ i, (hμ i).set (x i))), + Union_univ_pi (λ i, (hμ i).set), (hμ _).spanning, pi_univ] } +end + +/-- A measure on a finite product space equals the product measure if they are equal on rectangles + with as sides sets that generate the corresponding σ-algebras. -/ +lemma pi_eq_generate_from {C : Π i, set (set (α i))} + (hC : ∀ i, generate_from (C i) = _inst_3 i) + (h2C : ∀ i, is_pi_system (C i)) + (h3C : ∀ i, (μ i).finite_spanning_sets_in (C i)) + {μν : measure (Π i, α i)} + (h₁ : ∀ s : Π i, set (α i), (∀ i, s i ∈ C i) → μν (pi univ s) = ∏ i, μ i (s i)) : + measure.pi μ = μν := +begin + have h4C : ∀ i (s : set (α i)), s ∈ C i → measurable_set s, + { intros i s hs, rw [← hC], exact measurable_set_generate_from hs }, + refine (finite_spanning_sets_in.pi h3C h4C).ext + (generate_from_eq_pi hC (λ i, (h3C i).is_countably_spanning)).symm + (is_pi_system.pi h2C) _, + rintro _ ⟨s, hs, rfl⟩, + rw [mem_univ_pi] at hs, + haveI := λ i, (h3C i).sigma_finite (h4C i), + simp_rw [h₁ s hs, pi_pi μ s (λ i, h4C i _ (hs i))] +end + +variables [∀ i, sigma_finite (μ i)] + +/-- A measure on a finite product space equals the product measure if they are equal on + rectangles. -/ +lemma pi_eq {μ' : measure (Π i, α i)} + (h : ∀ s : Π i, set (α i), (∀ i, measurable_set (s i)) → μ' (pi univ s) = ∏ i, μ i (s i)) : + measure.pi μ = μ' := +pi_eq_generate_from (λ i, generate_from_measurable_set) + (λ i, is_pi_system_measurable_set) + (λ i, (μ i).to_finite_spanning_sets_in) h + +variable (μ) + +instance pi.sigma_finite : sigma_finite (measure.pi μ) := +⟨⟨(finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in) (λ _ _, id)).mono $ + by { rintro _ ⟨s, hs, rfl⟩, exact measurable_set.pi_fintype hs }⟩⟩ + lemma pi_eval_preimage_null {i : ι} {s : set (α i)} (hs : μ i s = 0) : measure.pi μ (eval i ⁻¹' s) = 0 := begin diff --git a/src/measure_theory/prod.lean b/src/measure_theory/prod.lean index 0ac2730268a03..426fdec76ed12 100644 --- a/src/measure_theory/prod.lean +++ b/src/measure_theory/prod.lean @@ -113,7 +113,7 @@ begin intro n, apply measurable_set_generate_from, exact ⟨s, t n, hs, h1t n, rfl⟩ }, { rcases hC with ⟨t, h1t, h2t⟩, - rw [← univ_prod, ← h2t, Union_prod], + rw [← univ_prod, ← h2t, Union_prod_const], apply measurable_set.Union, rintro n, apply measurable_set_generate_from, exact mem_image2_of_mem (h1t n) hs } }, @@ -434,7 +434,7 @@ instance prod.sigma_finite : sigma_finite (μ.prod ν) := ⟨⟨(μ.to_finite_spanning_sets_in.prod ν.to_finite_spanning_sets_in (λ _, id) (λ _, id)).mono $ by { rintro _ ⟨s, t, hs, ht, rfl⟩, exact hs.prod ht }⟩⟩ -/-- Measures on a product space are equal the product measure if they are equal on rectangles +/-- A measure on a product space equals the product measure if they are equal on rectangles with as sides sets that generate the corresponding σ-algebras. -/ lemma prod_eq_generate_from {μ : measure α} {ν : measure β} {C : set (set α)} {D : set (set β)} (hC : generate_from C = ‹_›) @@ -454,7 +454,7 @@ begin simp_rw [h₁ s hs t ht, prod_prod (h4C s hs) (h4D t ht)] } end -/-- Measures on a product space are equal to the product measure if they are equal on rectangles. -/ +/-- A measure on a product space equals the product measure if they are equal on rectangles. -/ lemma prod_eq {μν : measure (α × β)} (h : ∀ s t, measurable_set s → measurable_set t → μν (s.prod t) = μ s * ν t) : μ.prod ν = μν := prod_eq_generate_from generate_from_measurable_set generate_from_measurable_set