Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(measure_theory/constructions/{pi,prod}): drop some measurability assumptions #10241

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(measure_theory/constructions/{pi,prod}): drop some measurability assumptions #10241

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
de14e4e
Snapshot
urkud Nov 9, 2021
b8585a3
Snapshot
urkud Nov 9, 2021
72003a9
Snapshot
urkud Nov 9, 2021
4a88bd7
Fix
urkud Nov 9, 2021
512e0f9
Fix
urkud Nov 9, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
14 changes: 9 additions & 5 deletions src/data/equiv/list.lean
View file
Open in desktop
Expand Up @@ -144,24 +144,28 @@ def fintype_pi (α : Type*) (π : α → Type*) [decidable_eq α] [fintype α] [
def sorted_univ (α) [fintype α] [encodable α] : list α :=
finset.univ.sort (encodable.encode' α ⁻¹'o (≤))

theorem mem_sorted_univ {α} [fintype α] [encodable α] (x : α) : x ∈ sorted_univ α :=
@[simp] theorem mem_sorted_univ {α} [fintype α] [encodable α] (x : α) : x ∈ sorted_univ α :=
(finset.mem_sort _).2 (finset.mem_univ _)

theorem length_sorted_univ {α} [fintype α] [encodable α] :
@[simp] theorem length_sorted_univ (α) [fintype α] [encodable α] :
(sorted_univ α).length = fintype.card α :=
finset.length_sort _

theorem sorted_univ_nodup {α} [fintype α] [encodable α] : (sorted_univ α).nodup :=
@[simp] theorem sorted_univ_nodup (α) [fintype α] [encodable α] : (sorted_univ α).nodup :=
finset.sort_nodup _ _

@[simp] theorem sorted_univ_to_finset (α) [fintype α] [encodable α] [decidable_eq α] :
(sorted_univ α).to_finset = finset.univ :=
finset.sort_to_finset _ _

/-- An encodable `fintype` is equivalent to the same size `fin`. -/
def fintype_equiv_fin {α} [fintype α] [encodable α] :
α ≃ fin (fintype.card α) :=
begin
haveI : decidable_eq α := encodable.decidable_eq_of_encodable _,
transitivity,
{ exact fintype.equiv_fin_of_forall_mem_list mem_sorted_univ (@sorted_univ_nodup α _ _) },
exact equiv.cast (congr_arg _ (@length_sorted_univ α _ _))
{ exact fintype.equiv_fin_of_forall_mem_list mem_sorted_univ (sorted_univ_nodup α) },
exact equiv.cast (congr_arg _ (length_sorted_univ α))
end

/-- If `α` and `β` are encodable and `α` is a fintype, then `α → β` is encodable as well. -/
Expand Down
162 changes: 68 additions & 94 deletions src/measure_theory/constructions/pi.lean
View file
Open in desktop
Expand Up @@ -218,20 +218,11 @@ begin
end

lemma tprod_tprod (l : list δ) (μ : Π i, measure (π i)) [∀ i, sigma_finite (μ i)]
{s : Π i, set (π i)} (hs : ∀ i, measurable_set (s i)) :
(s : Π i, set (π i)) :
measure.tprod l μ (set.tprod l s) = (l.map (λ i, (μ i) (s i))).prod :=
begin
induction l with i l ih, { simp },
simp_rw [tprod_cons, set.tprod, prod_prod (hs i) (measurable_set.tprod l hs), map_cons,
prod_cons, ih]
end

lemma tprod_tprod_le (l : list δ) (μ : Π i, measure (π i)) [∀ i, sigma_finite (μ i)]
(s : Π i, set (π i)) : measure.tprod l μ (set.tprod l s) ≤ (l.map (λ i, (μ i) (s i))).prod :=
begin
induction l with i l ih, { simp [le_refl] },
simp_rw [tprod_cons, set.tprod, map_cons, prod_cons],
refine (prod_prod_le _ _).trans _, exact ennreal.mul_left_mono ih
rw [tprod_cons, set.tprod, prod_prod, map_cons, prod_cons, ih]
end

end tprod
Expand All @@ -247,28 +238,10 @@ variables [encodable ι]
def pi' : measure (Π i, α i) :=
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 : ι, 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]
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 : ι, 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_symm_apply],
rw [elim_preimage_pi hnd],
refine (tprod_tprod_le _ _ _).trans_eq _,
rw [← list.prod_to_finset _ hnd],
congr' with i, simp [hl]
end
lemma pi'_pi [∀ i, sigma_finite (μ i)] (s : Π i, set (α i)) : pi' μ (pi univ s) = ∏ i, μ i (s i) :=
by rw [pi', ← measurable_equiv.pi_measurable_equiv_tprod_symm_apply, measurable_equiv.map_apply,
measurable_equiv.pi_measurable_equiv_tprod_symm_apply, elim_preimage_pi, tprod_tprod _ μ,
← list.prod_to_finset, sorted_univ_to_finset]; exact sorted_univ_nodup ι

end encodable

Expand All @@ -293,73 +266,45 @@ end
@[irreducible] protected def pi : measure (Π i, α i) :=
to_measure (outer_measure.pi (λ i, (μ i).to_outer_measure)) (pi_caratheodory μ)

lemma pi_pi [∀ i, sigma_finite (μ i)] (s : Π i, set (α i)) (hs : ∀ i, measurable_set (s i)) :
lemma pi_pi_aux [∀ 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 ι := fintype.encodable ι,
rw [← pi'_pi μ hs],
simp_rw [← pi'_pi μ hs, measure.pi,
rw [← pi'_pi μ s],
simp_rw [← pi'_pi μ s, measure.pi,
to_measure_apply _ _ (measurable_set.pi_fintype (λ i _, hs i)), ← to_outer_measure_apply],
suffices : (pi' μ).to_outer_measure ≤ outer_measure.pi (λ i, (μ i).to_outer_measure),
{ exact this _ },
clear hs s,
rw [outer_measure.le_pi],
intros s hs,
simp_rw [to_outer_measure_apply],
exact pi'_pi_le μ }
exact (pi'_pi μ s).le }
end

lemma pi_univ [∀ i, sigma_finite (μ i)] : measure.pi μ univ = ∏ i, μ i univ :=
by rw [← pi_univ, pi_pi μ _ (λ i, measurable_set.univ)]

lemma pi_ball [∀ i, sigma_finite (μ i)] [∀ i, metric_space (α i)] [∀ i, borel_space (α i)]
(x : Π i, α i) {r : ℝ} (hr : 0 < r) :
measure.pi μ (metric.ball x r) = ∏ i, μ i (metric.ball (x i) r) :=
begin
rw [ball_pi _ hr, pi_pi],
exact λ i, measurable_set_ball
end

lemma pi_closed_ball [∀ i, sigma_finite (μ i)] [∀ i, metric_space (α i)] [∀ i, borel_space (α i)]
(x : Π i, α i) {r : ℝ} (hr : 0 ≤ r) :
measure.pi μ (metric.closed_ball x r) = ∏ i, μ i (metric.closed_ball (x i) r) :=
begin
rw [closed_ball_pi _ hr, pi_pi],
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. -/
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) :
(hμ : ∀ i, (μ i).finite_spanning_sets_in (C i)) :
(measure.pi μ).finite_spanning_sets_in (pi univ '' pi univ C) :=
begin
haveI := λ i, (hμ i).sigma_finite,
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 _).ne) },
{ calc measure.pi μ (pi univ (λ i, (hμ i).set (e n i)))
≤ measure.pi μ (pi univ (λ i, to_measurable (μ i) ((hμ i).set (e n i)))) :
measure_mono (pi_mono $ λ i hi, subset_to_measurable _ _)
... = ∏ i, μ i (to_measurable (μ i) ((hμ i).set (e n i))) :
pi_pi_aux μ _ (λ i, measurable_set_to_measurable _ _)
... = ∏ i, μ i ((hμ i).set (e n i)) :
by simp only [measure_to_measurable]
... < ∞ : ennreal.prod_lt_top (λ i hi, ((hμ i).finite _).ne) },
{ 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, set.pi_univ] }
end
Expand All @@ -376,13 +321,13 @@ lemma pi_eq_generate_from {C : Π i, set (set (α i))}
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
refine (finite_spanning_sets_in.pi h3C).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,
simp_rw [h₁ s hs, pi_pi μ s (λ i, h4C i _ (hs i))]
simp_rw [h₁ s hs, pi_pi_aux μ s (λ i, h4C i _ (hs i))]
end

variables [∀ i, sigma_finite (μ i)]
Expand All @@ -396,10 +341,46 @@ pi_eq_generate_from (λ i, generate_from_measurable_set)
(λ i, is_pi_system_measurable_set)
(λ i, (μ i).to_finite_spanning_sets_in) h

variable (μ)
variables (μ)

lemma pi'_eq_pi [encodable ι] : pi' μ = measure.pi μ :=
eq.symm $ pi_eq $ λ s hs, pi'_pi μ s

@[simp] lemma pi_pi (s : Π i, set (α i)) : measure.pi μ (pi univ s) = ∏ i, μ i (s i) :=
begin
haveI : encodable ι := fintype.encodable ι,
rw [← pi'_eq_pi, pi'_pi]
end

lemma pi_univ : measure.pi μ univ = ∏ i, μ i univ := by rw [← pi_univ, pi_pi μ]

lemma pi_ball [∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ}
(hr : 0 < r) :
measure.pi μ (metric.ball x r) = ∏ i, μ i (metric.ball (x i) r) :=
by rw [ball_pi _ hr, pi_pi]

lemma pi_closed_ball [∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ}
(hr : 0 ≤ r) :
measure.pi μ (metric.closed_ball x r) = ∏ i, μ i (metric.closed_ball (x i) r) :=
by rw [closed_ball_pi _ hr, pi_pi]

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

instance pi.sigma_finite : sigma_finite (measure.pi μ) :=
(finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in) (λ _ _, id)).sigma_finite
(finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in)).sigma_finite

lemma pi_of_empty {α : Type*} [is_empty α] {β : α → Type*} {m : Π a, measurable_space (β a)}
(μ : Π a : α, measure (β a)) (x : Π a, β a := is_empty_elim) :
Expand All @@ -417,7 +398,7 @@ lemma {u} pi_fin_two_eq_map {α : fin 2 → Type u} {m : Π i, measurable_space
begin
refine pi_eq (λ s hs, _),
rw [measurable_equiv.map_apply, fin.prod_univ_succ, fin.prod_univ_succ, fin.prod_univ_zero,
mul_one, ← measure.prod_prod (hs _) (hs _)]; [skip, apply_instance],
mul_one, ← measure.prod_prod],
congr' 1,
ext ⟨a, b⟩,
simp [fin.forall_fin_succ, is_empty.forall_iff]
Expand Down Expand Up @@ -451,9 +432,8 @@ begin
clear_dependent s,
/- Now rewrite it as `set.pi`, and apply `pi_pi` -/
rw [← univ_pi_update_univ, pi_pi],
{ apply finset.prod_eq_zero (finset.mem_univ i), simp [hμt] },
{ intro j,
rcases em (j = i) with rfl | hj; simp * }
apply finset.prod_eq_zero (finset.mem_univ i),
simp [hμt]
end

lemma pi_hyperplane (i : ι) [has_no_atoms (μ i)] (x : α i) :
Expand Down Expand Up @@ -549,15 +529,14 @@ lemma pi_has_no_atoms (i : ι) [has_no_atoms (μ i)] :
instance [h : nonempty ι] [∀ i, has_no_atoms (μ i)] : has_no_atoms (measure.pi μ) :=
h.elim $ λ i, pi_has_no_atoms i

instance [Π i, topological_space (α i)] [∀ i, opens_measurable_space (α i)]
[∀ i, is_locally_finite_measure (μ i)] :
instance [Π i, topological_space (α i)] [∀ i, is_locally_finite_measure (μ i)] :
is_locally_finite_measure (measure.pi μ) :=
begin
refine ⟨λ x, _⟩,
choose s hxs ho hμ using λ i, (μ i).exists_is_open_measure_lt_top (x i),
refine ⟨pi univ s, set_pi_mem_nhds finite_univ (λ i hi, is_open.mem_nhds (ho i) (hxs i)), _⟩,
rw [pi_pi],
exacts [ennreal.prod_lt_top (λ i _, (hμ i).ne), λ i, (ho i).measurable_set]
exact ennreal.prod_lt_top (λ i _, (hμ i).ne)
end

variable (μ)
Expand Down Expand Up @@ -585,10 +564,6 @@ begin
rw [measure.map_apply (measurable_pi_equiv_pi_subtype_prod_symm _ p)
(measurable_set.univ_pi_fintype hs), A,
measure.prod_prod, pi_pi, pi_pi, ← fintype.prod_subtype_mul_prod_subtype p (λ i, μ i (s i))],
{ exact λ i, hs i.1 },
{ exact λ i, hs i.1 },
{ exact measurable_set.univ_pi_fintype (λ i, hs i.1) },
{ exact measurable_set.univ_pi_fintype (λ i, hs i.1) },
end

lemma map_pi_equiv_pi_subtype_prod (p : ι → Prop) [decidable_pred p] :
Expand All @@ -610,18 +585,17 @@ lemma volume_pi [Π i, measure_space (α i)] :
rfl

lemma volume_pi_pi [Π i, measure_space (α i)] [∀ i, sigma_finite (volume : measure (α i))]
(s : Π i, set (α i)) (hs : ∀ i, measurable_set (s i)) :
(s : Π i, set (α i)) :
volume (pi univ s) = ∏ i, volume (s i) :=
measure.pi_pi (λ i, volume) s hs
measure.pi_pi (λ i, volume) s

lemma volume_pi_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (volume : measure (α i))]
[∀ i, metric_space (α i)] [∀ i, borel_space (α i)] (x : Π i, α i) {r : ℝ} (hr : 0 < r) :
[∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ} (hr : 0 < r) :
volume (metric.ball x r) = ∏ i, volume (metric.ball (x i) r) :=
measure.pi_ball _ _ hr

lemma volume_pi_closed_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (volume : measure (α i))]
[∀ i, metric_space (α i)] [∀ i, borel_space (α i)]
(x : Π i, α i) {r : ℝ} (hr : 0 ≤ r) :
[∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ} (hr : 0 ≤ r) :
volume (metric.closed_ball x r) = ∏ i, volume (metric.closed_ball (x i) r) :=
measure.pi_closed_ball _ _ hr

Expand Down