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

Commit f3b0295

Browse files
committed
chore(measure_theory): use notation for (⊤ : ℝ≥0∞) (#6080)
1 parent 5d4d815 commit f3b0295

14 files changed

+197
-197
lines changed

src/measure_theory/bochner_integration.lean

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -191,9 +191,9 @@ variables {μ : measure α}
191191
finite volume support. -/
192192
lemma integrable_iff_fin_meas_supp {f : α →ₛ E} {μ : measure α} :
193193
integrable f μ ↔ f.fin_meas_supp μ :=
194-
calc integrable f μ ↔ ∫⁻ x, f.map (coe ∘ nnnorm : E → ℝ≥0∞) x ∂μ < :
194+
calc integrable f μ ↔ ∫⁻ x, f.map (coe ∘ nnnorm : E → ℝ≥0∞) x ∂μ < :
195195
and_iff_right f.ae_measurable
196-
... ↔ (f.map (coe ∘ nnnorm : E → ℝ≥0∞)).lintegral μ < : by rw lintegral_eq_lintegral
196+
... ↔ (f.map (coe ∘ nnnorm : E → ℝ≥0∞)).lintegral μ < : by rw lintegral_eq_lintegral
197197
... ↔ (f.map (coe ∘ nnnorm : E → ℝ≥0∞)).fin_meas_supp μ : iff.symm $
198198
fin_meas_supp.iff_lintegral_lt_top $ eventually_of_forall $ λ x, coe_lt_top
199199
... ↔ _ : fin_meas_supp.map_iff $ λ b, coe_eq_zero.trans nnnorm_eq_zero
@@ -256,7 +256,7 @@ end
256256
`α →ₛ ℝ≥0∞`. But since `ℝ≥0∞` is not a `normed_space`, we need some form of coercion.
257257
See `integral_eq_lintegral` for a simpler version. -/
258258
lemma integral_eq_lintegral' {f : α →ₛ E} {g : E → ℝ≥0∞} (hf : integrable f μ) (hg0 : g 0 = 0)
259-
(hgt : ∀b, g b < ):
259+
(hgt : ∀b, g b < ):
260260
(f.map (ennreal.to_real ∘ g)).integral μ = ennreal.to_real (∫⁻ a, g (f a) ∂μ) :=
261261
begin
262262
have hf' : f.fin_meas_supp μ := integrable_iff_fin_meas_supp.1 hf,
@@ -630,7 +630,7 @@ begin
630630
end
631631

632632
lemma lintegral_edist_to_simple_func_lt_top (f g : α →₁ₛ[μ] E) :
633-
∫⁻ (x : α), edist ((to_simple_func f) x) ((to_simple_func g) x) ∂μ < :=
633+
∫⁻ (x : α), edist ((to_simple_func f) x) ((to_simple_func g) x) ∂μ < :=
634634
begin
635635
rw lintegral_rw₂ (to_simple_func_eq_to_fun f) (to_simple_func_eq_to_fun g),
636636
exact lintegral_edist_to_fun_lt_top _ _
@@ -1255,7 +1255,7 @@ begin
12551255
rw [← lt_top_iff_ne_top], convert hfi.has_finite_integral, ext1 x, rw [real.nnnorm_coe_eq_self]
12561256
end
12571257

1258-
lemma integral_to_real {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hf : ∀ᵐ x ∂μ, f x < ) :
1258+
lemma integral_to_real {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hf : ∀ᵐ x ∂μ, f x < ) :
12591259
∫ a, (f a).to_real ∂μ = (∫⁻ a, f a ∂μ).to_real :=
12601260
begin
12611261
rw [integral_eq_lintegral_of_nonneg_ae _ hfm.to_real],
@@ -1378,7 +1378,7 @@ end
13781378

13791379
@[simp] lemma integral_const (c : E) : ∫ x : α, c ∂μ = (μ univ).to_real • c :=
13801380
begin
1381-
by_cases hμ : μ univ < ,
1381+
by_cases hμ : μ univ < ,
13821382
{ haveI : finite_measure μ := ⟨hμ⟩,
13831383
calc ∫ x : α, c ∂μ = (simple_func.const α c).integral μ :
13841384
((simple_func.const α c).integral_eq_integral (integrable_const _)).symm
@@ -1449,7 +1449,7 @@ end
14491449
norm_le_zero_iff.1 $ le_trans (norm_integral_le_lintegral_norm f) $ by simp
14501450

14511451
private lemma integral_smul_measure_aux {f : α → E} {c : ℝ≥0∞}
1452-
(h0 : 0 < c) (hc : c < ) (fmeas : measurable f) (hfi : integrable f μ) :
1452+
(h0 : 0 < c) (hc : c < ) (fmeas : measurable f) (hfi : integrable f μ) :
14531453
∫ x, f x ∂(c • μ) = c.to_real • ∫ x, f x ∂μ :=
14541454
begin
14551455
refine tendsto_nhds_unique _
@@ -1469,26 +1469,26 @@ begin
14691469
by_cases hfm : ae_measurable f μ, swap,
14701470
{ have : ¬ (ae_measurable f (c • μ)), by simpa [ne_of_gt h0] using hfm,
14711471
simp [integral_non_ae_measurable, hfm, this] },
1472-
-- `c = `
1473-
rcases (le_top : c ≤ ).eq_or_lt with rfl|hc,
1472+
-- `c = `
1473+
rcases (le_top : c ≤ ).eq_or_lt with rfl|hc,
14741474
{ rw [ennreal.top_to_real, zero_smul],
14751475
by_cases hf : f =ᵐ[μ] 0,
1476-
{ have : f =ᵐ[ • μ] 0 := ae_smul_measure hf ,
1476+
{ have : f =ᵐ[ • μ] 0 := ae_smul_measure hf ,
14771477
exact integral_eq_zero_of_ae this },
14781478
{ apply integral_undef,
1479-
rw [integrable, has_finite_integral, iff_true_intro (hfm.smul_measure ), true_and,
1479+
rw [integrable, has_finite_integral, iff_true_intro (hfm.smul_measure ), true_and,
14801480
lintegral_smul_measure, top_mul, if_neg],
14811481
{ apply lt_irrefl },
14821482
{ rw [lintegral_eq_zero_iff' hfm.ennnorm],
14831483
refine λ h, hf (h.mono $ λ x, _),
14841484
simp } } },
1485-
-- `f` is not integrable and `0 < c < `
1485+
-- `f` is not integrable and `0 < c < `
14861486
by_cases hfi : integrable f μ, swap,
14871487
{ rw [integral_undef hfi, smul_zero],
14881488
refine integral_undef (mt (λ h, _) hfi),
14891489
convert h.smul_measure (ennreal.inv_lt_top.2 h0),
14901490
rw [smul_smul, ennreal.inv_mul_cancel (ne_of_gt h0) (ne_of_lt hc), one_smul] },
1491-
-- Main case: `0 < c < `, `f` is almost everywhere measurable and integrable
1491+
-- Main case: `0 < c < `, `f` is almost everywhere measurable and integrable
14921492
let g := hfm.mk f,
14931493
calc ∫ x, f x ∂(c • μ) = ∫ x, g x ∂(c • μ) : integral_congr_ae $ ae_smul_measure hfm.ae_eq_mk c
14941494
... = c.to_real • ∫ x, g x ∂μ :

src/measure_theory/borel_space.lean

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1089,7 +1089,7 @@ lemma measurable.ennreal_of_real {f : α → ℝ} (hf : measurable f) :
10891089
ennreal.continuous_of_real.measurable.comp hf
10901090

10911091
/-- The set of finite `ℝ≥0∞` numbers is `measurable_equiv` to `ℝ≥0`. -/
1092-
def measurable_equiv.ennreal_equiv_nnreal : {r : ℝ≥0∞ | r ≠ } ≃ᵐ ℝ≥0 :=
1092+
def measurable_equiv.ennreal_equiv_nnreal : {r : ℝ≥0∞ | r ≠ } ≃ᵐ ℝ≥0 :=
10931093
ennreal.ne_top_homeomorph_nnreal.to_measurable_equiv
10941094

10951095
namespace ennreal
@@ -1099,20 +1099,20 @@ measurable_id.ennreal_coe
10991099

11001100
lemma measurable_of_measurable_nnreal {f : ℝ≥0∞ → α}
11011101
(h : measurable (λ p : ℝ≥0, f p)) : measurable f :=
1102-
measurable_of_measurable_on_compl_singleton
1102+
measurable_of_measurable_on_compl_singleton
11031103
(measurable_equiv.ennreal_equiv_nnreal.symm.measurable_coe_iff.1 h)
11041104

11051105
/-- `ℝ≥0∞` is `measurable_equiv` to `ℝ≥0 ⊕ unit`. -/
11061106
def ennreal_equiv_sum : ℝ≥0∞ ≃ᵐ ℝ≥0 ⊕ unit :=
11071107
{ measurable_to_fun := measurable_of_measurable_nnreal measurable_inl,
1108-
measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ℝ≥0∞ unit _ _ ),
1108+
measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ℝ≥0∞ unit _ _ ),
11091109
.. equiv.option_equiv_sum_punit ℝ≥0 }
11101110

11111111
open function (uncurry)
11121112

11131113
lemma measurable_of_measurable_nnreal_prod [measurable_space β] [measurable_space γ]
11141114
{f : ℝ≥0∞ × β → γ} (H₁ : measurable (λ p : ℝ≥0 × β, f (p.1, p.2)))
1115-
(H₂ : measurable (λ x, f (, x))) :
1115+
(H₂ : measurable (λ x, f (, x))) :
11161116
measurable f :=
11171117
let e : ℝ≥0∞ × β ≃ᵐ ℝ≥0 × β ⊕ unit × β :=
11181118
(ennreal_equiv_sum.prod_congr (measurable_equiv.refl β)).trans
@@ -1121,7 +1121,7 @@ e.symm.measurable_coe_iff.1 $ measurable_sum H₁ (H₂.comp measurable_id.snd)
11211121

11221122
lemma measurable_of_measurable_nnreal_nnreal [measurable_space β]
11231123
{f : ℝ≥0∞ × ℝ≥0∞ → β} (h₁ : measurable (λ p : ℝ≥0 × ℝ≥0, f (p.1, p.2)))
1124-
(h₂ : measurable (λ r : ℝ≥0, f (, r))) (h₃ : measurable (λ r : ℝ≥0, f (r, ))) :
1124+
(h₂ : measurable (λ r : ℝ≥0, f (, r))) (h₃ : measurable (λ r : ℝ≥0, f (r, ))) :
11251125
measurable f :=
11261126
measurable_of_measurable_nnreal_prod
11271127
(measurable_swap_iff.1 $ measurable_of_measurable_nnreal_prod (h₁.comp measurable_swap) h₃)
@@ -1386,7 +1386,7 @@ variables [topological_space α] {μ : measure α}
13861386
- it is outer regular: `μ(A) = inf { μ(U) | A ⊆ U open }` for `A` measurable;
13871387
- it is inner regular: `μ(U) = sup { μ(K) | K ⊆ U compact }` for `U` open. -/
13881388
structure regular (μ : measure α) : Prop :=
1389-
(lt_top_of_is_compact : ∀ {{K : set α}}, is_compact K → μ K < )
1389+
(lt_top_of_is_compact : ∀ {{K : set α}}, is_compact K → μ K < )
13901390
(outer_regular : ∀ {{A : set α}}, measurable_set A →
13911391
(⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), μ U) ≤ μ A)
13921392
(inner_regular : ∀ {{U : set α}}, is_open U →
@@ -1429,7 +1429,7 @@ begin
14291429
rw [map_apply hf hK.measurable_set] }
14301430
end
14311431

1432-
protected lemma smul (hμ : μ.regular) {x : ℝ≥0∞} (hx : x < ) :
1432+
protected lemma smul (hμ : μ.regular) {x : ℝ≥0∞} (hx : x < ) :
14331433
(x • μ).regular :=
14341434
begin
14351435
split,
@@ -1460,11 +1460,11 @@ end measure_theory
14601460

14611461
lemma is_compact.measure_lt_top_of_nhds_within [topological_space α]
14621462
{s : set α} {μ : measure α} (h : is_compact s) (hμ : ∀ x ∈ s, μ.finite_at_filter (𝓝[s] x)) :
1463-
μ s < :=
1463+
μ s < :=
14641464
is_compact.induction_on h (by simp) (λ s t hst ht, (measure_mono hst).trans_lt ht)
14651465
(λ s t hs ht, (measure_union_le s t).trans_lt (ennreal.add_lt_top.2 ⟨hs, ht⟩)) hμ
14661466

14671467
lemma is_compact.measure_lt_top [topological_space α] {s : set α} {μ : measure α}
14681468
[locally_finite_measure μ] (h : is_compact s) :
1469-
μ s < :=
1469+
μ s < :=
14701470
h.measure_lt_top_of_nhds_within $ λ x hx, μ.finite_at_nhds_within _ _

src/measure_theory/content.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ lemma inner_content_mono {μ : compacts G → ℝ≥0∞} ⦃U V : set G⦄ (hU
8484
supr_le_supr $ λ K, supr_le_supr_const $ λ hK, subset.trans hK h2
8585

8686
lemma inner_content_exists_compact {μ : compacts G → ℝ≥0∞} {U : opens G}
87-
(hU : inner_content μ U < ) {ε : ℝ≥0} (hε : 0 < ε) :
87+
(hU : inner_content μ U < ) {ε : ℝ≥0} (hε : 0 < ε) :
8888
∃ K : compacts G, K.1 ⊆ U ∧ inner_content μ U ≤ μ K + ε :=
8989
begin
9090
have h'ε := ennreal.zero_lt_coe_iff.2 hε,
@@ -208,15 +208,15 @@ lemma of_content_interior_compacts (h3 : ∀ (K₁ K₂ : compacts G), K₁.1
208208
le_trans (le_of_eq $ of_content_opens h2 (opens.interior K.1))
209209
(inner_content_le h3 _ _ interior_subset)
210210

211-
lemma of_content_exists_compact {U : opens G} (hU : of_content μ h1 U < ) {ε : ℝ≥0}
211+
lemma of_content_exists_compact {U : opens G} (hU : of_content μ h1 U < ) {ε : ℝ≥0}
212212
(hε : 0 < ε) : ∃ K : compacts G, K.1 ⊆ U ∧ of_content μ h1 U ≤ of_content μ h1 K.1 + ε :=
213213
begin
214214
rw [of_content_opens h2] at hU ⊢,
215215
rcases inner_content_exists_compact hU hε with ⟨K, h1K, h2K⟩,
216216
exact ⟨K, h1K, le_trans h2K $ add_le_add_right (le_of_content_compacts h2 K) _⟩,
217217
end
218218

219-
lemma of_content_exists_open {A : set G} (hA : of_content μ h1 A < ) {ε : ℝ≥0} (hε : 0 < ε) :
219+
lemma of_content_exists_open {A : set G} (hA : of_content μ h1 A < ) {ε : ℝ≥0} (hε : 0 < ε) :
220220
∃ U : opens G, A ⊆ U ∧ of_content μ h1 U ≤ of_content μ h1 A + ε :=
221221
begin
222222
rcases induced_outer_measure_exists_set _ _ inner_content_mono hA hε with ⟨U, hU, h2U, h3U⟩,

src/measure_theory/decomposition.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ private lemma aux {m : ℕ} {γ d : ℝ} (h : γ - (1 / 2) ^ m < d) :
2323
γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d :=
2424
by linarith
2525

26-
lemma hahn_decomposition (hμ : μ univ < ) (hν : ν univ < ) :
26+
lemma hahn_decomposition (hμ : μ univ < ) (hν : ν univ < ) :
2727
∃s, measurable_set s ∧
2828
(∀t, measurable_set t → t ⊆ s → ν t ≤ μ t) ∧
2929
(∀t, measurable_set t → t ⊆ sᶜ → μ t ≤ ν t) :=
@@ -32,8 +32,8 @@ begin
3232
let c : set ℝ := d '' {s | measurable_set s },
3333
let γ : ℝ := Sup c,
3434

35-
have hμ : ∀s, μ s < := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hμ,
36-
have hν : ∀s, ν s < := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hν,
35+
have hμ : ∀s, μ s < := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hμ,
36+
have hν : ∀s, ν s < := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hν,
3737
have to_nnreal_μ : ∀s, ((μ s).to_nnreal : ℝ≥0∞) = μ s :=
3838
(assume s, ennreal.coe_to_nnreal $ ne_top_of_lt $ hμ _),
3939
have to_nnreal_ν : ∀s, ((ν s).to_nnreal : ℝ≥0∞) = ν s :=
@@ -56,7 +56,7 @@ begin
5656
{ assume s hs hm,
5757
refine tendsto.sub _ _;
5858
refine (nnreal.tendsto_coe.2 $
59-
(ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ _).comp $ tendsto_measure_Union hs hm),
59+
(ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ _).comp $ tendsto_measure_Union hs hm),
6060
exact hμ _,
6161
exact hν _ },
6262

@@ -65,7 +65,7 @@ begin
6565
{ assume s hs hm,
6666
refine tendsto.sub _ _;
6767
refine (nnreal.tendsto_coe.2 $
68-
(ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ _).comp $ tendsto_measure_Inter hs hm _),
68+
(ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ _).comp $ tendsto_measure_Inter hs hm _),
6969
exact hμ _,
7070
exact ⟨0, hμ _⟩,
7171
exact hν _,

src/measure_theory/haar_measure.lean

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -470,12 +470,12 @@ lemma haar_outer_measure_le_echaar {K₀ : positive_compacts G} {U : set G} (hU
470470
(outer_measure.of_content_le echaar_sup_le echaar_mono ⟨U, hU⟩ K h : _)
471471

472472
lemma haar_outer_measure_exists_open {K₀ : positive_compacts G} {A : set G}
473-
(hA : haar_outer_measure K₀ A < ) {ε : ℝ≥0} (hε : 0 < ε) :
473+
(hA : haar_outer_measure K₀ A < ) {ε : ℝ≥0} (hε : 0 < ε) :
474474
∃ U : opens G, A ⊆ U ∧ haar_outer_measure K₀ U ≤ haar_outer_measure K₀ A + ε :=
475475
outer_measure.of_content_exists_open echaar_sup_le hA hε
476476

477477
lemma haar_outer_measure_exists_compact {K₀ : positive_compacts G} {U : opens G}
478-
(hU : haar_outer_measure K₀ U < ) {ε : ℝ≥0} (hε : 0 < ε) :
478+
(hU : haar_outer_measure K₀ U < ) {ε : ℝ≥0} (hε : 0 < ε) :
479479
∃ K : compacts G, K.1 ⊆ U ∧ haar_outer_measure K₀ U ≤ haar_outer_measure K₀ K.1 + ε :=
480480
outer_measure.of_content_exists_compact echaar_sup_le hU hε
481481

@@ -502,7 +502,7 @@ lemma haar_outer_measure_self_pos {K₀ : positive_compacts G} :
502502
((haar_outer_measure K₀).mono interior_subset)
503503

504504
lemma haar_outer_measure_lt_top_of_is_compact [locally_compact_space G] {K₀ : positive_compacts G}
505-
{K : set G} (hK : is_compact K) : haar_outer_measure K₀ K < :=
505+
{K : set G} (hK : is_compact K) : haar_outer_measure K₀ K < :=
506506
begin
507507
rcases exists_compact_superset hK with ⟨F, h1F, h2F⟩,
508508
refine ((haar_outer_measure K₀).mono h2F).trans_lt _,
@@ -612,7 +612,7 @@ begin
612612
end
613613

614614
theorem regular_of_left_invariant (hμ : is_mul_left_invariant μ) {K} (hK : is_compact K)
615-
(h2K : (interior K).nonempty) (hμK : μ K < ) : regular μ :=
615+
(h2K : (interior K).nonempty) (hμK : μ K < ) : regular μ :=
616616
begin
617617
rw [haar_measure_unique hμ ⟨K, hK, h2K⟩],
618618
exact regular.smul regular_haar_measure hμK

0 commit comments

Comments
 (0)