Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit bf6a013

Browse files
hrmacbethhrmacbeth
committed
chore(measure_theory/{constructions/borel_space,integral/lebesgue}): split (#19015)
Remove dependence on ```text import analysis.complex.basic import analysis.normed_space.basic import topology.instances.add_circle import topology.metric_space.metrizable ``` from `measure_theory.constructions.borel_space` (in particular this gets rid of the `operator_norm` dependency, which is currently the big blocker) and `measure_theory.integral.lebesgue`.
1 parent 2f5b500 commit bf6a013

23 files changed

Lines changed: 357 additions & 299 deletions

‎src/analysis/calculus/fderiv_measurable.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Sébastien Gouëzel, Yury Kudryashov
55
-/
66
import analysis.calculus.deriv
7+
import measure_theory.constructions.borel_space.continuous_linear_map
78
import measure_theory.function.strongly_measurable.basic
89

910
/-!

‎src/dynamics/ergodic/conservative.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov
55
-/
6-
import measure_theory.constructions.borel_space
6+
import measure_theory.constructions.borel_space.basic
77
import dynamics.ergodic.measure_preserving
88
import combinatorics.pigeonhole
99

src/measure_theory/constructions/borel_space.lean renamed to src/measure_theory/constructions/borel_space/basic.lean

Lines changed: 2 additions & 255 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,18 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl, Yury Kudryashov
55
-/
6-
import analysis.complex.basic
7-
import analysis.normed_space.finite_dimension
6+
import analysis.normed.group.basic
87
import measure_theory.function.ae_measurable_sequence
98
import measure_theory.group.arithmetic
109
import measure_theory.lattice
1110
import measure_theory.measure.open_pos
1211
import topology.algebra.order.liminf_limsup
1312
import topology.continuous_function.basic
14-
import topology.instances.add_circle
1513
import topology.instances.ereal
14+
import topology.metric_space.hausdorff_distance
1615
import topology.G_delta
1716
import topology.order.lattice
1817
import topology.semicontinuous
19-
import topology.metric_space.metrizable
2018

2119
/-!
2220
# Borel (measurable) space
@@ -1327,11 +1325,6 @@ instance nat.borel_space : borel_space ℕ := ⟨borel_eq_top_of_discrete.symm
13271325
instance int.borel_space : borel_space ℤ := ⟨borel_eq_top_of_discrete.symm⟩
13281326
instance rat.borel_space : borel_space ℚ := ⟨borel_eq_top_of_countable.symm⟩
13291327

1330-
@[priority 900]
1331-
instance is_R_or_C.measurable_space {𝕜 : Type*} [is_R_or_C 𝕜] : measurable_space 𝕜 := borel 𝕜
1332-
@[priority 900]
1333-
instance is_R_or_C.borel_space {𝕜 : Type*} [is_R_or_C 𝕜] : borel_space 𝕜 := ⟨rfl⟩
1334-
13351328
/- Instances on `real` and `complex` are special cases of `is_R_or_C` but without these instances,
13361329
Lean fails to prove `borel_space (ι → ℝ)`, so we leave them here. -/
13371330

@@ -1347,18 +1340,6 @@ instance ennreal.borel_space : borel_space ℝ≥0∞ := ⟨rfl⟩
13471340
instance ereal.measurable_space : measurable_space ereal := borel ereal
13481341
instance ereal.borel_space : borel_space ereal := ⟨rfl⟩
13491342

1350-
instance complex.measurable_space : measurable_space ℂ := borel ℂ
1351-
instance complex.borel_space : borel_space ℂ := ⟨rfl⟩
1352-
1353-
instance add_circle.measurable_space {a : ℝ} : measurable_space (add_circle a) :=
1354-
borel (add_circle a)
1355-
1356-
instance add_circle.borel_space {a : ℝ} : borel_space (add_circle a) := ⟨rfl⟩
1357-
1358-
@[measurability] protected lemma add_circle.measurable_mk' {a : ℝ} :
1359-
measurable (coe : ℝ → add_circle a) :=
1360-
continuous.measurable $ add_circle.continuous_mk' a
1361-
13621343
/-- One can cut out `ℝ≥0∞` into the sets `{0}`, `Ico (t^n) (t^(n+1))` for `n : ℤ` and `{∞}`. This
13631344
gives a way to compute the measure of a set in terms of sets on which a given function `f` does not
13641345
fluctuate by more than `t`. -/
@@ -1899,237 +1880,3 @@ lemma ae_measurable.ennnorm {f : β → α} {μ : measure β} (hf : ae_measurabl
18991880
measurable_ennnorm.comp_ae_measurable hf
19001881

19011882
end normed_add_comm_group
1902-
1903-
section limits
1904-
1905-
variables [topological_space β] [pseudo_metrizable_space β] [measurable_space β] [borel_space β]
1906-
1907-
open metric
1908-
1909-
/-- A limit (over a general filter) of measurable `ℝ≥0∞` valued functions is measurable. -/
1910-
lemma measurable_of_tendsto_ennreal' {ι} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞} (u : filter ι)
1911-
[ne_bot u] [is_countably_generated u] (hf : ∀ i, measurable (f i)) (lim : tendsto f u (𝓝 g)) :
1912-
measurable g :=
1913-
begin
1914-
rcases u.exists_seq_tendsto with ⟨x, hx⟩,
1915-
rw [tendsto_pi_nhds] at lim,
1916-
have : (λ y, liminf (λ n, (f (x n) y : ℝ≥0∞)) at_top) = g :=
1917-
by { ext1 y, exact ((lim y).comp hx).liminf_eq, },
1918-
rw ← this,
1919-
show measurable (λ y, liminf (λ n, (f (x n) y : ℝ≥0∞)) at_top),
1920-
exact measurable_liminf (λ n, hf (x n)),
1921-
end
1922-
1923-
/-- A sequential limit of measurable `ℝ≥0∞` valued functions is measurable. -/
1924-
lemma measurable_of_tendsto_ennreal {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞}
1925-
(hf : ∀ i, measurable (f i)) (lim : tendsto f at_top (𝓝 g)) : measurable g :=
1926-
measurable_of_tendsto_ennreal' at_top hf lim
1927-
1928-
/-- A limit (over a general filter) of measurable `ℝ≥0` valued functions is measurable. -/
1929-
lemma measurable_of_tendsto_nnreal' {ι} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : filter ι)
1930-
[ne_bot u] [is_countably_generated u] (hf : ∀ i, measurable (f i)) (lim : tendsto f u (𝓝 g)) :
1931-
measurable g :=
1932-
begin
1933-
simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf ⊢,
1934-
refine measurable_of_tendsto_ennreal' u hf _,
1935-
rw tendsto_pi_nhds at lim ⊢,
1936-
exact λ x, (ennreal.continuous_coe.tendsto (g x)).comp (lim x),
1937-
end
1938-
1939-
/-- A sequential limit of measurable `ℝ≥0` valued functions is measurable. -/
1940-
lemma measurable_of_tendsto_nnreal {f : ℕ → α → ℝ≥0} {g : α → ℝ≥0}
1941-
(hf : ∀ i, measurable (f i)) (lim : tendsto f at_top (𝓝 g)) : measurable g :=
1942-
measurable_of_tendsto_nnreal' at_top hf lim
1943-
1944-
/-- A limit (over a general filter) of measurable functions valued in a (pseudo) metrizable space is
1945-
measurable. -/
1946-
lemma measurable_of_tendsto_metrizable' {ι} {f : ι → α → β} {g : α → β}
1947-
(u : filter ι) [ne_bot u] [is_countably_generated u]
1948-
(hf : ∀ i, measurable (f i)) (lim : tendsto f u (𝓝 g)) :
1949-
measurable g :=
1950-
begin
1951-
letI : pseudo_metric_space β := pseudo_metrizable_space_pseudo_metric β,
1952-
apply measurable_of_is_closed', intros s h1s h2s h3s,
1953-
have : measurable (λ x, inf_nndist (g x) s),
1954-
{ suffices : tendsto (λ i x, inf_nndist (f i x) s) u (𝓝 (λ x, inf_nndist (g x) s)),
1955-
from measurable_of_tendsto_nnreal' u (λ i, (hf i).inf_nndist) this,
1956-
rw [tendsto_pi_nhds] at lim ⊢, intro x,
1957-
exact ((continuous_inf_nndist_pt s).tendsto (g x)).comp (lim x) },
1958-
have h4s : g ⁻¹' s = (λ x, inf_nndist (g x) s) ⁻¹' {0},
1959-
{ ext x, simp [h1s, ← h1s.mem_iff_inf_dist_zero h2s, ← nnreal.coe_eq_zero] },
1960-
rw [h4s], exact this (measurable_set_singleton 0),
1961-
end
1962-
1963-
/-- A sequential limit of measurable functions valued in a (pseudo) metrizable space is
1964-
measurable. -/
1965-
lemma measurable_of_tendsto_metrizable {f : ℕ → α → β} {g : α → β}
1966-
(hf : ∀ i, measurable (f i)) (lim : tendsto f at_top (𝓝 g)) :
1967-
measurable g :=
1968-
measurable_of_tendsto_metrizable' at_top hf lim
1969-
1970-
lemma ae_measurable_of_tendsto_metrizable_ae {ι}
1971-
{μ : measure α} {f : ι → α → β} {g : α → β}
1972-
(u : filter ι) [hu : ne_bot u] [is_countably_generated u]
1973-
(hf : ∀ n, ae_measurable (f n) μ) (h_tendsto : ∀ᵐ x ∂μ, tendsto (λ n, f n x) u (𝓝 (g x))) :
1974-
ae_measurable g μ :=
1975-
begin
1976-
rcases u.exists_seq_tendsto with ⟨v, hv⟩,
1977-
have h'f : ∀ n, ae_measurable (f (v n)) μ := λ n, hf (v n),
1978-
set p : α → (ℕ → β) → Prop := λ x f', tendsto (λ n, f' n) at_top (𝓝 (g x)),
1979-
have hp : ∀ᵐ x ∂μ, p x (λ n, f (v n) x),
1980-
by filter_upwards [h_tendsto] with x hx using hx.comp hv,
1981-
set ae_seq_lim := λ x, ite (x ∈ ae_seq_set h'f p) (g x) (⟨f (v 0) x⟩ : nonempty β).some with hs,
1982-
refine ⟨ae_seq_lim, measurable_of_tendsto_metrizable' at_top (ae_seq.measurable h'f p)
1983-
(tendsto_pi_nhds.mpr (λ x, _)), _⟩,
1984-
{ simp_rw [ae_seq, ae_seq_lim],
1985-
split_ifs with hx,
1986-
{ simp_rw ae_seq.mk_eq_fun_of_mem_ae_seq_set h'f hx,
1987-
exact @ae_seq.fun_prop_of_mem_ae_seq_set _ α β _ _ _ _ _ h'f x hx, },
1988-
{ exact tendsto_const_nhds } },
1989-
{ exact (ite_ae_eq_of_measure_compl_zero g (λ x, (⟨f (v 0) x⟩ : nonempty β).some)
1990-
(ae_seq_set h'f p) (ae_seq.measure_compl_ae_seq_set_eq_zero h'f hp)).symm },
1991-
end
1992-
1993-
lemma ae_measurable_of_tendsto_metrizable_ae' {μ : measure α} {f : ℕ → α → β} {g : α → β}
1994-
(hf : ∀ n, ae_measurable (f n) μ)
1995-
(h_ae_tendsto : ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (g x))) :
1996-
ae_measurable g μ :=
1997-
ae_measurable_of_tendsto_metrizable_ae at_top hf h_ae_tendsto
1998-
1999-
lemma ae_measurable_of_unif_approx {β} [measurable_space β] [pseudo_metric_space β] [borel_space β]
2000-
{μ : measure α} {g : α → β}
2001-
(hf : ∀ ε > (0 : ℝ), ∃ (f : α → β), ae_measurable f μ ∧ ∀ᵐ x ∂μ, dist (f x) (g x) ≤ ε) :
2002-
ae_measurable g μ :=
2003-
begin
2004-
obtain ⟨u, u_anti, u_pos, u_lim⟩ :
2005-
∃ (u : ℕ → ℝ), strict_anti u ∧ (∀ (n : ℕ), 0 < u n) ∧ tendsto u at_top (𝓝 0) :=
2006-
exists_seq_strict_anti_tendsto (0 : ℝ),
2007-
choose f Hf using λ (n : ℕ), hf (u n) (u_pos n),
2008-
have : ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (g x)),
2009-
{ have : ∀ᵐ x ∂ μ, ∀ n, dist (f n x) (g x) ≤ u n := ae_all_iff.2 (λ n, (Hf n).2),
2010-
filter_upwards [this],
2011-
assume x hx,
2012-
rw tendsto_iff_dist_tendsto_zero,
2013-
exact squeeze_zero (λ n, dist_nonneg) hx u_lim },
2014-
exact ae_measurable_of_tendsto_metrizable_ae' (λ n, (Hf n).1) this,
2015-
end
2016-
2017-
lemma measurable_of_tendsto_metrizable_ae {μ : measure α} [μ.is_complete] {f : ℕ → α → β}
2018-
{g : α → β} (hf : ∀ n, measurable (f n))
2019-
(h_ae_tendsto : ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (g x))) :
2020-
measurable g :=
2021-
ae_measurable_iff_measurable.mp
2022-
(ae_measurable_of_tendsto_metrizable_ae' (λ i, (hf i).ae_measurable) h_ae_tendsto)
2023-
2024-
lemma measurable_limit_of_tendsto_metrizable_ae {ι} [countable ι] [nonempty ι] {μ : measure α}
2025-
{f : ι → α → β} {L : filter ι} [L.is_countably_generated] (hf : ∀ n, ae_measurable (f n) μ)
2026-
(h_ae_tendsto : ∀ᵐ x ∂μ, ∃ l : β, tendsto (λ n, f n x) L (𝓝 l)) :
2027-
∃ (f_lim : α → β) (hf_lim_meas : measurable f_lim),
2028-
∀ᵐ x ∂μ, tendsto (λ n, f n x) L (𝓝 (f_lim x)) :=
2029-
begin
2030-
inhabit ι,
2031-
unfreezingI { rcases eq_or_ne L ⊥ with rfl | hL },
2032-
{ exact ⟨(hf default).mk _, (hf default).measurable_mk,
2033-
eventually_of_forall $ λ x, tendsto_bot⟩ },
2034-
haveI : ne_bot L := ⟨hL⟩,
2035-
let p : α → (ι → β) → Prop := λ x f', ∃ l : β, tendsto (λ n, f' n) L (𝓝 l),
2036-
have hp_mem : ∀ x ∈ ae_seq_set hf p, p x (λ n, f n x),
2037-
from λ x hx, ae_seq.fun_prop_of_mem_ae_seq_set hf hx,
2038-
have h_ae_eq : ∀ᵐ x ∂μ, ∀ n, ae_seq hf p n x = f n x,
2039-
from ae_seq.ae_seq_eq_fun_ae hf h_ae_tendsto,
2040-
let f_lim : α → β := λ x, dite (x ∈ ae_seq_set hf p) (λ h, (hp_mem x h).some)
2041-
(λ h, (⟨f default x⟩ : nonempty β).some),
2042-
have hf_lim : ∀ x, tendsto (λ n, ae_seq hf p n x) L (𝓝 (f_lim x)),
2043-
{ intros x,
2044-
simp only [f_lim, ae_seq],
2045-
split_ifs,
2046-
{ refine (hp_mem x h).some_spec.congr (λ n, _),
2047-
exact (ae_seq.mk_eq_fun_of_mem_ae_seq_set hf h n).symm },
2048-
{ exact tendsto_const_nhds, }, },
2049-
have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, tendsto (λ n, f n x) L (𝓝 (f_lim x)),
2050-
from h_ae_eq.mono (λ x hx, (hf_lim x).congr hx),
2051-
have h_f_lim_meas : measurable f_lim,
2052-
from measurable_of_tendsto_metrizable' L (ae_seq.measurable hf p)
2053-
(tendsto_pi_nhds.mpr (λ x, hf_lim x)),
2054-
exact ⟨f_lim, h_f_lim_meas, h_ae_tendsto_f_lim⟩,
2055-
end
2056-
2057-
end limits
2058-
2059-
namespace continuous_linear_map
2060-
2061-
variables {𝕜 : Type*} [normed_field 𝕜]
2062-
variables {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E] [measurable_space E]
2063-
[opens_measurable_space E] {F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
2064-
[measurable_space F] [borel_space F]
2065-
2066-
@[measurability]
2067-
protected lemma measurable (L : E →L[𝕜] F) : measurable L :=
2068-
L.continuous.measurable
2069-
2070-
lemma measurable_comp (L : E →L[𝕜] F) {φ : α → E} (φ_meas : measurable φ) :
2071-
measurable (λ (a : α), L (φ a)) :=
2072-
L.measurable.comp φ_meas
2073-
2074-
end continuous_linear_map
2075-
2076-
namespace continuous_linear_map
2077-
2078-
variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
2079-
variables {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
2080-
{F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
2081-
2082-
instance : measurable_space (E →L[𝕜] F) := borel _
2083-
2084-
instance : borel_space (E →L[𝕜] F) := ⟨rfl⟩
2085-
2086-
@[measurability]
2087-
lemma measurable_apply [measurable_space F] [borel_space F] (x : E) :
2088-
measurable (λ f : E →L[𝕜] F, f x) :=
2089-
(apply 𝕜 F x).continuous.measurable
2090-
2091-
@[measurability]
2092-
lemma measurable_apply' [measurable_space E] [opens_measurable_space E]
2093-
[measurable_space F] [borel_space F] :
2094-
measurable (λ (x : E) (f : E →L[𝕜] F), f x) :=
2095-
measurable_pi_lambda _ $ λ f, f.measurable
2096-
2097-
@[measurability]
2098-
lemma measurable_coe [measurable_space F] [borel_space F] :
2099-
measurable (λ (f : E →L[𝕜] F) (x : E), f x) :=
2100-
measurable_pi_lambda _ measurable_apply
2101-
2102-
end continuous_linear_map
2103-
2104-
section continuous_linear_map_nontrivially_normed_field
2105-
2106-
variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
2107-
variables {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E] [measurable_space E]
2108-
[borel_space E] {F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
2109-
2110-
@[measurability]
2111-
lemma measurable.apply_continuous_linear_map {φ : α → F →L[𝕜] E} (hφ : measurable φ) (v : F) :
2112-
measurable (λ a, φ a v) :=
2113-
(continuous_linear_map.apply 𝕜 E v).measurable.comp hφ
2114-
2115-
@[measurability]
2116-
lemma ae_measurable.apply_continuous_linear_map {φ : α → F →L[𝕜] E} {μ : measure α}
2117-
(hφ : ae_measurable φ μ) (v : F) : ae_measurable (λ a, φ a v) μ :=
2118-
(continuous_linear_map.apply 𝕜 E v).measurable.comp_ae_measurable hφ
2119-
2120-
end continuous_linear_map_nontrivially_normed_field
2121-
2122-
section normed_space
2123-
variables {𝕜 : Type*} [nontrivially_normed_field 𝕜] [complete_space 𝕜] [measurable_space 𝕜]
2124-
variables [borel_space 𝕜] {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
2125-
[measurable_space E] [borel_space E]
2126-
2127-
lemma measurable_smul_const {f : α → 𝕜} {c : E} (hc : c ≠ 0) :
2128-
measurable (λ x, f x • c) ↔ measurable f :=
2129-
(closed_embedding_smul_left hc).measurable_embedding.measurable_comp_iff
2130-
2131-
lemma ae_measurable_smul_const {f : α → 𝕜} {μ : measure α} {c : E} (hc : c ≠ 0) :
2132-
ae_measurable (λ x, f x • c) μ ↔ ae_measurable f μ :=
2133-
(closed_embedding_smul_left hc).measurable_embedding.ae_measurable_comp_iff
2134-
2135-
end normed_space

‎src/measure_theory/constructions/borel_space/complex.lean‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
/-
2+
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yury Kudryashov
5+
-/
6+
import analysis.complex.basic
7+
import measure_theory.constructions.borel_space.basic
8+
9+
/-! # Equip `ℂ` with the Borel sigma-algebra -/
10+
11+
noncomputable theory
12+
13+
@[priority 900]
14+
instance is_R_or_C.measurable_space {𝕜 : Type*} [is_R_or_C 𝕜] : measurable_space 𝕜 := borel 𝕜
15+
@[priority 900]
16+
instance is_R_or_C.borel_space {𝕜 : Type*} [is_R_or_C 𝕜] : borel_space 𝕜 := ⟨rfl⟩
17+
18+
19+
instance complex.measurable_space : measurable_space ℂ := borel ℂ
20+
instance complex.borel_space : borel_space ℂ := ⟨rfl⟩

0 commit comments

Comments
 (0)