From ed2cc4bc22fbb7d226db37fc4d3dedde964d49dd Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 12 Dec 2023 16:10:46 +0100 Subject: [PATCH] chore: tidy various files --- Mathlib/MeasureTheory/Function/Jacobian.lean | 81 +++++------ .../MeasureTheory/Integral/SetIntegral.lean | 134 +++++++++--------- 2 files changed, 101 insertions(+), 114 deletions(-) diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean index 86f943d7538b7..93713ad8606bd 100644 --- a/Mathlib/MeasureTheory/Function/Jacobian.lean +++ b/Mathlib/MeasureTheory/Function/Jacobian.lean @@ -218,11 +218,9 @@ theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt [SecondCou obtain ⟨F, hF⟩ : ∃ F : ℕ → ℕ × T × ℕ, Function.Surjective F := by haveI : Encodable T := T_count.toEncodable have : Nonempty T := by - rcases eq_empty_or_nonempty T with (rfl | hT) - · rcases hs with ⟨x, xs⟩ - rcases s_subset x xs with ⟨n, z, _⟩ - exact False.elim z.2 - · exact hT.coe_sort + rcases hs with ⟨x, xs⟩ + rcases s_subset x xs with ⟨n, z, _⟩ + exact ⟨z⟩ inhabit ↥T exact ⟨_, Encodable.surjective_decode_iget (ℕ × T × ℕ)⟩ -- these sets `t q = K n z p` will do @@ -321,19 +319,20 @@ theorem addHaar_image_le_mul_of_det_lt (A : E →L[ℝ] E) {m : ℝ≥0} filter_upwards [this] -- fix a function `f` which is close enough to `A`. intro δ hδ s f hf + simp only [mem_Iio, ← NNReal.coe_lt_coe, NNReal.coe_mk] at hδ -- This function expands the volume of any ball by at most `m` have I : ∀ x r, x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ m * μ (closedBall x r) := by intro x r xs r0 have K : f '' (s ∩ closedBall x r) ⊆ A '' closedBall 0 r + closedBall (f x) (ε * r) := by rintro y ⟨z, ⟨zs, zr⟩, rfl⟩ + rw [mem_closedBall_iff_norm] at zr apply Set.mem_add.2 ⟨A (z - x), _, f z - f x - A (z - x) + f x, _, _⟩ · apply mem_image_of_mem simpa only [dist_eq_norm, mem_closedBall, mem_closedBall_zero_iff, sub_zero] using zr · rw [mem_closedBall_iff_norm, add_sub_cancel] calc ‖f z - f x - A (z - x)‖ ≤ δ * ‖z - x‖ := hf _ zs _ xs - _ ≤ ε * r := - mul_le_mul (le_of_lt hδ) (mem_closedBall_iff_norm.1 zr) (norm_nonneg _) εpos.le + _ ≤ ε * r := by gcongr · simp only [map_sub, Pi.sub_apply] abel have : @@ -356,7 +355,7 @@ theorem addHaar_image_le_mul_of_det_lt (A : E →L[ℝ] E) {m : ℝ≥0} -- measure of `f '' s` is at most `m * (μ s + a)` for any positive `a`. have J : ∀ᶠ a in 𝓝[>] (0 : ℝ≥0∞), μ (f '' s) ≤ m * (μ s + a) := by filter_upwards [self_mem_nhdsWithin] with a ha - change 0 < a at ha + rw [mem_Ioi] at ha obtain ⟨t, r, t_count, ts, rpos, st, μt⟩ : ∃ (t : Set E) (r : E → ℝ), t.Countable ∧ @@ -532,21 +531,19 @@ theorem _root_.ApproximatesLinearOn.norm_fderiv_sub_le {A : E →L[ℝ] E} {δ : ring _ ≤ r * (δ + ε) * (‖z‖ + ε) := mul_le_mul_of_nonneg_left norm_a (mul_nonneg rpos.le (add_nonneg δ.2 εpos.le)) - show ‖(f' x - A) z‖ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε; - exact - calc - ‖(f' x - A) z‖ = ‖(f' x - A) a + (f' x - A) (z - a)‖ := by - congr 1 - simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply] - abel - _ ≤ ‖(f' x - A) a‖ + ‖(f' x - A) (z - a)‖ := (norm_add_le _ _) - _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ := by - apply add_le_add - · rw [mul_assoc] at I; exact (mul_le_mul_left rpos).1 I - · apply ContinuousLinearMap.le_opNorm - _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε := - add_le_add le_rfl - (mul_le_mul_of_nonneg_left (mem_closedBall_iff_norm'.1 az) (norm_nonneg _)) + calc + ‖(f' x - A) z‖ = ‖(f' x - A) a + (f' x - A) (z - a)‖ := by + congr 1 + simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply] + abel + _ ≤ ‖(f' x - A) a‖ + ‖(f' x - A) (z - a)‖ := (norm_add_le _ _) + _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ := by + apply add_le_add + · rw [mul_assoc] at I; exact (mul_le_mul_left rpos).1 I + · apply ContinuousLinearMap.le_opNorm + _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε := + add_le_add le_rfl + (mul_le_mul_of_nonneg_left (mem_closedBall_iff_norm'.1 az) (norm_nonneg _)) #align approximates_linear_on.norm_fderiv_sub_le ApproximatesLinearOn.norm_fderiv_sub_le /-! @@ -743,8 +740,8 @@ theorem aemeasurable_fderivWithin (hs : MeasurableSet s) (hf' x hx.1).mono (inter_subset_left _ _) -- moreover, `g x` is equal to `A n` there. have E₂ : ∀ᵐ x : E ∂μ.restrict (s ∩ t n), g x = A n := by - suffices H : ∀ᵐ x : E ∂μ.restrict (t n), g x = A n - exact ae_mono (restrict_mono (inter_subset_right _ _) le_rfl) H + suffices H : ∀ᵐ x : E ∂μ.restrict (t n), g x = A n from + ae_mono (restrict_mono (inter_subset_right _ _) le_rfl) H filter_upwards [ae_restrict_mem (t_meas n)] exact hg n -- putting these two properties together gives the conclusion. @@ -895,7 +892,8 @@ theorem addHaar_image_le_lintegral_abs_det_fderiv_aux2 (hs : MeasurableSet s) (h simp only [add_zero, zero_mul, mul_zero, ENNReal.coe_zero] at this apply ge_of_tendsto this filter_upwards [self_mem_nhdsWithin] - rintro ε (εpos : 0 < ε) + intro ε εpos + rw [mem_Ioi] at εpos exact addHaar_image_le_lintegral_abs_det_fderiv_aux1 μ hs hf' εpos #align measure_theory.add_haar_image_le_lintegral_abs_det_fderiv_aux2 MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2 @@ -1049,7 +1047,8 @@ theorem lintegral_abs_det_fderiv_le_addHaar_image_aux2 (hs : MeasurableSet s) (h simp only [add_zero, zero_mul, mul_zero, ENNReal.coe_zero] at this apply ge_of_tendsto this filter_upwards [self_mem_nhdsWithin] - rintro ε (εpos : 0 < ε) + intro ε εpos + rw [mem_Ioi] at εpos exact lintegral_abs_det_fderiv_le_addHaar_image_aux1 μ hs hf' hf εpos #align measure_theory.lintegral_abs_det_fderiv_le_add_haar_image_aux2 MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2 @@ -1171,11 +1170,10 @@ theorem lintegral_image_eq_lintegral_abs_det_fderiv_mul (hs : MeasurableSet s) ∫⁻ x in f '' s, g x ∂μ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ := by rw [← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf, (measurableEmbedding_of_fderivWithin hs hf' hf).lintegral_map] - have : ∀ x : s, g (s.restrict f x) = (g ∘ f) x := fun x => rfl - simp only [this] + simp only [Set.restrict_apply, ← Function.comp_apply (f := g)] rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs, set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀ _ _ _ hs] - · rfl + · simp only [Pi.mul_apply] · simp only [eventually_true, ENNReal.ofReal_lt_top] · exact aemeasurable_ofReal_abs_det_fderivWithin μ hs hf' #align measure_theory.lintegral_image_eq_lintegral_abs_det_fderiv_mul MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul @@ -1189,14 +1187,10 @@ theorem integrableOn_image_iff_integrableOn_abs_det_fderiv_smul (hs : Measurable IntegrableOn g (f '' s) μ ↔ IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ := by rw [IntegrableOn, ← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf, (measurableEmbedding_of_fderivWithin hs hf' hf).integrable_map_iff] - change Integrable ((g ∘ f) ∘ ((↑) : s → E)) _ ↔ _ - rw [← (MeasurableEmbedding.subtype_coe hs).integrable_map_iff, map_comap_subtype_coe hs] - simp only [ENNReal.ofReal] - rw [restrict_withDensity hs, integrable_withDensity_iff_integrable_coe_smul₀, IntegrableOn] - · rw [iff_iff_eq] - congr 2 with x - rw [Real.coe_toNNReal _ (abs_nonneg _)] - rfl + simp only [Set.restrict_eq, ← Function.comp.assoc, ENNReal.ofReal] + rw [← (MeasurableEmbedding.subtype_coe hs).integrable_map_iff, map_comap_subtype_coe hs, + restrict_withDensity hs, integrable_withDensity_iff_integrable_coe_smul₀] + · simp_rw [IntegrableOn, Real.coe_toNNReal _ (abs_nonneg _), Function.comp_apply] · exact aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf' #align measure_theory.integrable_on_image_iff_integrable_on_abs_det_fderiv_smul MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul @@ -1208,13 +1202,12 @@ theorem integral_image_eq_integral_abs_det_fderiv_smul (hs : MeasurableSet s) ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ := by rw [← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf, (measurableEmbedding_of_fderivWithin hs hf' hf).integral_map] - have : ∀ x : s, g (s.restrict f x) = (g ∘ f) x := fun x => rfl - simp only [this, ENNReal.ofReal] + simp only [Set.restrict_apply, ← Function.comp_apply (f := g), ENNReal.ofReal] rw [← (MeasurableEmbedding.subtype_coe hs).integral_map, map_comap_subtype_coe hs, set_integral_withDensity_eq_set_integral_smul₀ (aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf') _ hs] congr with x - conv_rhs => rw [← Real.coe_toNNReal _ (abs_nonneg (f' x).det)] + rw [NNReal.smul_def, Real.coe_toNNReal _ (abs_nonneg (f' x).det)] #align measure_theory.integral_image_eq_integral_abs_det_fderiv_smul MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul -- Porting note: move this to `Topology.Algebra.Module.Basic` when port is over @@ -1224,9 +1217,9 @@ theorem det_one_smulRight {𝕜 : Type*} [NormedField 𝕜] (v : 𝕜) : ext1 simp only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, Algebra.id.smul_eq_mul, one_mul, ContinuousLinearMap.coe_smul', Pi.smul_apply, mul_one] - rw [this, ContinuousLinearMap.det, ContinuousLinearMap.coe_smul] - rw [show ((1 : 𝕜 →L[𝕜] 𝕜) : 𝕜 →ₗ[𝕜] 𝕜) = LinearMap.id from rfl] - rw [LinearMap.det_smul, FiniteDimensional.finrank_self, LinearMap.det_id, pow_one, mul_one] + rw [this, ContinuousLinearMap.det, ContinuousLinearMap.coe_smul, + ContinuousLinearMap.one_def, ContinuousLinearMap.coe_id, LinearMap.det_smul, + FiniteDimensional.finrank_self, LinearMap.det_id, pow_one, mul_one] #align measure_theory.det_one_smul_right MeasureTheory.det_one_smulRight /-- Integrability in the change of variable formula for differentiable functions (one-variable diff --git a/Mathlib/MeasureTheory/Integral/SetIntegral.lean b/Mathlib/MeasureTheory/Integral/SetIntegral.lean index 5d5db7b109ab9..10500ade0c414 100644 --- a/Mathlib/MeasureTheory/Integral/SetIntegral.lean +++ b/Mathlib/MeasureTheory/Integral/SetIntegral.lean @@ -45,7 +45,7 @@ We provide the following notations for expressing the integral of a function on * `∫ a in s, f a ∂μ` is `MeasureTheory.integral (μ.restrict s) f` * `∫ a in s, f a` is `∫ a in s, f a ∂volume` -Note that the set notations are defined in the file `MeasureTheory/Integral/Bochner.lean`, +Note that the set notations are defined in the file `Mathlib/MeasureTheory/Integral/Bochner.lean`, but we reference them here because all theorems about set integrals are in this file. -/ @@ -95,30 +95,30 @@ theorem set_integral_congr_set_ae (hst : s =ᵐ[μ] t) : ∫ x in s, f x ∂μ = theorem integral_union_ae (hst : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) : - ∫ x in s ∪ t, f x ∂μ = (∫ x in s, f x ∂μ) + ∫ x in t, f x ∂μ := by + ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ + ∫ x in t, f x ∂μ := by simp only [IntegrableOn, Measure.restrict_union₀ hst ht, integral_add_measure hfs hft] #align measure_theory.integral_union_ae MeasureTheory.integral_union_ae theorem integral_union (hst : Disjoint s t) (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) - (hft : IntegrableOn f t μ) : ∫ x in s ∪ t, f x ∂μ = (∫ x in s, f x ∂μ) + ∫ x in t, f x ∂μ := + (hft : IntegrableOn f t μ) : ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ + ∫ x in t, f x ∂μ := integral_union_ae hst.aedisjoint ht.nullMeasurableSet hfs hft #align measure_theory.integral_union MeasureTheory.integral_union theorem integral_diff (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) : - ∫ x in s \ t, f x ∂μ = (∫ x in s, f x ∂μ) - ∫ x in t, f x ∂μ := by + ∫ x in s \ t, f x ∂μ = ∫ x in s, f x ∂μ - ∫ x in t, f x ∂μ := by rw [eq_sub_iff_add_eq, ← integral_union, diff_union_of_subset hts] exacts [disjoint_sdiff_self_left, ht, hfs.mono_set (diff_subset _ _), hfs.mono_set hts] #align measure_theory.integral_diff MeasureTheory.integral_diff theorem integral_inter_add_diff₀ (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ) : - ((∫ x in s ∩ t, f x ∂μ) + ∫ x in s \ t, f x ∂μ) = ∫ x in s, f x ∂μ := by + ∫ x in s ∩ t, f x ∂μ + ∫ x in s \ t, f x ∂μ = ∫ x in s, f x ∂μ := by rw [← Measure.restrict_inter_add_diff₀ s ht, integral_add_measure] · exact Integrable.mono_measure hfs (Measure.restrict_mono (inter_subset_left _ _) le_rfl) · exact Integrable.mono_measure hfs (Measure.restrict_mono (diff_subset _ _) le_rfl) #align measure_theory.integral_inter_add_diff₀ MeasureTheory.integral_inter_add_diff₀ theorem integral_inter_add_diff (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) : - ((∫ x in s ∩ t, f x ∂μ) + ∫ x in s \ t, f x ∂μ) = ∫ x in s, f x ∂μ := + ∫ x in s ∩ t, f x ∂μ + ∫ x in s \ t, f x ∂μ = ∫ x in s, f x ∂μ := integral_inter_add_diff₀ ht.nullMeasurableSet hfs #align measure_theory.integral_inter_add_diff MeasureTheory.integral_inter_add_diff @@ -153,14 +153,14 @@ theorem integral_univ : ∫ x in univ, f x ∂μ = ∫ x, f x ∂μ := by rw [Me #align measure_theory.integral_univ MeasureTheory.integral_univ theorem integral_add_compl₀ (hs : NullMeasurableSet s μ) (hfi : Integrable f μ) : - ((∫ x in s, f x ∂μ) + ∫ x in sᶜ, f x ∂μ) = ∫ x, f x ∂μ := by - rw [← integral_union_ae (@disjoint_compl_right (Set α) _ _).aedisjoint hs.compl hfi.integrableOn - hfi.integrableOn, + ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ := by + rw [ + ← integral_union_ae disjoint_compl_right.aedisjoint hs.compl hfi.integrableOn hfi.integrableOn, union_compl_self, integral_univ] #align measure_theory.integral_add_compl₀ MeasureTheory.integral_add_compl₀ theorem integral_add_compl (hs : MeasurableSet s) (hfi : Integrable f μ) : - ((∫ x in s, f x ∂μ) + ∫ x in sᶜ, f x ∂μ) = ∫ x, f x ∂μ := + ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ := integral_add_compl₀ hs.nullMeasurableSet hfi #align measure_theory.integral_add_compl MeasureTheory.integral_add_compl @@ -169,12 +169,12 @@ over the whole space is equal to `∫ x in s, f x ∂μ` defined as `∫ x, f x theorem integral_indicator (hs : MeasurableSet s) : ∫ x, indicator s f x ∂μ = ∫ x in s, f x ∂μ := by by_cases hfi : IntegrableOn f s μ; swap - · rwa [integral_undef, integral_undef] + · rw [integral_undef hfi, integral_undef] rwa [integrable_indicator_iff hs] calc - ∫ x, indicator s f x ∂μ = (∫ x in s, indicator s f x ∂μ) + ∫ x in sᶜ, indicator s f x ∂μ := + ∫ x, indicator s f x ∂μ = ∫ x in s, indicator s f x ∂μ + ∫ x in sᶜ, indicator s f x ∂μ := (integral_add_compl hs (hfi.integrable_indicator hs)).symm - _ = (∫ x in s, f x ∂μ) + ∫ x in sᶜ, 0 ∂μ := + _ = ∫ x in s, f x ∂μ + ∫ x in sᶜ, 0 ∂μ := (congr_arg₂ (· + ·) (integral_congr_ae (indicator_ae_eq_restrict hs)) (integral_congr_ae (indicator_ae_eq_restrict_compl hs))) _ = ∫ x in s, f x ∂μ := by simp @@ -203,7 +203,7 @@ theorem ofReal_set_integral_one {α : Type*} {_ : MeasurableSpace α} (μ : Meas theorem integral_piecewise [DecidablePred (· ∈ s)] (hs : MeasurableSet s) (hf : IntegrableOn f s μ) (hg : IntegrableOn g sᶜ μ) : - ∫ x, s.piecewise f g x ∂μ = (∫ x in s, f x ∂μ) + ∫ x in sᶜ, g x ∂μ := by + ∫ x, s.piecewise f g x ∂μ = ∫ x in s, f x ∂μ + ∫ x in sᶜ, g x ∂μ := by rw [← Set.indicator_add_compl_eq_piecewise, integral_add' (hf.integrable_indicator hs) (hg.integrable_indicator hs.compl), integral_indicator hs, integral_indicator hs.compl] @@ -213,7 +213,7 @@ theorem tendsto_set_integral_of_monotone {ι : Type*} [Countable ι] [Semilattic {s : ι → Set α} (hsm : ∀ i, MeasurableSet (s i)) (h_mono : Monotone s) (hfi : IntegrableOn f (⋃ n, s n) μ) : Tendsto (fun i => ∫ a in s i, f a ∂μ) atTop (𝓝 (∫ a in ⋃ n, s n, f a ∂μ)) := by - have hfi' : (∫⁻ x in ⋃ n, s n, ‖f x‖₊ ∂μ) < ∞ := hfi.2 + have hfi' : ∫⁻ x in ⋃ n, s n, ‖f x‖₊ ∂μ < ∞ := hfi.2 set S := ⋃ i, s i have hSm : MeasurableSet S := MeasurableSet.iUnion hsm have hsub : ∀ {i}, s i ⊆ S := @(subset_iUnion s) @@ -334,7 +334,7 @@ theorem set_integral_eq_of_subset_of_ae_diff_eq_zero_aux (hts : s ⊆ t) let k := f ⁻¹' {0} have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _) calc - ∫ x in t, f x ∂μ = (∫ x in t ∩ k, f x ∂μ) + ∫ x in t \ k, f x ∂μ := by + ∫ x in t, f x ∂μ = ∫ x in t ∩ k, f x ∂μ + ∫ x in t \ k, f x ∂μ := by rw [integral_inter_add_diff hk h'aux] _ = ∫ x in t \ k, f x ∂μ := by rw [set_integral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]; exact hx.2 @@ -349,7 +349,7 @@ theorem set_integral_eq_of_subset_of_ae_diff_eq_zero_aux (hts : s ⊆ t) · simp only [xs, iff_false_iff] intro xt exact h'x (hx ⟨xt, xs⟩) - _ = (∫ x in s ∩ k, f x ∂μ) + ∫ x in s \ k, f x ∂μ := by + _ = ∫ x in s ∩ k, f x ∂μ + ∫ x in s \ k, f x ∂μ := by have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2 rw [set_integral_eq_zero_of_forall_eq_zero this, zero_add] _ = ∫ x in s, f x ∂μ := by rw [integral_inter_add_diff hk (h'aux.mono hts le_rfl)] @@ -375,7 +375,6 @@ theorem set_integral_eq_of_subset_of_ae_diff_eq_zero (ht : NullMeasurableSet t apply integral_congr_ae apply ae_restrict_of_ae_restrict_of_subset hts exact h.1.ae_eq_mk.symm - #align measure_theory.set_integral_eq_of_subset_of_ae_diff_eq_zero MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero /-- If a function vanishes on `t \ s` with `s ⊆ t`, then its integrals on `s` @@ -407,7 +406,7 @@ theorem set_integral_neg_eq_set_integral_nonpos [LinearOrder E] {f : α → E} (hf : AEStronglyMeasurable f μ) : ∫ x in {x | f x < 0}, f x ∂μ = ∫ x in {x | f x ≤ 0}, f x ∂μ := by have h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0} := by - ext; simp_rw [Set.mem_union, Set.mem_setOf_eq]; exact le_iff_lt_or_eq + simp_rw [le_iff_lt_or_eq, setOf_or] rw [h_union] have B : NullMeasurableSet {x | f x = 0} μ := hf.nullMeasurableSet_eq_fun aestronglyMeasurable_zero @@ -417,19 +416,19 @@ theorem set_integral_neg_eq_set_integral_nonpos [LinearOrder E] {f : α → E} #align measure_theory.set_integral_neg_eq_set_integral_nonpos MeasureTheory.set_integral_neg_eq_set_integral_nonpos theorem integral_norm_eq_pos_sub_neg {f : α → ℝ} (hfi : Integrable f μ) : - ∫ x, ‖f x‖ ∂μ = (∫ x in {x | 0 ≤ f x}, f x ∂μ) - ∫ x in {x | f x ≤ 0}, f x ∂μ := + ∫ x, ‖f x‖ ∂μ = ∫ x in {x | 0 ≤ f x}, f x ∂μ - ∫ x in {x | f x ≤ 0}, f x ∂μ := have h_meas : NullMeasurableSet {x | 0 ≤ f x} μ := aestronglyMeasurable_const.nullMeasurableSet_le hfi.1 calc - ∫ x, ‖f x‖ ∂μ = (∫ x in {x | 0 ≤ f x}, ‖f x‖ ∂μ) + ∫ x in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ := by + ∫ x, ‖f x‖ ∂μ = ∫ x in {x | 0 ≤ f x}, ‖f x‖ ∂μ + ∫ x in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ := by rw [← integral_add_compl₀ h_meas hfi.norm] - _ = (∫ x in {x | 0 ≤ f x}, f x ∂μ) + ∫ x in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ := by + _ = ∫ x in {x | 0 ≤ f x}, f x ∂μ + ∫ x in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ := by congr 1 refine' set_integral_congr₀ h_meas fun x hx => _ dsimp only rw [Real.norm_eq_abs, abs_eq_self.mpr _] exact hx - _ = (∫ x in {x | 0 ≤ f x}, f x ∂μ) - ∫ x in {x | 0 ≤ f x}ᶜ, f x ∂μ := by + _ = ∫ x in {x | 0 ≤ f x}, f x ∂μ - ∫ x in {x | 0 ≤ f x}ᶜ, f x ∂μ := by congr 1 rw [← integral_neg] refine' set_integral_congr₀ h_meas.compl fun x hx => _ @@ -437,8 +436,8 @@ theorem integral_norm_eq_pos_sub_neg {f : α → ℝ} (hfi : Integrable f μ) : rw [Real.norm_eq_abs, abs_eq_neg_self.mpr _] rw [Set.mem_compl_iff, Set.nmem_setOf_iff] at hx linarith - _ = (∫ x in {x | 0 ≤ f x}, f x ∂μ) - ∫ x in {x | f x ≤ 0}, f x ∂μ := by - rw [← set_integral_neg_eq_set_integral_nonpos hfi.1]; congr; ext1 x; simp + _ = ∫ x in {x | 0 ≤ f x}, f x ∂μ - ∫ x in {x | f x ≤ 0}, f x ∂μ := by + rw [← set_integral_neg_eq_set_integral_nonpos hfi.1, compl_setOf]; simp only [not_le] #align measure_theory.integral_norm_eq_pos_sub_neg MeasureTheory.integral_norm_eq_pos_sub_neg theorem set_integral_const [CompleteSpace E] (c : E) : ∫ _ in s, c ∂μ = (μ s).toReal • c := by @@ -447,7 +446,7 @@ theorem set_integral_const [CompleteSpace E] (c : E) : ∫ _ in s, c ∂μ = (μ @[simp] theorem integral_indicator_const [CompleteSpace E] (e : E) ⦃s : Set α⦄ (s_meas : MeasurableSet s) : - (∫ a : α, s.indicator (fun _ : α => e) a ∂μ) = (μ s).toReal • e := by + ∫ a : α, s.indicator (fun _ : α => e) a ∂μ = (μ s).toReal • e := by rw [integral_indicator s_meas, ← set_integral_const] #align measure_theory.integral_indicator_const MeasureTheory.integral_indicator_const @@ -500,7 +499,7 @@ theorem _root_.ClosedEmbedding.set_integral_map [TopologicalSpace α] [BorelSpac theorem MeasurePreserving.set_integral_preimage_emb {β} {_ : MeasurableSpace β} {f : α → β} {ν} (h₁ : MeasurePreserving f μ ν) (h₂ : MeasurableEmbedding f) (g : β → E) (s : Set β) : - (∫ x in f ⁻¹' s, g (f x) ∂μ) = ∫ y in s, g y ∂ν := + ∫ x in f ⁻¹' s, g (f x) ∂μ = ∫ y in s, g y ∂ν := (h₁.restrict_preimage_emb h₂ s).integral_comp h₂ _ #align measure_theory.measure_preserving.set_integral_preimage_emb MeasureTheory.MeasurePreserving.set_integral_preimage_emb @@ -518,7 +517,7 @@ theorem set_integral_map_equiv {β} [MeasurableSpace β] (e : α ≃ᵐ β) (f : theorem norm_set_integral_le_of_norm_le_const_ae {C : ℝ} (hs : μ s < ∞) (hC : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ C) : ‖∫ x in s, f x ∂μ‖ ≤ C * (μ s).toReal := by rw [← Measure.restrict_apply_univ] at * - haveI : IsFiniteMeasure (μ.restrict s) := ⟨‹_›⟩ + haveI : IsFiniteMeasure (μ.restrict s) := ⟨hs⟩ exact norm_integral_le_of_norm_le_const hC #align measure_theory.norm_set_integral_le_of_norm_le_const_ae MeasureTheory.norm_set_integral_le_of_norm_le_const_ae @@ -530,7 +529,7 @@ theorem norm_set_integral_le_of_norm_le_const_ae' {C : ℝ} (hs : μ s < ∞) filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3 rw [← h2 h3] exact h1 h3 - have B : MeasurableSet {x | ‖(hfm.mk f) x‖ ≤ C} := + have B : MeasurableSet {x | ‖hfm.mk f x‖ ≤ C} := hfm.stronglyMeasurable_mk.norm.measurable measurableSet_Iic filter_upwards [hfm.ae_eq_mk, (ae_restrict_iff B).2 A] with _ h1 _ rwa [h1] @@ -581,8 +580,7 @@ theorem set_integral_gt_gt {R : ℝ} {f : α → ℝ} (hR : 0 ≤ R) (hfm : Meas · rw [← zero_lt_iff] at hμ rwa [Set.inter_eq_self_of_subset_right] exact fun x hx => Ne.symm (ne_of_lt <| sub_pos.2 hx) - · change ∀ᵐ x ∂μ.restrict _, _ - rw [ae_restrict_iff] + · rw [Pi.zero_def, EventuallyLE, ae_restrict_iff] · exact eventually_of_forall fun x hx => sub_nonneg.2 <| le_of_lt hx · exact measurableSet_le measurable_zero (hfm.sub measurable_const) · exact Integrable.sub hfint this @@ -680,36 +678,36 @@ variable {μ : Measure α} {f g : α → ℝ} {s t : Set α} (hf : IntegrableOn (hg : IntegrableOn g s μ) theorem set_integral_mono_ae_restrict (h : f ≤ᵐ[μ.restrict s] g) : - (∫ a in s, f a ∂μ) ≤ ∫ a in s, g a ∂μ := + ∫ a in s, f a ∂μ ≤ ∫ a in s, g a ∂μ := integral_mono_ae hf hg h #align measure_theory.set_integral_mono_ae_restrict MeasureTheory.set_integral_mono_ae_restrict -theorem set_integral_mono_ae (h : f ≤ᵐ[μ] g) : (∫ a in s, f a ∂μ) ≤ ∫ a in s, g a ∂μ := +theorem set_integral_mono_ae (h : f ≤ᵐ[μ] g) : ∫ a in s, f a ∂μ ≤ ∫ a in s, g a ∂μ := set_integral_mono_ae_restrict hf hg (ae_restrict_of_ae h) #align measure_theory.set_integral_mono_ae MeasureTheory.set_integral_mono_ae theorem set_integral_mono_on (hs : MeasurableSet s) (h : ∀ x ∈ s, f x ≤ g x) : - (∫ a in s, f a ∂μ) ≤ ∫ a in s, g a ∂μ := + ∫ a in s, f a ∂μ ≤ ∫ a in s, g a ∂μ := set_integral_mono_ae_restrict hf hg (by simp [hs, EventuallyLE, eventually_inf_principal, ae_of_all _ h]) #align measure_theory.set_integral_mono_on MeasureTheory.set_integral_mono_on theorem set_integral_mono_on_ae (hs : MeasurableSet s) (h : ∀ᵐ x ∂μ, x ∈ s → f x ≤ g x) : - (∫ a in s, f a ∂μ) ≤ ∫ a in s, g a ∂μ := by + ∫ a in s, f a ∂μ ≤ ∫ a in s, g a ∂μ := by refine' set_integral_mono_ae_restrict hf hg _; rwa [EventuallyLE, ae_restrict_iff' hs] #align measure_theory.set_integral_mono_on_ae MeasureTheory.set_integral_mono_on_ae -theorem set_integral_mono (h : f ≤ g) : (∫ a in s, f a ∂μ) ≤ ∫ a in s, g a ∂μ := +theorem set_integral_mono (h : f ≤ g) : ∫ a in s, f a ∂μ ≤ ∫ a in s, g a ∂μ := integral_mono hf hg h #align measure_theory.set_integral_mono MeasureTheory.set_integral_mono theorem set_integral_mono_set (hfi : IntegrableOn f t μ) (hf : 0 ≤ᵐ[μ.restrict t] f) - (hst : s ≤ᵐ[μ] t) : (∫ x in s, f x ∂μ) ≤ ∫ x in t, f x ∂μ := + (hst : s ≤ᵐ[μ] t) : ∫ x in s, f x ∂μ ≤ ∫ x in t, f x ∂μ := integral_mono_measure (Measure.restrict_mono_ae hst) hf hfi #align measure_theory.set_integral_mono_set MeasureTheory.set_integral_mono_set theorem set_integral_le_integral (hfi : Integrable f μ) (hf : 0 ≤ᵐ[μ] f) : - (∫ x in s, f x ∂μ) ≤ ∫ x, f x ∂μ := + ∫ x in s, f x ∂μ ≤ ∫ x, f x ∂μ := integral_mono_measure (Measure.restrict_le_self) hf hfi theorem set_integral_ge_of_const_le {c : ℝ} (hs : MeasurableSet s) (hμs : μ s ≠ ∞) @@ -744,7 +742,7 @@ theorem set_integral_nonneg_ae (hs : MeasurableSet s) (hf : ∀ᵐ a ∂μ, a #align measure_theory.set_integral_nonneg_ae MeasureTheory.set_integral_nonneg_ae theorem set_integral_le_nonneg {s : Set α} (hs : MeasurableSet s) (hf : StronglyMeasurable f) - (hfi : Integrable f μ) : (∫ x in s, f x ∂μ) ≤ ∫ x in {y | 0 ≤ f y}, f x ∂μ := by + (hfi : Integrable f μ) : ∫ x in s, f x ∂μ ≤ ∫ x in {y | 0 ≤ f y}, f x ∂μ := by rw [← integral_indicator hs, ← integral_indicator (stronglyMeasurable_const.measurableSet_le hf)] exact @@ -753,26 +751,26 @@ theorem set_integral_le_nonneg {s : Set α} (hs : MeasurableSet s) (hf : Strongl (indicator_le_indicator_nonneg s f) #align measure_theory.set_integral_le_nonneg MeasureTheory.set_integral_le_nonneg -theorem set_integral_nonpos_of_ae_restrict (hf : f ≤ᵐ[μ.restrict s] 0) : (∫ a in s, f a ∂μ) ≤ 0 := +theorem set_integral_nonpos_of_ae_restrict (hf : f ≤ᵐ[μ.restrict s] 0) : ∫ a in s, f a ∂μ ≤ 0 := integral_nonpos_of_ae hf #align measure_theory.set_integral_nonpos_of_ae_restrict MeasureTheory.set_integral_nonpos_of_ae_restrict -theorem set_integral_nonpos_of_ae (hf : f ≤ᵐ[μ] 0) : (∫ a in s, f a ∂μ) ≤ 0 := +theorem set_integral_nonpos_of_ae (hf : f ≤ᵐ[μ] 0) : ∫ a in s, f a ∂μ ≤ 0 := set_integral_nonpos_of_ae_restrict (ae_restrict_of_ae hf) #align measure_theory.set_integral_nonpos_of_ae MeasureTheory.set_integral_nonpos_of_ae -theorem set_integral_nonpos (hs : MeasurableSet s) (hf : ∀ a, a ∈ s → f a ≤ 0) : - (∫ a in s, f a ∂μ) ≤ 0 := - set_integral_nonpos_of_ae_restrict ((ae_restrict_iff' hs).mpr (ae_of_all μ hf)) -#align measure_theory.set_integral_nonpos MeasureTheory.set_integral_nonpos - theorem set_integral_nonpos_ae (hs : MeasurableSet s) (hf : ∀ᵐ a ∂μ, a ∈ s → f a ≤ 0) : - (∫ a in s, f a ∂μ) ≤ 0 := + ∫ a in s, f a ∂μ ≤ 0 := set_integral_nonpos_of_ae_restrict <| by rwa [EventuallyLE, ae_restrict_iff' hs] #align measure_theory.set_integral_nonpos_ae MeasureTheory.set_integral_nonpos_ae +theorem set_integral_nonpos (hs : MeasurableSet s) (hf : ∀ a, a ∈ s → f a ≤ 0) : + ∫ a in s, f a ∂μ ≤ 0 := + set_integral_nonpos_ae hs <| ae_of_all μ hf +#align measure_theory.set_integral_nonpos MeasureTheory.set_integral_nonpos + theorem set_integral_nonpos_le {s : Set α} (hs : MeasurableSet s) (hf : StronglyMeasurable f) - (hfi : Integrable f μ) : (∫ x in {y | f y ≤ 0}, f x ∂μ) ≤ ∫ x in s, f x ∂μ := by + (hfi : Integrable f μ) : ∫ x in {y | f y ≤ 0}, f x ∂μ ≤ ∫ x in s, f x ∂μ := by rw [← integral_indicator hs, ← integral_indicator (hf.measurableSet_le stronglyMeasurable_const)] exact @@ -1099,13 +1097,13 @@ namespace ContinuousLinearMap variable [NormedSpace ℝ F] theorem integral_compLp (L : E →L[𝕜] F) (φ : Lp E p μ) : - (∫ a, (L.compLp φ) a ∂μ) = ∫ a, L (φ a) ∂μ := + ∫ a, (L.compLp φ) a ∂μ = ∫ a, L (φ a) ∂μ := integral_congr_ae <| coeFn_compLp _ _ set_option linter.uppercaseLean3 false in #align continuous_linear_map.integral_comp_Lp ContinuousLinearMap.integral_compLp theorem set_integral_compLp (L : E →L[𝕜] F) (φ : Lp E p μ) {s : Set α} (hs : MeasurableSet s) : - (∫ a in s, (L.compLp φ) a ∂μ) = ∫ a in s, L (φ a) ∂μ := + ∫ a in s, (L.compLp φ) a ∂μ = ∫ a in s, L (φ a) ∂μ := set_integral_congr_ae hs ((L.coeFn_compLp φ).mono fun _x hx _ => hx) set_option linter.uppercaseLean3 false in #align continuous_linear_map.set_integral_comp_Lp ContinuousLinearMap.set_integral_compLp @@ -1119,15 +1117,14 @@ set_option linter.uppercaseLean3 false in variable [CompleteSpace E] [CompleteSpace F] [NormedSpace ℝ E] theorem integral_comp_comm (L : E →L[𝕜] F) {φ : α → E} (φ_int : Integrable φ μ) : - (∫ a, L (φ a) ∂μ) = L (∫ a, φ a ∂μ) := by - apply Integrable.induction (P := fun φ => (∫ a, L (φ a) ∂μ) = L (∫ a, φ a ∂μ)) + ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) := by + apply φ_int.induction (P := fun φ => ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ)) · intro e s s_meas _ rw [integral_indicator_const e s_meas, ← @smul_one_smul E ℝ 𝕜 _ _ _ _ _ (μ s).toReal e, ContinuousLinearMap.map_smul, @smul_one_smul F ℝ 𝕜 _ _ _ _ _ (μ s).toReal (L e), ← integral_indicator_const (L e) s_meas] congr 1 with a - erw [Set.indicator_comp_of_zero L.map_zero] - rfl + rw [← Function.comp_def L, Set.indicator_comp_of_zero L.map_zero, Function.comp_apply] · intro f g _ f_int g_int hf hg simp [L.map_add, integral_add (μ := μ) f_int g_int, integral_add (μ := μ) (L.integrable_comp f_int) (L.integrable_comp g_int), hf, hg] @@ -1136,7 +1133,6 @@ theorem integral_comp_comm (L : E →L[𝕜] F) {φ : α → E} (φ_int : Integr convert hf using 1 <;> clear hf · exact integral_congr_ae (hfg.fun_comp L).symm · rw [integral_congr_ae hfg.symm] - all_goals assumption #align continuous_linear_map.integral_comp_comm ContinuousLinearMap.integral_comp_comm theorem integral_apply {H : Type*} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {φ : α → H →L[𝕜] E} @@ -1145,7 +1141,7 @@ theorem integral_apply {H : Type*} [NormedAddCommGroup H] [NormedSpace 𝕜 H] { #align continuous_linear_map.integral_apply ContinuousLinearMap.integral_apply theorem integral_comp_comm' (L : E →L[𝕜] F) {K} (hL : AntilipschitzWith K L) (φ : α → E) : - (∫ a, L (φ a) ∂μ) = L (∫ a, φ a ∂μ) := by + ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) := by by_cases h : Integrable φ μ · exact integral_comp_comm L h have : ¬Integrable (fun a => L (φ a)) μ := by @@ -1155,7 +1151,7 @@ theorem integral_comp_comm' (L : E →L[𝕜] F) {K} (hL : AntilipschitzWith K L #align continuous_linear_map.integral_comp_comm' ContinuousLinearMap.integral_comp_comm' theorem integral_comp_L1_comm (L : E →L[𝕜] F) (φ : α →₁[μ] E) : - (∫ a, L (φ a) ∂μ) = L (∫ a, φ a ∂μ) := + ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) := L.integral_comp_comm (L1.integrable_coeFn φ) set_option linter.uppercaseLean3 false in #align continuous_linear_map.integral_comp_L1_comm ContinuousLinearMap.integral_comp_L1_comm @@ -1166,7 +1162,7 @@ namespace LinearIsometry variable [CompleteSpace F] [NormedSpace ℝ F] [CompleteSpace E] [NormedSpace ℝ E] -theorem integral_comp_comm (L : E →ₗᵢ[𝕜] F) (φ : α → E) : (∫ a, L (φ a) ∂μ) = L (∫ a, φ a ∂μ) := +theorem integral_comp_comm (L : E →ₗᵢ[𝕜] F) (φ : α → E) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) := L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _ #align linear_isometry.integral_comp_comm LinearIsometry.integral_comp_comm @@ -1176,39 +1172,37 @@ namespace ContinuousLinearEquiv variable [NormedSpace ℝ F] [NormedSpace ℝ E] -theorem integral_comp_comm (L : E ≃L[𝕜] F) (φ : α → E) : (∫ a, L (φ a) ∂μ) = L (∫ a, φ a ∂μ) := by +theorem integral_comp_comm (L : E ≃L[𝕜] F) (φ : α → E) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) := by have : CompleteSpace E ↔ CompleteSpace F := completeSpace_congr (e := L.toEquiv) L.uniformEmbedding - by_cases hE : CompleteSpace E - · have : CompleteSpace F := this.1 hE - exact L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _ - · have := this.not.1 hE - simp [integral, *] + obtain ⟨_, _⟩|⟨_, _⟩ := iff_iff_and_or_not_and_not.mp this + · exact L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _ + · simp [integral, *] #align continuous_linear_equiv.integral_comp_comm ContinuousLinearEquiv.integral_comp_comm end ContinuousLinearEquiv @[norm_cast] -theorem integral_ofReal {f : α → ℝ} : (∫ a, (f a : 𝕜) ∂μ) = ↑(∫ a, f a ∂μ) := +theorem integral_ofReal {f : α → ℝ} : ∫ a, (f a : 𝕜) ∂μ = ↑(∫ a, f a ∂μ) := (@IsROrC.ofRealLI 𝕜 _).integral_comp_comm f #align integral_of_real integral_ofReal theorem integral_re {f : α → 𝕜} (hf : Integrable f μ) : - (∫ a, IsROrC.re (f a) ∂μ) = IsROrC.re (∫ a, f a ∂μ) := + ∫ a, IsROrC.re (f a) ∂μ = IsROrC.re (∫ a, f a ∂μ) := (@IsROrC.reCLM 𝕜 _).integral_comp_comm hf #align integral_re integral_re theorem integral_im {f : α → 𝕜} (hf : Integrable f μ) : - (∫ a, IsROrC.im (f a) ∂μ) = IsROrC.im (∫ a, f a ∂μ) := + ∫ a, IsROrC.im (f a) ∂μ = IsROrC.im (∫ a, f a ∂μ) := (@IsROrC.imCLM 𝕜 _).integral_comp_comm hf #align integral_im integral_im -theorem integral_conj {f : α → 𝕜} : (∫ a, conj (f a) ∂μ) = conj (∫ a, f a ∂μ) := +theorem integral_conj {f : α → 𝕜} : ∫ a, conj (f a) ∂μ = conj (∫ a, f a ∂μ) := (@IsROrC.conjLIE 𝕜 _).toLinearIsometry.integral_comp_comm f #align integral_conj integral_conj theorem integral_coe_re_add_coe_im {f : α → 𝕜} (hf : Integrable f μ) : - (∫ x, (IsROrC.re (f x) : 𝕜) ∂μ) + (∫ x, (IsROrC.im (f x) : 𝕜) ∂μ) * IsROrC.I = ∫ x, f x ∂μ := by + ∫ x, (IsROrC.re (f x) : 𝕜) ∂μ + (∫ x, (IsROrC.im (f x) : 𝕜) ∂μ) * IsROrC.I = ∫ x, f x ∂μ := by rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add] · congr ext1 x @@ -1250,7 +1244,7 @@ theorem snd_integral [CompleteSpace E] {f : α → E × F} (hf : Integrable f μ theorem integral_pair [CompleteSpace E] [CompleteSpace F] {f : α → E} {g : α → F} (hf : Integrable f μ) (hg : Integrable g μ) : - (∫ x, (f x, g x) ∂μ) = (∫ x, f x ∂μ, ∫ x, g x ∂μ) := + ∫ x, (f x, g x) ∂μ = (∫ x, f x ∂μ, ∫ x, g x ∂μ) := have := hf.prod_mk hg Prod.ext (fst_integral this) (snd_integral this) #align integral_pair integral_pair