feat(measure_theory): image of Lebesgue measure under shift/rescale (#…

…3760)

src/data/finset/lattice.lean

@@ -491,6 +491,14 @@ by simp
 theorem infi_singleton (a : α) (s : α → β) : (⨅ x ∈ ({a} : finset α), s x) = s a :=
 by simp
 
+lemma supr_option_to_finset (o : option α) (f : α → β) :
+  (⨆ x ∈ o.to_finset, f x) = ⨆ x ∈ o, f x :=
+by { congr, ext, rw [option.mem_to_finset] }
+
+lemma infi_option_to_finset (o : option α) (f : α → β) :
+  (⨅ x ∈ o.to_finset, f x) = ⨅ x ∈ o, f x :=
+@supr_option_to_finset _ (order_dual β) _ _ _
+
 variables [decidable_eq α]
 
 theorem supr_union {f : α → β} {s t : finset α} :
@@ -528,6 +536,16 @@ lemma infi_insert_update {x : α} {t : finset α} (f : α → β) {s : β} (hx :
   (⨅ (i ∈ insert x t), update f x s i) = (s ⊓ ⨅ (i ∈ t), f i) :=
 @supr_insert_update α (order_dual β) _ _ _ _ f _ hx
 
+lemma supr_bind (s : finset γ) (t : γ → finset α) (f : α → β) :
+  (⨆ y ∈ s.bind t, f y) = ⨆ (x ∈ s) (y ∈ t x), f y :=
+calc (⨆ y ∈ s.bind t, f y) = ⨆ y (hy : ∃ x ∈ s, y ∈ t x), f y :
+  congr_arg _ $ funext $ λ y, by rw [mem_bind]
+... = _ : by simp only [supr_exists, @supr_comm _ α]
+
+lemma infi_bind (s : finset γ) (t : γ → finset α) (f : α → β) :
+  (⨅ y ∈ s.bind t, f y) = ⨅ (x ∈ s) (y ∈ t x), f y :=
+@supr_bind _ (order_dual β) _ _ _ _ _ _
+
 end lattice
 
 @[simp] theorem bUnion_coe (s : finset α) (t : α → set β) :
@@ -548,6 +566,14 @@ infi_singleton a s
   (⋃ y ∈ s, f ⁻¹' {y}) = f ⁻¹' ↑s :=
 set.bUnion_preimage_singleton f ↑s
 
+@[simp] lemma bUnion_option_to_finset (o : option α) (f : α → set β) :
+  (⋃ x ∈ o.to_finset, f x) = ⋃ x ∈ o, f x :=
+supr_option_to_finset o f
+
+@[simp] lemma bInter_option_to_finset (o : option α) (f : α → set β) :
+  (⋂ x ∈ o.to_finset, f x) = ⋂ x ∈ o, f x :=
+infi_option_to_finset o f
+
 variables [decidable_eq α]
 
 lemma bUnion_union (s t : finset α) (u : α → set β) :
@@ -582,4 +608,12 @@ lemma bInter_insert_update {x : α} {t : finset α} (f : α → set β) {s : set
   (⋂ (i ∈ insert x t), @update _ _ _ f x s i) = (s ∩ ⋂ (i ∈ t), f i) :=
 infi_insert_update f hx
 
+@[simp] lemma bUnion_bind (s : finset γ) (t : γ → finset α) (f : α → set β) :
+  (⋃ y ∈ s.bind t, f y) = ⋃ (x ∈ s) (y ∈ t x), f y :=
+supr_bind s t f
+
+@[simp] lemma bInter_bind (s : finset γ) (t : γ → finset α) (f : α → set β) :
+  (⋂ y ∈ s.bind t, f y) = ⋂ (x ∈ s) (y ∈ t x), f y :=
+infi_bind s t f
+
 end finset

src/data/indicator_function.lean

@@ -311,6 +311,21 @@ lemma indicator_le {β} [canonically_ordered_add_monoid β] {s : set α}
   indicator s f ≤ g :=
 indicator_le' hfg $ λ _ _, zero_le _
 
+lemma indicator_Union_apply {ι β} [complete_lattice β] [has_zero β] (h0 : (⊥:β) = 0)
+  (s : ι → set α) (f : α → β) (x : α) :
+  indicator (⋃ i, s i) f x = ⨆ i, indicator (s i) f x :=
+begin
+  by_cases hx : x ∈ ⋃ i, s i,
+  { rw [indicator_of_mem hx],
+    rw [mem_Union] at hx,
+    refine le_antisymm _ (supr_le $ λ i, indicator_le_self' (λ x hx, h0 ▸ bot_le) x),
+    rcases hx with ⟨i, hi⟩,
+    exact le_supr_of_le i (ge_of_eq $ indicator_of_mem hi _) },
+  { rw [indicator_of_not_mem hx],
+    simp only [mem_Union, not_exists] at hx,
+    simp [hx, ← h0] }
+end
+
 end order
 
 end set

src/data/set/basic.lean

@@ -125,9 +125,13 @@ subtype.forall
 subtype.exists
 
 theorem set_coe.exists' {s : set α} {p : Π x, x ∈ s → Prop} :
-  (∃ x (h : x ∈ s), p x h) ↔ (∃ x : s, p x.1 x.2)  :=
+  (∃ x (h : x ∈ s), p x h) ↔ (∃ x : s, p x x.2)  :=
 (@set_coe.exists _ _ $ λ x, p x.1 x.2).symm
 
+theorem set_coe.forall' {s : set α} {p : Π x, x ∈ s → Prop} :
+  (∀ x (h : x ∈ s), p x h) ↔ (∀ x : s, p x x.2)  :=
+(@set_coe.forall _ _ $ λ x, p x.1 x.2).symm
+
 @[simp] theorem set_coe_cast : ∀ {s t : set α} (H' : s = t) (H : @eq (Type u) s t) (x : s),
   cast H x = ⟨x.1, H' ▸ x.2⟩
 | s _ rfl _ ⟨x, h⟩ := rfl

src/data/set/disjointed.lean

@@ -66,13 +66,18 @@ ext $ λ a, by simp [nat.lt_succ_iff_lt_or_eq, or_and_distrib_right, exists_or_d
 lemma Inter_lt_succ {f : ℕ → set α} {n} : (⋂i < nat.succ n, f i) = f n ∩ (⋂i < n, f i) :=
 ext $ λ a, by simp [nat.lt_succ_iff_lt_or_eq, or_imp_distrib, forall_and_distrib, and_comm]
 
-lemma Union_disjointed {f : ℕ → set α} : (⋃n, disjointed f n) = (⋃n, f n) :=
-subset.antisymm (Union_subset_Union $ assume i, inter_subset_left _ _) $
-  assume x h,
-  have ∃n, x ∈ f n, from mem_Union.mp h,
+lemma subset_Union_disjointed {f : ℕ → set α} {n} : f n ⊆ ⋃ i < n.succ, disjointed f i :=
+λ x hx,
+  have ∃ k, x ∈ f k, from ⟨n, hx⟩,
   have hn : ∀ (i : ℕ), i < nat.find this → x ∉ f i,
     from assume i, nat.find_min this,
-  mem_Union.mpr ⟨nat.find this, nat.find_spec this, by simp; assumption⟩
+  have hlt : nat.find this < n.succ,
+    from (nat.find_min' this hx).trans_lt n.lt_succ_self,
+  mem_bUnion hlt ⟨nat.find_spec this, mem_bInter hn⟩
+
+lemma Union_disjointed {f : ℕ → set α} : (⋃n, disjointed f n) = (⋃n, f n) :=
+subset.antisymm (Union_subset_Union $ assume i, inter_subset_left _ _)
+  (Union_subset $ λ n, subset.trans subset_Union_disjointed (bUnion_subset_Union _ _))
 
 lemma disjointed_induct {f : ℕ → set α} {n : ℕ} {p : set α → Prop}
   (h₁ : p (f n)) (h₂ : ∀t i, p t → p (t \ f i)) :
@@ -95,11 +100,9 @@ have (⋂i (h : i < n + 1), (f i)ᶜ) = (f n)ᶜ,
     (le_infi $ assume i, le_infi $ assume hi, compl_le_compl $ hf $ nat.le_of_succ_le_succ hi),
 by simp [disjointed, this, diff_eq]
 
-lemma Union_disjointed_of_mono {f : ℕ → set α} (hf : monotone f) :
-  ∀ n : ℕ, (⋃i<n.succ, disjointed f i) = f n
-| 0 := by rw [Union_lt_succ]; simp [disjointed, nat.not_lt_zero]
-| (n+1) := by rw [Union_lt_succ,
-  disjointed_of_mono hf, Union_disjointed_of_mono n,
-  diff_union_self, union_eq_self_of_subset_right (hf (nat.le_succ _))]
+lemma Union_disjointed_of_mono {f : ℕ → set α} (hf : monotone f) (n : ℕ) :
+  (⋃i<n.succ, disjointed f i) = f n :=
+subset.antisymm (bUnion_subset $ λ k hk, subset.trans disjointed_subset $ hf $ nat.lt_succ_iff.1 hk)
+  subset_Union_disjointed
 
 end set

src/measure_theory/borel_space.lean

@@ -553,12 +553,34 @@ continuous_edist.measurable2
 end emetric_space
 
 namespace real
-open measurable_space
+open measurable_space measure_theory
 
 lemma borel_eq_generate_from_Ioo_rat :
   borel ℝ = generate_from (⋃(a b : ℚ) (h : a < b), {Ioo a b}) :=
 borel_eq_generate_from_of_subbasis is_topological_basis_Ioo_rat.2.2
 
+lemma measure_ext_Ioo_rat {μ ν : measure ℝ} [locally_finite_measure μ]
+  (h : ∀ a b : ℚ, μ (Ioo a b) = ν (Ioo a b)) : μ = ν :=
+begin
+  refine measure.ext_of_generate_from_of_cover_subset borel_eq_generate_from_Ioo_rat _
+    (subset.refl _) _ _ _ _,
+  { simp only [mem_Union, mem_singleton_iff],
+    rintros _ ⟨a₁, b₁, h₁, rfl⟩ _ ⟨a₂, b₂, h₂, rfl⟩ ne,
+    simp only [Ioo_inter_Ioo, sup_eq_max, inf_eq_min, ← rat.cast_max, ← rat.cast_min, nonempty_Ioo] at ne ⊢,
+    refine ⟨_, _, _, rfl⟩,
+    assumption_mod_cast },
+  { exact countable_Union (λ a, (countable_encodable _).bUnion $ λ _ _, countable_singleton _) },
+  { exact is_topological_basis_Ioo_rat.2.1 },
+  { simp only [mem_Union, mem_singleton_iff],
+    rintros _ ⟨a, b, h, rfl⟩,
+    refine (measure_mono subset_closure).trans_lt _,
+    rw [closure_Ioo],
+    exacts [compact_Icc.finite_measure, rat.cast_lt.2 h] },
+  { simp only [mem_Union, mem_singleton_iff],
+    rintros _ ⟨a, b, hab, rfl⟩,
+    exact h a b }
+end
+
 lemma borel_eq_generate_from_Iio_rat :
   borel ℝ = generate_from (⋃a:ℚ, {Iio a}) :=
 begin

src/measure_theory/integration.lean

@@ -847,6 +847,9 @@ lintegral_mono
 @[simp] lemma lintegral_const (c : ennreal) : ∫⁻ a, c ∂μ = c * μ univ :=
 by rw [← simple_func.const_lintegral, ← simple_func.lintegral_eq_lintegral, simple_func.coe_const]
 
+lemma set_lintegral_one (s) : ∫⁻ a in s, 1 ∂μ = μ s :=
+by rw [lintegral_const, one_mul, measure.restrict_apply_univ]
+
 /-- `∫⁻ a in s, f a ∂μ` is defined as the supremum of integrals of simple functions
 `φ : α →ₛ ennreal` such that `φ ≤ f`. This lemma says that it suffices to take
 functions `φ : α →ₛ ℝ≥0`. -/
@@ -941,7 +944,7 @@ begin
     ... ≤ ∑ r in (rs.map c).range, (⨆n, r * μ ((rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a})) :
       le_of_eq (finset.sum_congr rfl $ assume x hx,
         begin
-          rw [measure_Union_eq_supr_nat _ (mono x), ennreal.mul_supr],
+          rw [measure_Union_eq_supr _ (directed_of_sup $ mono x), ennreal.mul_supr],
           { assume i,
             refine ((rs.map c).is_measurable_preimage _).inter _,
             exact hf i is_measurable_Ici }
@@ -1117,6 +1120,10 @@ lemma lintegral_congr {f g : α → ennreal} (h : ∀ a, f a = g a) :
   (∫⁻ a, f a ∂μ) = (∫⁻ a, g a ∂μ) :=
 by simp only [h]
 
+lemma set_lintegral_congr {f : α → ennreal} {s t : set α} (h : s =ᵐ[μ] t) :
+  ∫⁻ x in s, f x ∂μ = ∫⁻ x in t, f x ∂μ :=
+by rw [restrict_congr_set h]
+
 -- TODO: Need a better way of rewriting inside of a integral
 lemma lintegral_rw₁ {f f' : α → β} (h : f =ᵐ[μ] f') (g : β → ennreal) :
   (∫⁻ a, g (f a) ∂μ) = (∫⁻ a, g (f' a) ∂μ) :=
@@ -1346,12 +1353,9 @@ theorem lintegral_supr_directed [encodable β] {f : β → α → ennreal}
   (hf : ∀b, measurable (f b)) (h_directed : directed (≤) f) :
   ∫⁻ a, ⨆b, f b a ∂μ = ⨆b, ∫⁻ a, f b a ∂μ :=
 begin
-  by_cases hβ : ¬ nonempty β,
-  { have : ∀f : β → ennreal, (⨆(b : β), f b) = 0 :=
-      assume f, supr_eq_bot.2 (assume b, (hβ ⟨b⟩).elim),
-    simp [this] },
-  cases of_not_not hβ with b,
-  haveI iβ : inhabited β := ⟨b⟩, clear hβ b,
+  by_cases hβ : nonempty β, swap,
+  { simp [supr_of_empty hβ] },
+  resetI, inhabit β,
   have : ∀a, (⨆ b, f b a) = (⨆ n, f (h_directed.sequence f n) a),
   { assume a,
     refine le_antisymm (supr_le $ assume b, _) (supr_le $ assume n, le_supr (λn, f n a) _),
@@ -1410,6 +1414,11 @@ begin
     { assume s hs, exact map_apply hg hs } },
 end
 
+lemma set_lintegral_map [measurable_space β] {f : β → ennreal} {g : α → β}
+  {s : set β} (hs : is_measurable s) (hf : measurable f) (hg : measurable g) :
+  ∫⁻ y in s, f y ∂(map g μ) = ∫⁻ x in g ⁻¹' s, f (g x) ∂μ :=
+by rw [restrict_map hg hs, lintegral_map hf hg]
+
 lemma lintegral_dirac (a : α) {f : α → ennreal} (hf : measurable f) :
   ∫⁻ a, f a ∂(dirac a) = f a :=
 by simp [lintegral_congr_ae (eventually_eq_dirac hf)]

src/measure_theory/interval_integral.lean

@@ -322,6 +322,35 @@ lemma integral_const {a b : ℝ} (c : E) : (∫ (x : ℝ) in a..b, c) = (b - a)
 by simp only [integral_const', real.volume_Ioc, ennreal.to_real_of_real', ← neg_sub b,
   max_zero_sub_eq_self]
 
+lemma integral_smul_measure (c : ennreal) :
+  ∫ x in a..b, f x ∂(c • μ) = c.to_real • ∫ x in a..b, f x ∂μ :=
+by simp only [interval_integral, measure.restrict_smul, integral_smul_measure, smul_sub]
+
+lemma integral_comp_add_right (a b c : ℝ) (f : ℝ → E) (hfm : measurable f) :
+  ∫ x in a..b, f (x + c) = ∫ x in a+c..b+c, f x :=
+calc ∫ x in a..b, f (x + c) = ∫ x in a+c..b+c, f x ∂(measure.map (λ x, x + c) volume) :
+  by simp only [interval_integral, set_integral_map is_measurable_Ioc hfm (measurable_add_right _),
+    preimage_add_const_Ioc, add_sub_cancel]
+... = ∫ x in a+c..b+c, f x : by rw [real.map_volume_add_right]
+
+lemma integral_comp_mul_right {c : ℝ} (hc : 0 < c) (a b : ℝ) (f : ℝ → E) (hfm : measurable f) :
+  ∫ x in a..b, f (x * c) = c⁻¹ • ∫ x in a*c..b*c, f x :=
+begin
+  conv_rhs { rw [← real.smul_map_volume_mul_right (ne_of_gt hc)] },
+  rw [integral_smul_measure],
+  simp only [interval_integral, set_integral_map is_measurable_Ioc hfm (measurable_mul_right _),
+    hc, preimage_mul_const_Ioc, mul_div_cancel _ (ne_of_gt hc), abs_of_pos,
+    ennreal.to_real_of_real (le_of_lt hc), inv_smul_smul' (ne_of_gt hc)]
+end
+
+lemma integral_comp_neg (a b : ℝ) (f : ℝ → E) (hfm : measurable f) :
+  ∫ x in a..b, f (-x) = ∫ x in -b..-a, f x :=
+begin
+  conv_rhs { rw ← real.map_volume_neg },
+  simp only [interval_integral, set_integral_map is_measurable_Ioc hfm measurable_neg, neg_preimage,
+    preimage_neg_Ioc, neg_neg, restrict_congr_set Ico_ae_eq_Ioc]
+end
+
 /-!
 ### Integral is an additive function of the interval
 

src/measure_theory/lebesgue_measure.lean

@@ -231,40 +231,73 @@ end measure_theory
 
 open measure_theory
 
-section volume
+namespace real
 
-open_locale interval
+open_locale topological_space
 
-theorem real.volume_val (s) : volume s = lebesgue_outer s := rfl
+theorem volume_val (s) : volume s = lebesgue_outer s := rfl
 
-@[simp]
-lemma real.volume_Ico {a b : ℝ} : volume (Ico a b) = of_real (b - a) := lebesgue_outer_Ico a b
+instance has_no_atoms_volume : has_no_atoms (volume : measure ℝ) :=
+⟨lebesgue_outer_singleton⟩
 
-@[simp]
-lemma real.volume_Icc {a b : ℝ} : volume (Icc a b) = of_real (b - a) := lebesgue_outer_Icc a b
+@[simp] lemma volume_Ico {a b : ℝ} : volume (Ico a b) = of_real (b - a) := lebesgue_outer_Ico a b
 
-@[simp]
-lemma real.volume_Ioo {a b : ℝ} : volume (Ioo a b) = of_real (b - a) := lebesgue_outer_Ioo a b
+@[simp] lemma volume_Icc {a b : ℝ} : volume (Icc a b) = of_real (b - a) := lebesgue_outer_Icc a b
 
-@[simp]
-lemma real.volume_Ioc {a b : ℝ} : volume (Ioc a b) = of_real (b - a) := lebesgue_outer_Ioc a b
+@[simp] lemma volume_Ioo {a b : ℝ} : volume (Ioo a b) = of_real (b - a) := lebesgue_outer_Ioo a b
 
-@[simp]
-lemma real.volume_singleton {a : ℝ} : volume ({a} : set ℝ) = 0 := lebesgue_outer_singleton a
+@[simp] lemma volume_Ioc {a b : ℝ} : volume (Ioc a b) = of_real (b - a) := lebesgue_outer_Ioc a b
 
-@[simp] lemma real.volume_interval {a b : ℝ} : volume [a, b] = of_real (abs (b - a)) :=
-begin
-  rw [interval, real.volume_Icc],
-  congr,
-  exact max_sub_min_eq_abs _ _
-end
+@[simp] lemma volume_singleton {a : ℝ} : volume ({a} : set ℝ) = 0 := lebesgue_outer_singleton a
+
+@[simp] lemma volume_interval {a b : ℝ} : volume (interval a b) = of_real (abs (b - a)) :=
+by rw [interval, volume_Icc, max_sub_min_eq_abs]
 
-instance real.locally_finite_volume : locally_finite_measure (volume : measure ℝ) :=
+instance locally_finite_volume : locally_finite_measure (volume : measure ℝ) :=
 ⟨λ x, ⟨Ioo (x - 1) (x + 1),
   mem_nhds_sets is_open_Ioo ⟨sub_lt_self _ zero_lt_one, lt_add_of_pos_right _ zero_lt_one⟩,
   by simp only [real.volume_Ioo, ennreal.of_real_lt_top]⟩⟩
 
-end volume
+lemma map_volume_add_left (a : ℝ) : measure.map ((+) a) volume = volume :=
+eq.symm $ real.measure_ext_Ioo_rat $ λ p q,
+  by simp [measure.map_apply (measurable_add_left a) is_measurable_Ioo, sub_sub_sub_cancel_right]
+
+lemma map_volume_add_right (a : ℝ) : measure.map (+ a) volume = volume :=
+by simpa only [add_comm] using real.map_volume_add_left a
+
+lemma smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
+  ennreal.of_real (abs a) • measure.map ((*) a) volume = volume :=
+begin
+  refine (real.measure_ext_Ioo_rat $ λ p q, _).symm,
+  cases lt_or_gt_of_ne h with h h,
+  { simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt $ neg_pos.2 h),
+      measure.map_apply (measurable_mul_left a) is_measurable_Ioo, neg_sub_neg,
+      ← neg_mul_eq_neg_mul, preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub,
+      mul_div_cancel' _ (ne_of_lt h)] },
+  { simp only [real.volume_Ioo, measure.smul_apply, ← ennreal.of_real_mul (le_of_lt h),
+      measure.map_apply (measurable_mul_left a) is_measurable_Ioo, preimage_const_mul_Ioo _ _ h,
+      abs_of_pos h, mul_sub, mul_div_cancel' _ (ne_of_gt h)] }
+end
+
+lemma map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
+  measure.map ((*) a) volume = ennreal.of_real (abs a⁻¹) • volume :=
+by conv_rhs { rw [← real.smul_map_volume_mul_left h, smul_smul,
+  ← ennreal.of_real_mul (abs_nonneg _), ← abs_mul, inv_mul_cancel h, abs_one, ennreal.of_real_one,
+  one_smul] }
+
+lemma smul_map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
+  ennreal.of_real (abs a) • measure.map (* a) volume = volume :=
+by simpa only [mul_comm] using real.smul_map_volume_mul_left h
+
+lemma map_volume_mul_right {a : ℝ} (h : a ≠ 0) :
+  measure.map (* a) volume = ennreal.of_real (abs a⁻¹) • volume :=
+by simpa only [mul_comm] using real.map_volume_mul_left h
+
+@[simp] lemma map_volume_neg : measure.map has_neg.neg (volume : measure ℝ) = volume :=
+eq.symm $ real.measure_ext_Ioo_rat $ λ p q,
+  by simp [measure.map_apply measurable_neg is_measurable_Ioo]
+
+end real
 /-
 section vitali