chore(measure_theory/l1_space): make measure argument of integrable optional (#3508)

Other changes:

* a few trivial lemmas;
* fix notation for `∀ᵐ`: now Lean can use it for printing, not only
  for parsing.

Author: urkud

src/measure_theory/bochner_integration.lean

@@ -1267,6 +1267,9 @@ begin
   simpa only [← simple_func.integral_eq_integral, *, simple_func.integral_add_meas] using hμ.add hν
 end
 
+@[simp] lemma integral_zero_meas (f : α → E) : ∫ x, f x ∂0 = 0 :=
+norm_le_zero_iff.1 $ le_trans (norm_integral_le_lintegral_norm f) $ by simp
+
 end properties
 
 mk_simp_attribute integral_simps "Simp set for integral rules."

src/measure_theory/l1_space.lean

@@ -61,8 +61,9 @@ universes u v w
 variables {α : Type u} [measurable_space α] {μ ν : measure α}
 variables {β : Type v} [normed_group β] {γ : Type w} [normed_group γ]
 
-/-- A function is `integrable` if the integral of its pointwise norm is less than infinity. -/
-def integrable (f : α → β) (μ : measure α) : Prop := ∫⁻ a, nnnorm (f a) ∂μ < ⊤
+/-- `integrable f μ` means that the integral `∫⁻ a, ∥f a∥ ∂μ` is finite; `integrable f` means
+`integrable f volume`. -/
+def integrable (f : α → β) (μ : measure α . volume_tac) : Prop := ∫⁻ a, nnnorm (f a) ∂μ < ⊤
 
 lemma integrable_iff_norm (f : α → β) : integrable f μ ↔ ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ < ⊤ :=
 by simp only [integrable, of_real_norm_eq_coe_nnnorm]
@@ -79,13 +80,21 @@ begin
 end,
 by rw [integrable_iff_norm, lintegral_eq]
 
-lemma integrable.congr {f g : α → β} (hf : integrable f μ) (h : f =ᵐ[μ] g) : integrable g μ :=
+lemma integrable.mono {f : α → β} {g : α → γ} (hg : integrable g μ) (h : ∀ᵐ a ∂μ, ∥f a∥ ≤ ∥g a∥) :
+  integrable f μ :=
 begin
-  simp only [integrable],
-  convert hf using 1,
-  exact lintegral_rw₁ (h.symm.fun_comp _) _
+  simp only [integrable_iff_norm] at *,
+  calc ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ ≤ ∫⁻ (a : α), (ennreal.of_real ∥g a∥) ∂μ :
+    lintegral_mono_ae (h.mono $ assume a h, of_real_le_of_real h)
+    ... < ⊤ : hg
 end
 
+lemma integrable.congr {f g : α → β} (hf : integrable f μ) (h : f =ᵐ[μ] g) : integrable g μ :=
+hf.mono $ h.rw (λ a b, ∥b∥ ≤ ∥f a∥) (eventually_le.refl _ $ λ x, ∥f x∥)
+
+lemma integrable_congr {f g : α → β} (h : f =ᵐ[μ] g) : integrable f μ ↔ integrable g μ :=
+⟨λ hf, hf.congr h, λ hg, hg.congr h.symm⟩
+
 lemma integrable_const {c : β} : integrable (λ x : α, c) μ ↔ c = 0 ∨ μ univ < ⊤ :=
 begin
   simp only [integrable, lintegral_const],
@@ -98,18 +107,6 @@ begin
     rwa [ne.def, nnnorm_eq_zero] }
 end
 
-lemma integrable_congr {f g : α → β} (h : f =ᵐ[μ] g) : integrable f μ ↔ integrable g μ :=
-⟨λ hf, hf.congr h, λ hg, hg.congr h.symm⟩
-
-lemma integrable.mono {f : α → β} {g : α → γ} (hg : integrable g μ) (h : ∀ᵐ a ∂μ, ∥f a∥ ≤ ∥g a∥) :
-  integrable f μ :=
-begin
-  simp only [integrable_iff_norm] at *,
-  calc ∫⁻ a, (ennreal.of_real ∥f a∥) ∂μ ≤ ∫⁻ (a : α), (ennreal.of_real ∥g a∥) ∂μ :
-    lintegral_mono_ae (h.mono $ assume a h, of_real_le_of_real h)
-    ... < ⊤ : hg
-end
-
 lemma integrable.mono_meas {f : α → β} (h : integrable f ν) (hμ : μ ≤ ν) :
   integrable f μ :=
 lt_of_le_of_lt (lintegral_mono' hμ (le_refl _)) h

src/measure_theory/measure_space.lean

@@ -1028,9 +1028,9 @@ end measure
 
 variables {α : Type*} {β : Type*} [measurable_space α] {μ : measure α}
 
-notation `∀ᵐ` binders `∂` μ `, ` r:(scoped P, μ.ae.eventually P) := r
-notation f ` =ᵐ[`:50 μ:50 `] `:0 g:50 := f =ᶠ[μ.ae] g
-notation f ` ≤ᵐ[`:50 μ:50 `] `:0 g:50 := f ≤ᶠ[μ.ae] g
+notation `∀ᵐ` binders `∂` μ `, ` r:(scoped P, filter.eventually P (measure.ae μ)) := r
+notation f ` =ᵐ[`:50 μ:50 `] `:0 g:50 := f =ᶠ[measure.ae μ] g
+notation f ` ≤ᵐ[`:50 μ:50 `] `:0 g:50 := f ≤ᶠ[measure.ae μ] g
 
 lemma mem_ae_iff {s : set α} : s ∈ μ.ae ↔ μ sᶜ = 0 := iff.rfl
 
@@ -1304,7 +1304,10 @@ add_decl_doc volume
 section measure_space
 variables {α : Type*} {ι : Type*} [measure_space α] {s₁ s₂ : set α}
 
-notation `∀ᵐ` binders `, ` r:(scoped P, volume.ae.eventually P) := r
+notation `∀ᵐ` binders `, ` r:(scoped P, filter.eventually P (measure.ae volume)) := r
+
+/-- The tactic `exact volume`, to be used in optional (`auto_param`) arguments. -/
+meta def volume_tac : tactic unit := `[exact measure_theory.measure_space.volume]
 
 end measure_space