feat(measure_theory): induction principles in measure theory (#3978)

This commit adds three induction principles for measure theory
* To prove something for arbitrary simple functions
* To prove something for arbitrary measurable functions into `ennreal`
* To prove something for arbitrary measurable + integrable functions.

This also adds some basic lemmas to various files. Not all of them are used in this PR, some will be used by near-future PRs.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/algebra/group/pi.lean

@@ -79,6 +79,19 @@ instance ordered_comm_group [∀ i, ordered_comm_group $ f i] :
   ..pi.comm_group,
   ..pi.partial_order }
 
+section instance_lemmas
+open function
+
+variables {α β γ : Type*}
+
+@[simp, to_additive] lemma const_one [has_one β] : const α (1 : β) = 1 := rfl
+
+@[simp, to_additive] lemma comp_one [has_one β] {f : β → γ} : f ∘ 1 = const α (f 1) := rfl
+
+@[simp, to_additive] lemma one_comp [has_one γ] {f : α → β} : (1 : β → γ) ∘ f = 1 := rfl
+
+end instance_lemmas
+
 variables [decidable_eq I]
 variables [Π i, has_zero (f i)]
 

src/data/indicator_function.lean

@@ -27,9 +27,9 @@ indicator, characteristic
 
 noncomputable theory
 open_locale classical big_operators
+open function
 
-universes u v
-variables {α : Type u} {β : Type v}
+variables {α β γ : Type*}
 
 namespace set
 
@@ -40,6 +40,8 @@ variables [has_zero β] {s t : set α} {f g : α → β} {a : α}
 @[reducible]
 def indicator (s : set α) (f : α → β) : α → β := λ x, if x ∈ s then f x else 0
 
+@[simp] lemma piecewise_eq_indicator {s : set α} : s.piecewise f 0 = s.indicator f := rfl
+
 lemma indicator_apply (s : set α) (f : α → β) (a : α) :
   indicator s f a = if a ∈ s then f a else 0 := rfl
 
@@ -71,14 +73,23 @@ funext $ λx, indicator_of_mem (mem_univ _) f
 funext $ λx, indicator_of_not_mem (not_mem_empty _) f
 
 variable (β)
+
 @[simp] lemma indicator_zero (s : set α) : indicator s (λx, (0:β)) = λx, (0:β) :=
 funext $ λx, by { simp only [indicator], split_ifs, refl, refl }
+
+@[simp] lemma indicator_zero' {s : set α} : s.indicator (0 : α → β) = 0 :=
+indicator_zero β s
+
 variable {β}
 
 lemma indicator_indicator (s t : set α) (f : α → β) : indicator s (indicator t f) = indicator (s ∩ t) f :=
 funext $ λx, by { simp only [indicator], split_ifs, repeat {simp * at * {contextual := tt}} }
 
-lemma indicator_comp_of_zero {γ} [has_zero γ] {g : β → γ} (hg : g 0 = 0) :
+lemma comp_indicator (h : β → γ) (f : α → β) {s : set α} {x : α} :
+  h (s.indicator f x) = s.piecewise (h ∘ f) (const α (h 0)) x :=
+s.comp_piecewise h
+
+lemma indicator_comp_of_zero [has_zero γ] {g : β → γ} (hg : g 0 = 0) :
   indicator s (g ∘ f) = g ∘ (indicator s f) :=
 begin
   funext,
@@ -178,6 +189,24 @@ lemma indicator_smul (s : set α) (r : 𝕜) (f : α → β) :
   indicator s (λ (x : α), r • f x) = λ (x : α), r • indicator s f x :=
 by { simp only [indicator], funext, split_ifs, refl, exact (smul_zero r).symm }
 
+lemma indicator_add_eq_left {f g : α → β} (h : univ ⊆ f ⁻¹' {0} ∪ g ⁻¹' {0}) :
+  (f ⁻¹' {0})ᶜ.indicator (f + g) = f :=
+begin
+  ext x, by_cases hx : x ∈ (f ⁻¹' {0})ᶜ,
+  { have : g x = 0, { simp at hx, specialize h (mem_univ x), simpa [hx] using h },
+    simp [hx, this] },
+  { simp * at * }
+end
+
+lemma indicator_add_eq_right {f g : α → β} (h : univ ⊆ f ⁻¹' {0} ∪ g ⁻¹' {0}) :
+  (g ⁻¹' {0})ᶜ.indicator (f + g) = g :=
+begin
+  ext x, by_cases hx : x ∈ (g ⁻¹' {0})ᶜ,
+  { have : f x = 0, { simp at hx, specialize h (mem_univ x), simpa [hx] using h },
+    simp [hx, this] },
+  { simp * at * }
+end
+
 end add_monoid
 
 section add_group

src/data/list/indexes.lean

@@ -147,7 +147,7 @@ theorem mmap_with_index'_aux_eq_mmap_with_index_aux {α} (f : ℕ → α → m p
   mmap_with_index'_aux f start as =
   mmap_with_index_aux f start as *> pure punit.star :=
 by induction as generalizing start;
-    simp [mmap_with_index'_aux, mmap_with_index_aux, *, seq_right_eq, const]
+    simp [mmap_with_index'_aux, mmap_with_index_aux, *, seq_right_eq, const, -comp_const]
       with functor_norm
 
 theorem mmap_with_index'_eq_mmap_with_index {α} (f : ℕ → α → m punit) (as : list α) :

src/data/real/ennreal.lean

@@ -182,6 +182,8 @@ end
 protected lemma lt_top_iff_ne_top : a < ∞ ↔ a ≠ ∞ := lt_top_iff_ne_top
 protected lemma bot_lt_iff_ne_bot : 0 < a ↔ a ≠ 0 := bot_lt_iff_ne_bot
 
+lemma not_lt_top {x : ennreal} : ¬ x < ∞ ↔ x = ∞ := by rw [lt_top_iff_ne_top, not_not]
+
 lemma add_ne_top : a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞ :=
 by simpa only [lt_top_iff_ne_top] using add_lt_top
 
@@ -197,16 +199,28 @@ lemma top_pow {n:ℕ} (h : 0 < n) : ∞^n = ∞ :=
 nat.le_induction (pow_one _) (λ m hm hm', by rw [pow_succ, hm', top_mul_top])
   _ (nat.succ_le_of_lt h)
 
-lemma mul_eq_top {a b : ennreal} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
+lemma mul_eq_top : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
 with_top.mul_eq_top_iff
 
-lemma mul_ne_top {a b : ennreal} : a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞ :=
+lemma mul_ne_top : a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞ :=
 by simp [(≠), mul_eq_top] {contextual := tt}
 
-lemma mul_lt_top {a b : ennreal}  : a < ⊤ → b < ⊤ → a * b < ⊤ :=
+lemma mul_lt_top  : a < ⊤ → b < ⊤ → a * b < ⊤ :=
 by simpa only [ennreal.lt_top_iff_ne_top] using mul_ne_top
 
-@[simp] lemma mul_pos {a b : ennreal} : 0 < a * b ↔ 0 < a ∧ 0 < b :=
+lemma ne_top_of_mul_ne_top_left (h : a * b ≠ ⊤) (hb : b ≠ 0) : a ≠ ⊤ :=
+by { simp [mul_eq_top, hb, not_or_distrib] at h ⊢, exact h.2 }
+
+lemma ne_top_of_mul_ne_top_right (h : a * b ≠ ⊤) (ha : a ≠ 0) : b ≠ ⊤ :=
+ne_top_of_mul_ne_top_left (by rwa [mul_comm]) ha
+
+lemma lt_top_of_mul_lt_top_left (h : a * b < ⊤) (hb : b ≠ 0) : a < ⊤ :=
+by { rw [ennreal.lt_top_iff_ne_top] at h ⊢, exact ne_top_of_mul_ne_top_left h hb }
+
+lemma lt_top_of_mul_lt_top_right (h : a * b < ⊤) (ha : a ≠ 0) : b < ⊤ :=
+lt_top_of_mul_lt_top_left (by rwa [mul_comm]) ha
+
+@[simp] lemma mul_pos : 0 < a * b ↔ 0 < a ∧ 0 < b :=
 by simp only [zero_lt_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
 
 lemma pow_eq_top : ∀ n:ℕ, a^n=∞ → a=∞
@@ -936,10 +950,10 @@ by rw [← two_mul, ← div_def, div_self two_ne_zero two_ne_top]
 lemma add_halves (a : ennreal) : a / 2 + a / 2 = a :=
 by rw [div_def, ← mul_add, inv_two_add_inv_two, mul_one]
 
-@[simp] lemma div_zero_iff {a b : ennreal} : a / b = 0 ↔ a = 0 ∨ b = ⊤ :=
+@[simp] lemma div_zero_iff : a / b = 0 ↔ a = 0 ∨ b = ⊤ :=
 by simp [div_def, mul_eq_zero]
 
-@[simp] lemma div_pos_iff {a b : ennreal} : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤ :=
+@[simp] lemma div_pos_iff : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤ :=
 by simp [zero_lt_iff_ne_zero, not_or_distrib]
 
 lemma half_pos {a : ennreal} (h : 0 < a) : 0 < a / 2 :=
@@ -1113,7 +1127,7 @@ end
 @[simp] lemma to_real_top_mul (a : ennreal) : ennreal.to_real (⊤ * a) = 0 :=
 by { rw mul_comm, exact to_real_mul_top _ }
 
-lemma to_real_eq_to_real {a b : ennreal} (ha : a < ⊤) (hb : b < ⊤) :
+lemma to_real_eq_to_real (ha : a < ⊤) (hb : b < ⊤) :
   ennreal.to_real a = ennreal.to_real b ↔ a = b :=
 begin
   rw ennreal.lt_top_iff_ne_top at *,
@@ -1124,7 +1138,7 @@ begin
   { assume h, rw h }
 end
 
-lemma to_real_mul_to_real {a b : ennreal} :
+lemma to_real_mul_to_real :
   (ennreal.to_real a) * (ennreal.to_real b) = ennreal.to_real (a * b) :=
 begin
   by_cases ha : a = ⊤,

src/data/set/basic.lean

@@ -143,6 +143,9 @@ end set_coe
 /-- See also `subtype.prop` -/
 lemma subtype.mem {α : Type*} {s : set α} (p : s) : (p : α) ∈ s := p.prop
 
+lemma eq.subset {α} {s t : set α} : s = t → s ⊆ t :=
+by { rintro rfl x hx, exact hx }
+
 namespace set
 
 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a : α} {s t : set α}
@@ -922,6 +925,10 @@ ext $ assume x, ⟨assume ⟨hx, _⟩, hx, assume h, ⟨h, not_false⟩⟩
 theorem diff_diff {u : set α} : s \ t \ u = s \ (t ∪ u) :=
 ext $ by simp [not_or_distrib, and.comm, and.left_comm]
 
+-- the following statement contains parentheses to help the reader
+lemma diff_diff_comm {s t u : set α} : (s \ t) \ u = (s \ u) \ t :=
+by simp_rw [diff_diff, union_comm]
+
 lemma diff_subset_iff {s t u : set α} : s \ t ⊆ u ↔ s ⊆ t ∪ u :=
 ⟨assume h x xs, classical.by_cases or.inl (assume nxt, or.inr (h ⟨xs, nxt⟩)),
  assume h x ⟨xs, nxt⟩, or.resolve_left (h xs) nxt⟩
@@ -1327,7 +1334,7 @@ lemma image_preimage_inter (f : α → β) (s : set α) (t : set β) :
   f '' (f ⁻¹' t ∩ s) = t ∩ f '' s :=
 by simp only [inter_comm, image_inter_preimage]
 
-lemma image_compl_preimage {f : α → β} {s : set α} {t : set β} : f '' (s \ f ⁻¹' t) = f '' s \ t :=
+lemma image_diff_preimage {f : α → β} {s : set α} {t : set β} : f '' (s \ f ⁻¹' t) = f '' s \ t :=
 by simp_rw [diff_eq, ← preimage_compl, image_inter_preimage]
 
 theorem compl_image : image (compl : set α → set α) = preimage compl :=
@@ -1490,6 +1497,9 @@ lemma image_preimage_eq_of_subset {f : α → β} {s : set β} (hs : s ⊆ range
   f '' (f ⁻¹' s) = s :=
 by rw [image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]
 
+lemma image_preimage_eq_iff {f : α → β} {s : set β} : f '' (f ⁻¹' s) = s ↔ s ⊆ range f :=
+⟨by { intro h, rw [← h], apply image_subset_range }, image_preimage_eq_of_subset⟩
+
 lemma preimage_subset_preimage_iff {s t : set α} {f : β → α} (hs : s ⊆ range f) :
   f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t :=
 begin
@@ -1538,6 +1548,12 @@ theorem preimage_singleton_eq_empty {f : α → β} {y : β} :
   f ⁻¹' {y} = ∅ ↔ y ∉ range f :=
 not_nonempty_iff_eq_empty.symm.trans $ not_congr preimage_singleton_nonempty
 
+lemma range_subset_singleton {f : ι → α} {x : α} : range f ⊆ {x} ↔ f = const ι x :=
+by simp [range_subset_iff, funext_iff, mem_singleton]
+
+lemma image_compl_preimage {f : α → β} {s : set β} : f '' ((f ⁻¹' s)ᶜ) = range f \ s :=
+by rw [compl_eq_univ_diff, image_diff_preimage, image_univ]
+
 @[simp] theorem range_sigma_mk {β : α → Type*} (a : α) :
   range (sigma.mk a : β a → Σ a, β a) = sigma.fst ⁻¹' {a} :=
 begin

src/data/set/function.lean

@@ -480,6 +480,8 @@ by simp [piecewise]
 
 variable [∀j, decidable (j ∈ s)]
 
+instance compl.decidable_mem (j : α) : decidable (j ∈ sᶜ) := not.decidable
+
 lemma piecewise_insert [decidable_eq α] (j : α) [∀i, decidable (i ∈ insert j s)] :
   (insert j s).piecewise f g = function.update (s.piecewise f g) j (f j) :=
 begin
@@ -521,6 +523,20 @@ lemma piecewise_preimage (f g : α → β) (t) :
   s.piecewise f g ⁻¹' t = s ∩ f ⁻¹' t ∪ sᶜ ∩ g ⁻¹' t :=
 ext $ λ x, by by_cases x ∈ s; simp *
 
+lemma comp_piecewise (h : β → γ) {f g : α → β} {x : α} :
+  h (s.piecewise f g x) = s.piecewise (h ∘ f) (h ∘ g) x :=
+by by_cases hx : x ∈ s; simp [hx]
+
+@[simp] lemma piecewise_same : s.piecewise f f = f :=
+by { ext x, by_cases hx : x ∈ s; simp [hx] }
+
+lemma range_piecewise (f g : α → β) : range (s.piecewise f g) = f '' s ∪ g '' sᶜ :=
+begin
+  ext y, split,
+  { rintro ⟨x, rfl⟩, by_cases h : x ∈ s;[left, right]; use x; simp [h] },
+  { rintro (⟨x, hx, rfl⟩|⟨x, hx, rfl⟩); use x; simp * at * }
+end
+
 end set
 
 namespace function

src/logic/function/basic.lean

@@ -15,14 +15,23 @@ universes u v w
 namespace function
 
 section
-variables {α : Sort u} {β : Sort v} {f : α → β}
+variables {α β γ : Sort*} {f : α → β}
 
 /-- Evaluate a function at an argument. Useful if you want to talk about the partially applied
   `function.eval x : (Π x, β x) → β x`. -/
 @[reducible] def eval {β : α → Sort*} (x : α) (f : Π x, β x) : β x := f x
 
 @[simp] lemma eval_apply {β : α → Sort*} (x : α) (f : Π x, β x) : eval x f = f x := rfl
 
+lemma comp_apply {α : Sort u} {β : Sort v} {φ : Sort w} (f : β → φ) (g : α → β) (a : α) :
+  (f ∘ g) a = f (g a) := rfl
+
+@[simp] lemma const_apply {y : β} {x : α} : const α y x = y := rfl
+
+@[simp] lemma const_comp {f : α → β} {c : γ} : const β c ∘ f = const α c := rfl
+
+@[simp] lemma comp_const {f : β → γ} {b : β} : f ∘ const α b = const α (f b) := rfl
+
 lemma hfunext {α α': Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : Πa, β a} {f' : Πa, β' a}
   (hα : α = α') (h : ∀a a', a == a' → f a == f' a') : f == f' :=
 begin
@@ -40,9 +49,6 @@ end
 lemma funext_iff {β : α → Sort*} {f₁ f₂ : Π (x : α), β x} : f₁ = f₂ ↔ (∀a, f₁ a = f₂ a) :=
 iff.intro (assume h a, h ▸ rfl) funext
 
-lemma comp_apply {α : Sort u} {β : Sort v} {φ : Sort w} (f : β → φ) (g : α → β) (a : α) :
-  (f ∘ g) a = f (g a) := rfl
-
 @[simp] theorem injective.eq_iff (I : injective f) {a b : α} :
   f a = f b ↔ a = b :=
 ⟨@I _ _, congr_arg f⟩
@@ -66,10 +72,10 @@ the domain `α` also has decidable equality. -/
 def injective.decidable_eq [decidable_eq β] (I : injective f) : decidable_eq α :=
 λ a b, decidable_of_iff _ I.eq_iff
 
-lemma injective.of_comp {γ : Sort w} {g : γ → α} (I : injective (f ∘ g)) : injective g :=
+lemma injective.of_comp {g : γ → α} (I : injective (f ∘ g)) : injective g :=
 λ x y h, I $ show f (g x) = f (g y), from congr_arg f h
 
-lemma surjective.of_comp {γ : Sort w} {g : γ → α} (S : surjective (f ∘ g)) : surjective f :=
+lemma surjective.of_comp {g : γ → α} (S : surjective (f ∘ g)) : surjective f :=
 λ y, let ⟨x, h⟩ := S y in ⟨g x, h⟩
 
 instance decidable_eq_pfun (p : Prop) [decidable p] (α : p → Type*)
@@ -140,11 +146,11 @@ funext h
 theorem right_inverse_iff_comp {f : α → β} {g : β → α} : right_inverse f g ↔ g ∘ f = id :=
 ⟨right_inverse.comp_eq_id, congr_fun⟩
 
-theorem left_inverse.comp {γ} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
+theorem left_inverse.comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
   (hf : left_inverse f g) (hh : left_inverse h i) : left_inverse (h ∘ f) (g ∘ i) :=
 assume a, show h (f (g (i a))) = a, by rw [hf (i a), hh a]
 
-theorem right_inverse.comp {γ} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
+theorem right_inverse.comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
   (hf : right_inverse f g) (hh : right_inverse h i) : right_inverse (h ∘ f) (g ∘ i) :=
 left_inverse.comp hh hf
 
@@ -346,7 +352,7 @@ lemma uncurry_def {α β γ} (f : α → β → γ) : uncurry f = (λp, f p.1 p.
 rfl
 
 section bicomp
-variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ε : Type*}
+variables {α β γ δ ε : Type*}
 
 /-- Compose a binary function `f` with a pair of unary functions `g` and `h`.
 If both arguments of `f` have the same type and `g = h`, then `bicompl f g g = f on g`. -/

src/measure_theory/bochner_integration.lean

@@ -69,9 +69,13 @@ The Bochner integral is defined following these steps:
 Some tips on how to prove a proposition if the API for the Bochner integral is not enough so that
 you need to unfold the definition of the Bochner integral and go back to simple functions.
 
+One method is to use the theorem `integrable.induction` in the file `set_integral`, which allows
+you to prove something for an arbitrary measurable + integrable function.
+
+Another method is using the following steps.
 See `integral_eq_lintegral_max_sub_lintegral_min` for a complicated example, which proves that
 `∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, with the first integral sign being the Bochner integral of a real-valued
-function f : α → ℝ, and second and third integral sign being the integral on ennreal-valued
+function `f : α → ℝ`, and second and third integral sign being the integral on ennreal-valued
 functions (called `lintegral`). The proof of `integral_eq_lintegral_max_sub_lintegral_min` is
 scattered in sections with the name `pos_part`.