Exact source: Mathlib/MeasureTheory/Function/Jacobian.lean
Pinned GitHub source · Raw UTF-8 source
Back to The absolute Jacobian integral of a radial sphere extension
1/-2Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Sébastien Gouëzel5-/6module78public import Mathlib.Analysis.Calculus.FDeriv.Congr9public import Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap10public import Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace11public import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar12public import Mathlib.Analysis.Normed.Module.Ball.Pointwise13public import Mathlib.MeasureTheory.Constructions.Polish.Basic14public import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn15public import Mathlib.Topology.Algebra.Module.Determinant1617/-!18# Change of variables in higher-dimensional integrals1920Let `μ` be a Lebesgue measure on a finite-dimensional real vector space `E`.21Let `f : E → E` be a function which is injective and differentiable on a measurable set `s`,22with derivative `f'`. Then we prove that `f '' s` is measurable, and23its measure is given by the formula `μ (f '' s) = ∫⁻ x in s, |(f' x).det| ∂μ` (where `(f' x).det`24is almost everywhere measurable, but not Borel-measurable in general). This formula is proved in25`lintegral_abs_det_fderiv_eq_addHaar_image`. We deduce the change of variables26formula for the Lebesgue and Bochner integrals, in `lintegral_image_eq_lintegral_abs_det_fderiv_mul`27and `integral_image_eq_integral_abs_det_fderiv_smul` respectively.2829Specialized versions in one dimension (using the derivative instead of the determinant of the30Fréchet derivative) can be found in the file `Mathlib/MeasureTheory/Function/JacobianOneDim.lean`,31together with versions for monotone and antitone functions.3233## Main results3435* `addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero`: if `f` is differentiable on a36 set `s` with zero measure, then `f '' s` also has zero measure.37* `addHaar_image_eq_zero_of_det_fderivWithin_eq_zero`: if `f` is differentiable on a set `s`, and38 its derivative is never invertible, then `f '' s` has zero measure (a version of Sard's lemma).39* `aemeasurable_fderivWithin`: if `f` is differentiable on a measurable set `s`, then `f'`40 is almost everywhere measurable on `s`.4142For the next statements, `s` is a measurable set and `f` is differentiable on `s`43(with a derivative `f'`) and injective on `s`.4445* `measurable_image_of_fderivWithin`: the image `f '' s` is measurable.46* `measurableEmbedding_of_fderivWithin`: the function `s.restrict f` is a measurable embedding.47* `lintegral_abs_det_fderiv_eq_addHaar_image`: the image measure is given by48 `μ (f '' s) = ∫⁻ x in s, |(f' x).det| ∂μ`.49* `lintegral_image_eq_lintegral_abs_det_fderiv_mul`: for `g : E → ℝ≥0∞`, one has50 `∫⁻ x in f '' s, g x ∂μ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ`.51* `integral_image_eq_integral_abs_det_fderiv_smul`: for `g : E → F`, one has52 `∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ`.53* `integrableOn_image_iff_integrableOn_abs_det_fderiv_smul`: for `g : E → F`, the function `g` is54 integrable on `f '' s` if and only if `|(f' x).det| • g (f x)` is integrable on `s`.5556## Implementation5758Typical versions of these results in the literature have much stronger assumptions: `s` would59typically be open, and the derivative `f' x` would depend continuously on `x` and be invertible60everywhere, to have the local inverse theorem at our disposal. The proof strategy under our weaker61assumptions is more involved. We follow [Fremlin, *Measure Theory* (volume 2)][fremlin_vol2].6263The first remark is that, if `f` is sufficiently well approximated by a linear map `A` on a set64`s`, then `f` expands the volume of `s` by at least `A.det - ε` and at most `A.det + ε`, where65the closeness condition depends on `A` in a non-explicit way (see `addHaar_image_le_mul_of_det_lt`66and `mul_le_addHaar_image_of_lt_det`). This fact holds for balls by a simple inclusion argument,67and follows for general sets using the Besicovitch covering theorem to cover the set by balls with68measures adding up essentially to `μ s`.6970When `f` is differentiable on `s`, one may partition `s` into countably many subsets `s ∩ t n`71(where `t n` is measurable), on each of which `f` is well approximated by a linear map, so that the72above results apply. See `exists_partition_approximatesLinearOn_of_hasFDerivWithinAt`, which73follows from the pointwise differentiability (in a non-completely trivial way, as one should ensure74a form of uniformity on the sets of the partition).7576Combining the above two results would give the conclusion, except for two difficulties: it is not77obvious why `f '' s` and `f'` should be measurable, which prevents us from using countable78additivity for the measure and the integral. It turns out that `f '' s` is indeed measurable,79and that `f'` is almost everywhere measurable, which is enough to recover countable additivity.8081The measurability of `f '' s` follows from the deep Lusin-Souslin theorem ensuring that, in a82Polish space, a continuous injective image of a measurable set is measurable.8384The key point to check the almost everywhere measurability of `f'` is that, if `f` is approximated85up to `δ` by a linear map on a set `s`, then `f'` is within `δ` of `A` on a full measure subset86of `s` (namely, its density points). With the above approximation argument, it follows that `f'`87is the almost everywhere limit of a sequence of measurable functions (which are constant on the88pieces of the good discretization), and is therefore almost everywhere measurable.8990## Tags91Change of variables in integrals9293## References94[Fremlin, *Measure Theory* (volume 2)][fremlin_vol2]95-/9697public section9899open MeasureTheory MeasureTheory.Measure Metric Filter Set Module Asymptotics100 TopologicalSpace101102open scoped NNReal ENNReal Topology Pointwise103104variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]105 [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E}106107/-!108### Decomposition lemmas109110We state lemmas ensuring that a differentiable function can be approximated, on countably many111measurable pieces, by linear maps (with a prescribed precision depending on the linear map).112-/113114/-- Assume that a function `f` has a derivative at every point of a set `s`. Then one may cover `s`115with countably many closed sets `t n` on which `f` is well approximated by linear maps `A n`. -/116theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt [SecondCountableTopology F]117 (f : E → F) (s : Set E) (f' : E → E →L[ℝ] F) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)118 (r : (E →L[ℝ] F) → ℝ≥0) (rpos : ∀ A, r A ≠ 0) :119 ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),120 (∀ n, IsClosed (t n)) ∧121 (s ⊆ ⋃ n, t n) ∧122 (∀ n, ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧123 (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) := by124 /- Choose countably many linear maps `f' z`. For every such map, if `f` has a derivative at `x`125 close enough to `f' z`, then `f y - f x` is well approximated by `f' z (y - x)` for `y` close126 enough to `x`, say on a ball of radius `r` (or even `u n` for some `n`, where `u` is a fixed127 sequence tending to `0`).128 Let `M n z` be the points where this happens. Then this set is relatively closed inside `s`,129 and moreover in every closed ball of radius `u n / 3` inside it the map is well approximated by130 `f' z`. Using countably many closed balls to split `M n z` into small diameter subsets131 `K n z p`, one obtains the desired sets `t q` after reindexing.132 -/133 -- exclude the trivial case where `s` is empty134 rcases eq_empty_or_nonempty s with (rfl | hs)135 · refine ⟨fun _ => ∅, fun _ => 0, ?_, ?_, ?_, ?_⟩ <;> simp136 -- we will use countably many linear maps. Select these from all the derivatives since the137 -- space of linear maps is second-countable138 obtain ⟨T, T_count, hT⟩ :139 ∃ T : Set s,140 T.Countable ∧ ⋃ x ∈ T, ball (f' (x : E)) (r (f' x)) = ⋃ x : s, ball (f' x) (r (f' x)) :=141 TopologicalSpace.isOpen_iUnion_countable _ fun x => isOpen_ball142 -- fix a sequence `u` of positive reals tending to zero.143 obtain ⟨u, _, u_pos, u_lim⟩ :144 ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=145 exists_seq_strictAnti_tendsto (0 : ℝ)146 -- `M n z` is the set of points `x` such that `f y - f x` is close to `f' z (y - x)` for `y`147 -- in the ball of radius `u n` around `x`.148 let M : ℕ → T → Set E := fun n z =>149 {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - f' z (y - x)‖ ≤ r (f' z) * ‖y - x‖}150 -- As `f` is differentiable everywhere on `s`, the sets `M n z` cover `s` by design.151 have s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : T), x ∈ M n z := by152 intro x xs153 obtain ⟨z, zT, hz⟩ : ∃ z ∈ T, f' x ∈ ball (f' (z : E)) (r (f' z)) := by154 have : f' x ∈ ⋃ z ∈ T, ball (f' (z : E)) (r (f' z)) := by155 rw [hT]156 refine mem_iUnion.2 ⟨⟨x, xs⟩, ?_⟩157 simpa only [mem_ball, Subtype.coe_mk, dist_self] using! (rpos (f' x)).bot_lt158 rwa [mem_iUnion₂, bex_def] at this159 obtain ⟨ε, εpos, hε⟩ : ∃ ε : ℝ, 0 < ε ∧ ‖f' x - f' z‖ + ε ≤ r (f' z) := by160 refine ⟨r (f' z) - ‖f' x - f' z‖, ?_, le_of_eq (by abel)⟩161 simpa only [sub_pos] using! mem_ball_iff_norm.mp hz162 obtain ⟨δ, δpos, hδ⟩ :163 ∃ (δ : ℝ), 0 < δ ∧ ball x δ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖} :=164 Metric.mem_nhdsWithin_iff.1 ((hf' x xs).isLittleO.def εpos)165 obtain ⟨n, hn⟩ : ∃ n, u n < δ := ((tendsto_order.1 u_lim).2 _ δpos).exists166 refine ⟨n, ⟨z, zT⟩, ⟨xs, ?_⟩⟩167 intro y hy168 calc169 ‖f y - f x - (f' z) (y - x)‖ = ‖f y - f x - (f' x) (y - x) + (f' x - f' z) (y - x)‖ := by170 congr 1171 simp only [FunLike.coe_sub, map_sub, Pi.sub_apply]172 abel173 _ ≤ ‖f y - f x - (f' x) (y - x)‖ + ‖(f' x - f' z) (y - x)‖ := norm_add_le _ _174 _ ≤ ε * ‖y - x‖ + ‖f' x - f' z‖ * ‖y - x‖ := by175 refine add_le_add (hδ ?_) (ContinuousLinearMap.le_opNorm _ _)176 rw [inter_comm]177 exact inter_subset_inter_right _ (ball_subset_ball hn.le) hy178 _ ≤ r (f' z) * ‖y - x‖ := by179 rw [← add_mul, add_comm]180 gcongr181 -- the sets `M n z` are relatively closed in `s`, as all the conditions defining it are clearly182 -- closed183 have closure_M_subset : ∀ n z, s ∩ closure (M n z) ⊆ M n z := by184 rintro n z x ⟨xs, hx⟩185 refine ⟨xs, fun y hy => ?_⟩186 obtain ⟨a, aM, a_lim⟩ : ∃ a : ℕ → E, (∀ k, a k ∈ M n z) ∧ Tendsto a atTop (𝓝 x) :=187 mem_closure_iff_seq_limit.1 hx188 have L1 :189 Tendsto (fun k : ℕ => ‖f y - f (a k) - (f' z) (y - a k)‖) atTop190 (𝓝 ‖f y - f x - (f' z) (y - x)‖) := by191 apply Tendsto.norm192 have L : Tendsto (fun k => f (a k)) atTop (𝓝 (f x)) := by193 apply (hf' x xs).continuousWithinAt.tendsto.comp194 apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ a_lim195 exact Eventually.of_forall fun k => (aM k).1196 apply Tendsto.sub (tendsto_const_nhds.sub L)197 exact ((f' z).continuous.tendsto _).comp (tendsto_const_nhds.sub a_lim)198 have L2 : Tendsto (fun k : ℕ => (r (f' z) : ℝ) * ‖y - a k‖) atTop (𝓝 (r (f' z) * ‖y - x‖)) :=199 (tendsto_const_nhds.sub a_lim).norm.const_mul _200 have I : ∀ᶠ k in atTop, ‖f y - f (a k) - (f' z) (y - a k)‖ ≤ r (f' z) * ‖y - a k‖ := by201 have L : Tendsto (fun k => dist y (a k)) atTop (𝓝 (dist y x)) :=202 tendsto_const_nhds.dist a_lim203 filter_upwards [(tendsto_order.1 L).2 _ hy.2]204 intro k hk205 exact (aM k).2 y ⟨hy.1, hk⟩206 exact le_of_tendsto_of_tendsto L1 L2 I207 -- choose a dense sequence `d p`208 rcases TopologicalSpace.exists_dense_seq E with ⟨d, hd⟩209 -- split `M n z` into subsets `K n z p` of small diameters by intersecting with the ball210 -- `closedBall (d p) (u n / 3)`.211 let K : ℕ → T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)212 -- on the sets `K n z p`, the map `f` is well approximated by `f' z` by design.213 have K_approx : ∀ (n) (z : T) (p), ApproximatesLinearOn f (f' z) (s ∩ K n z p) (r (f' z)) := by214 intro n z p x hx y hy215 have yM : y ∈ M n z := closure_M_subset _ _ ⟨hy.1, hy.2.1⟩216 refine yM.2 _ ⟨hx.1, ?_⟩217 calc218 dist x y ≤ dist x (d p) + dist y (d p) := dist_triangle_right _ _ _219 _ ≤ u n / 3 + u n / 3 := add_le_add hx.2.2 hy.2.2220 _ < u n := by linarith [u_pos n]221 -- the sets `K n z p` are also closed, again by design.222 have K_closed : ∀ (n) (z : T) (p), IsClosed (K n z p) := fun n z p =>223 isClosed_closure.inter isClosed_closedBall224 -- reindex the sets `K n z p`, to let them only depend on an integer parameter `q`.225 obtain ⟨F, hF⟩ : ∃ F : ℕ → ℕ × T × ℕ, Function.Surjective F := by226 haveI : Encodable T := T_count.toEncodable227 have : Nonempty T := by228 rcases hs with ⟨x, xs⟩229 rcases s_subset x xs with ⟨n, z, _⟩230 exact ⟨z⟩231 inhabit ↥T232 exact ⟨_, Encodable.surjective_decode_getD (ℕ × T × ℕ) default⟩233 -- these sets `t q = K n z p` will do234 refine235 ⟨fun q => K (F q).1 (F q).2.1 (F q).2.2, fun q => f' (F q).2.1, fun n => K_closed _ _ _,236 fun x xs => ?_, fun q => K_approx _ _ _, fun _ q => ⟨(F q).2.1, (F q).2.1.1.2, rfl⟩⟩237 -- the only fact that needs further checking is that they cover `s`.238 -- we already know that any point `x ∈ s` belongs to a set `M n z`.239 obtain ⟨n, z, hnz⟩ : ∃ (n : ℕ) (z : T), x ∈ M n z := s_subset x xs240 -- by density, it also belongs to a ball `closedBall (d p) (u n / 3)`.241 obtain ⟨p, hp⟩ : ∃ p : ℕ, x ∈ closedBall (d p) (u n / 3) := by242 have : Set.Nonempty (ball x (u n / 3)) := by simp only [nonempty_ball]; linarith [u_pos n]243 obtain ⟨p, hp⟩ : ∃ p : ℕ, d p ∈ ball x (u n / 3) := hd.exists_mem_open isOpen_ball this244 exact ⟨p, (mem_ball'.1 hp).le⟩245 -- choose `q` for which `t q = K n z p`.246 obtain ⟨q, hq⟩ : ∃ q, F q = (n, z, p) := hF _247 -- then `x` belongs to `t q`.248 apply mem_iUnion.2 ⟨q, _⟩249 simp -zeta only [K, hq, mem_inter_iff, hp, and_true]250 exact subset_closure hnz251252variable [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ]253254open scoped Function -- required for scoped `on` notation255256/-- Assume that a function `f` has a derivative at every point of a set `s`. Then one may257partition `s` into countably many disjoint relatively measurable sets (i.e., intersections258of `s` with measurable sets `t n`) on which `f` is well approximated by linear maps `A n`. -/259theorem exists_partition_approximatesLinearOn_of_hasFDerivWithinAt [SecondCountableTopology F]260 (f : E → F) (s : Set E) (f' : E → E →L[ℝ] F) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)261 (r : (E →L[ℝ] F) → ℝ≥0) (rpos : ∀ A, r A ≠ 0) :262 ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),263 Pairwise (Disjoint on t) ∧264 (∀ n, MeasurableSet (t n)) ∧265 (s ⊆ ⋃ n, t n) ∧266 (∀ n, ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧267 (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) := by268 rcases exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' r rpos with269 ⟨t, A, t_closed, st, t_approx, ht⟩270 refine271 ⟨disjointed t, A, disjoint_disjointed _,272 MeasurableSet.disjointed fun n => (t_closed n).measurableSet, ?_, ?_, ht⟩273 · rw [iUnion_disjointed]; exact st274 · intro n; exact (t_approx n).mono_set (inter_subset_inter_right _ (disjointed_subset _ _))275276namespace MeasureTheory277278/-!279### Local lemmas280281We check that a function which is well enough approximated by a linear map expands the volume282essentially like this linear map, and that its derivative (if it exists) is almost everywhere close283to the approximating linear map.284-/285286287/-- Let `f` be a function which is sufficiently close (in the Lipschitz sense) to a given linear288map `A`. Then it expands the volume of any set by at most `m` for any `m > det A`. -/289theorem addHaar_image_le_mul_of_det_lt (A : E →L[ℝ] E) {m : ℝ≥0}290 (hm : ENNReal.ofReal |A.det| < m) :291 ∀ᶠ δ in 𝓝[>] (0 : ℝ≥0),292 ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ m * μ s := by293 apply nhdsWithin_le_nhds294 let d := ENNReal.ofReal |A.det|295 -- construct a small neighborhood of `A '' (closedBall 0 1)` with measure comparable to296 -- the determinant of `A`.297 obtain ⟨ε, hε, εpos⟩ :298 ∃ ε : ℝ, μ (closedBall 0 ε + A '' closedBall 0 1) < m * μ (closedBall 0 1) ∧ 0 < ε := by299 have HC : IsCompact (A '' closedBall 0 1) :=300 (ProperSpace.isCompact_closedBall _ _).image A.continuous301 have L0 :302 Tendsto (fun ε => μ (cthickening ε (A '' closedBall 0 1))) (𝓝[>] 0)303 (𝓝 (μ (A '' closedBall 0 1))) := by304 apply Tendsto.mono_left _ nhdsWithin_le_nhds305 exact tendsto_measure_cthickening_of_isCompact HC306 have L1 :307 Tendsto (fun ε => μ (closedBall 0 ε + A '' closedBall 0 1)) (𝓝[>] 0)308 (𝓝 (μ (A '' closedBall 0 1))) := by309 apply L0.congr' _310 filter_upwards [self_mem_nhdsWithin] with r hr311 rw [← HC.add_closedBall_zero (le_of_lt hr), add_comm]312 have L2 :313 Tendsto (fun ε => μ (closedBall 0 ε + A '' closedBall 0 1)) (𝓝[>] 0)314 (𝓝 (d * μ (closedBall 0 1))) := by315 convert! L1316 exact (addHaar_image_continuousLinearMap _ _ _).symm317 have I : d * μ (closedBall 0 1) < m * μ (closedBall 0 1) := by318 gcongr; exacts [(measure_closedBall_pos μ _ zero_lt_one).ne', measure_closedBall_lt_top.ne]319 have H :320 ∀ᶠ b : ℝ in 𝓝[>] 0, μ (closedBall 0 b + A '' closedBall 0 1) < m * μ (closedBall 0 1) :=321 (tendsto_order.1 L2).2 _ I322 exact (H.and self_mem_nhdsWithin).exists323 have : Iio (.mk ε εpos.le) ∈ 𝓝 (0 : ℝ≥0) := by apply Iio_mem_nhds; exact εpos324 filter_upwards [this]325 -- fix a function `f` which is close enough to `A`.326 intro δ hδ s f hf327 simp only [mem_Iio, ← NNReal.coe_lt_coe, NNReal.coe_mk] at hδ328 -- This function expands the volume of any ball by at most `m`329 have I : ∀ x r, x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ m * μ (closedBall x r) := by330 intro x r xs r0331 have K : f '' (s ∩ closedBall x r) ⊆ A '' closedBall 0 r + closedBall (f x) (ε * r) := by332 rintro y ⟨z, ⟨zs, zr⟩, rfl⟩333 rw [mem_closedBall_iff_norm] at zr334 apply Set.mem_add.2 ⟨A (z - x), _, f z - f x - A (z - x) + f x, _, _⟩335 · apply mem_image_of_mem336 simpa only [dist_eq_norm, mem_closedBall, mem_closedBall_zero_iff, sub_zero] using zr337 · rw [mem_closedBall_iff_norm, add_sub_cancel_right]338 calc339 ‖f z - f x - A (z - x)‖ ≤ δ * ‖z - x‖ := hf _ zs _ xs340 _ ≤ ε * r := by gcongr341 · simp only [map_sub]342 abel343 have :344 A '' closedBall 0 r + closedBall (f x) (ε * r) =345 {f x} + r • (A '' closedBall 0 1 + closedBall 0 ε) := by346 rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,347 singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,348 smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]349 rw [this] at K350 calc351 μ (f '' (s ∩ closedBall x r)) ≤ μ ({f x} + r • (A '' closedBall 0 1 + closedBall 0 ε)) :=352 measure_mono K353 _ = ENNReal.ofReal (r ^ finrank ℝ E) * μ (A '' closedBall 0 1 + closedBall 0 ε) := by354 simp only [abs_of_nonneg r0, addHaar_smul, image_add_left, abs_pow, singleton_add,355 measure_preimage_add]356 _ ≤ ENNReal.ofReal (r ^ finrank ℝ E) * (m * μ (closedBall 0 1)) := by357 rw [add_comm]; gcongr358 _ = m * μ (closedBall x r) := by simp only [addHaar_closedBall' μ _ r0]; ring359 -- covering `s` by closed balls with total measure very close to `μ s`, one deduces that the360 -- measure of `f '' s` is at most `m * (μ s + a)` for any positive `a`.361 have J : ∀ᶠ a in 𝓝[>] (0 : ℝ≥0∞), μ (f '' s) ≤ m * (μ s + a) := by362 filter_upwards [self_mem_nhdsWithin] with a ha363 rw [mem_Ioi] at ha364 obtain ⟨t, r, t_count, ts, rpos, st, μt⟩ :365 ∃ (t : Set E) (r : E → ℝ),366 t.Countable ∧367 t ⊆ s ∧368 (∀ x : E, x ∈ t → 0 < r x) ∧369 (s ⊆ ⋃ x ∈ t, closedBall x (r x)) ∧370 (∑' x : ↥t, μ (closedBall (↑x) (r ↑x))) ≤ μ s + a :=371 Besicovitch.exists_closedBall_covering_tsum_measure_le μ ha.ne' (fun _ => Ioi 0) s372 fun x _ δ δpos => ⟨δ / 2, by simp [half_pos δpos, δpos]⟩373 haveI : Encodable t := t_count.toEncodable374 calc375 μ (f '' s) ≤ μ (⋃ x : t, f '' (s ∩ closedBall x (r x))) := by376 rw [biUnion_eq_iUnion] at st377 apply measure_mono378 rw [← image_iUnion, ← inter_iUnion]379 exact Set.image_mono (subset_inter (Subset.refl _) st)380 _ ≤ ∑' x : t, μ (f '' (s ∩ closedBall x (r x))) := measure_iUnion_le _381 _ ≤ ∑' x : t, m * μ (closedBall x (r x)) :=382 (ENNReal.tsum_le_tsum fun x => I x (r x) (ts x.2) (rpos x x.2).le)383 _ ≤ m * (μ s + a) := by rw [ENNReal.tsum_mul_left]; gcongr384 -- taking the limit in `a`, one obtains the conclusion385 have L : Tendsto (fun a => (m : ℝ≥0∞) * (μ s + a)) (𝓝[>] 0) (𝓝 (m * (μ s + 0))) := by386 apply Tendsto.mono_left _ nhdsWithin_le_nhds387 apply ENNReal.Tendsto.const_mul (tendsto_const_nhds.add tendsto_id)388 simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]389 rw [add_zero] at L390 exact ge_of_tendsto L J391392/-- Let `f` be a function which is sufficiently close (in the Lipschitz sense) to a given linear393map `A`. Then it expands the volume of any set by at least `m` for any `m < det A`. -/394theorem mul_le_addHaar_image_of_lt_det (A : E →L[ℝ] E) {m : ℝ≥0}395 (hm : (m : ℝ≥0∞) < ENNReal.ofReal |A.det|) :396 ∀ᶠ δ in 𝓝[>] (0 : ℝ≥0),397 ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → (m : ℝ≥0∞) * μ s ≤ μ (f '' s) := by398 apply nhdsWithin_le_nhds399 -- The assumption `hm` implies that `A` is invertible. If `f` is close enough to `A`, it is also400 -- invertible. One can then pass to the inverses, and deduce the estimate from401 -- `addHaar_image_le_mul_of_det_lt` applied to `f⁻¹` and `A⁻¹`.402 -- exclude first the trivial case where `m = 0`.403 rcases eq_zero_or_pos m with (rfl | mpos)404 · filter_upwards405 simp only [forall_const, zero_mul, imp_true_iff, zero_le, ENNReal.coe_zero]406 have hA : A.det ≠ 0 := by407 intro h; simp only [h, ENNReal.not_lt_zero, ENNReal.ofReal_zero, abs_zero] at hm408 -- let `B` be the continuous linear equiv version of `A`.409 let B := A.toContinuousLinearEquivOfDetNeZero hA410 -- the determinant of `B.symm` is bounded by `m⁻¹`411 have I : ENNReal.ofReal |(B.symm : E →L[ℝ] E).det| < (m⁻¹ : ℝ≥0) := by412 simp only [ENNReal.ofReal, abs_inv, Real.toNNReal_inv, ContinuousLinearEquiv.det_coe_symm,413 ENNReal.coe_lt_coe] at hm ⊢414 exact NNReal.inv_lt_inv mpos.ne' hm415 -- therefore, we may apply `addHaar_image_le_mul_of_det_lt` to `B.symm` and `m⁻¹`.416 obtain ⟨δ₀, δ₀pos, hδ₀⟩ :417 ∃ δ : ℝ≥0,418 0 < δ ∧419 ∀ (t : Set E) (g : E → E),420 ApproximatesLinearOn g (B.symm : E →L[ℝ] E) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t := by421 have :422 ∀ᶠ δ : ℝ≥0 in 𝓝[>] 0,423 ∀ (t : Set E) (g : E → E),424 ApproximatesLinearOn g (B.symm : E →L[ℝ] E) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t :=425 addHaar_image_le_mul_of_det_lt μ B.symm I426 rcases (this.and self_mem_nhdsWithin).exists with ⟨δ₀, h, h'⟩427 exact ⟨δ₀, h', h⟩428 -- record smallness conditions for `δ` that will be needed to apply `hδ₀` below.429 have L1 : ∀ᶠ δ in 𝓝 (0 : ℝ≥0), Subsingleton E ∨ δ < ‖(B.symm : E →L[ℝ] E)‖₊⁻¹ := by430 by_cases h : Subsingleton E431 · simp only [h, true_or, eventually_const]432 simp only [h, false_or]433 apply Iio_mem_nhds434 simpa only [h, false_or, inv_pos] using B.subsingleton_or_nnnorm_symm_pos435 have L2 :436 ∀ᶠ δ in 𝓝 (0 : ℝ≥0), ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀ := by437 have :438 Tendsto (fun δ => ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)439 (𝓝 (‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0)) := by440 rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)441 · simpa only [H, zero_mul] using tendsto_const_nhds442 refine Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id443 refine (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_444 simpa only [tsub_zero, inv_eq_zero, Ne] using H445 simp only [mul_zero] at this446 exact (tendsto_order.1 this).2 δ₀ δ₀pos447 -- let `δ` be small enough, and `f` approximated by `B` up to `δ`.448 filter_upwards [L1, L2]449 intro δ h1δ h2δ s f hf450 have hf' : ApproximatesLinearOn f (B : E →L[ℝ] E) s δ := by convert! hf451 let F := hf'.toPartialEquiv h1δ452 -- the condition to be checked can be reformulated in terms of the inverse maps453 suffices H : μ (F.symm '' F.target) ≤ (m⁻¹ : ℝ≥0) * μ F.target by454 change (m : ℝ≥0∞) * μ F.source ≤ μ F.target455 rwa [← F.symm_image_target_eq_source, mul_comm, ← ENNReal.le_div_iff_mul_le, div_eq_mul_inv,456 mul_comm, ← ENNReal.coe_inv mpos.ne']457 · apply Or.inl458 simpa only [ENNReal.coe_eq_zero, Ne] using mpos.ne'459 · simp460 -- as `f⁻¹` is well approximated by `B⁻¹`, the conclusion follows from `hδ₀`461 -- and our choice of `δ`.462 exact hδ₀ _ _ ((hf'.to_inv h1δ).mono_num h2δ.le)463464/-- If a differentiable function `f` is approximated by a linear map `A` on a set `s`, up to `δ`,465then at almost every `x` in `s` one has `‖f' x - A‖ ≤ δ`. -/466theorem _root_.ApproximatesLinearOn.norm_fderiv_sub_le {A : E →L[ℝ] E} {δ : ℝ≥0}467 (hf : ApproximatesLinearOn f A s δ) (hs : MeasurableSet s) (f' : E → E →L[ℝ] E)468 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) : ∀ᵐ x ∂μ.restrict s, ‖f' x - A‖₊ ≤ δ := by469 /- The conclusion will hold at the Lebesgue density points of `s` (which have full measure).470 At such a point `x`, for any `z` and any `ε > 0` one has for small `r`471 that `{x} + r • closedBall z ε` intersects `s`. At a point `y` in the intersection,472 `f y - f x` is close both to `f' x (r z)` (by differentiability) and to `A (r z)`473 (by linear approximation), so these two quantities are close, i.e., `(f' x - A) z` is small. -/474 filter_upwards [Besicovitch.ae_tendsto_measure_inter_div μ s, ae_restrict_mem hs]475 -- start from a Lebesgue density point `x`, belonging to `s`.476 intro x hx xs477 -- consider an arbitrary vector `z`.478 apply ContinuousLinearMap.opNorm_le_bound _ δ.2 fun z => ?_479 -- to show that `‖(f' x - A) z‖ ≤ δ ‖z‖`, it suffices to do it up to some error that vanishes480 -- asymptotically in terms of `ε > 0`.481 suffices H : ∀ ε, 0 < ε → ‖(f' x - A) z‖ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε by482 have :483 Tendsto (fun ε : ℝ => ((δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0)484 (𝓝 ((δ + 0) * (‖z‖ + 0) + ‖f' x - A‖ * 0)) :=485 Tendsto.mono_left (Continuous.tendsto (by fun_prop) 0) nhdsWithin_le_nhds486 simp only [add_zero, mul_zero] at this487 apply le_of_tendsto_of_tendsto tendsto_const_nhds this488 filter_upwards [self_mem_nhdsWithin]489 exact H490 -- fix a positive `ε`.491 intro ε εpos492 -- for small enough `r`, the rescaled ball `r • closedBall z ε` intersects `s`, as `x` is a493 -- density point494 have B₁ : ∀ᶠ r in 𝓝[>] (0 : ℝ), (s ∩ ({x} + r • closedBall z ε)).Nonempty :=495 eventually_nonempty_inter_smul_of_density_one μ s x hx _ measurableSet_closedBall496 (measure_closedBall_pos μ z εpos).ne'497 obtain ⟨ρ, ρpos, hρ⟩ :498 ∃ ρ > 0, ball x ρ ∩ s ⊆ {y : E | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖} :=499 mem_nhdsWithin_iff.1 ((hf' x xs).isLittleO.def εpos)500 -- for small enough `r`, the rescaled ball `r • closedBall z ε` is included in the set where501 -- `f y - f x` is well approximated by `f' x (y - x)`.502 have B₂ : ∀ᶠ r in 𝓝[>] (0 : ℝ), {x} + r • closedBall z ε ⊆ ball x ρ := by503 apply nhdsWithin_le_nhds504 exact eventually_singleton_add_smul_subset isBounded_closedBall (ball_mem_nhds x ρpos)505 -- fix a small positive `r` satisfying the above properties, as well as a corresponding `y`.506 obtain ⟨r, ⟨y, ⟨ys, hy⟩⟩, rρ, rpos⟩ :507 ∃ r : ℝ,508 (s ∩ ({x} + r • closedBall z ε)).Nonempty ∧ {x} + r • closedBall z ε ⊆ ball x ρ ∧ 0 < r :=509 (B₁.and (B₂.and self_mem_nhdsWithin)).exists510 -- write `y = x + r a` with `a ∈ closedBall z ε`.511 obtain ⟨a, az, ya⟩ : ∃ a, a ∈ closedBall z ε ∧ y = x + r • a := by512 simp only [mem_smul_set, image_add_left, mem_preimage, singleton_add] at hy513 rcases hy with ⟨a, az, ha⟩514 exact ⟨a, az, by simp only [ha, add_neg_cancel_left]⟩515 have norm_a : ‖a‖ ≤ ‖z‖ + ε :=516 calc517 ‖a‖ = ‖z + (a - z)‖ := by simp only [add_sub_cancel]518 _ ≤ ‖z‖ + ‖a - z‖ := norm_add_le _ _519 _ ≤ ‖z‖ + ε := by grw [mem_closedBall_iff_norm.1 az]520 -- use the approximation properties to control `(f' x - A) a`, and then `(f' x - A) z` as `z` is521 -- close to `a`.522 have I : r * ‖(f' x - A) a‖ ≤ r * (δ + ε) * (‖z‖ + ε) :=523 calc524 r * ‖(f' x - A) a‖ = ‖(f' x - A) (r • a)‖ := by525 simp only [map_smul, norm_smul, Real.norm_eq_abs, abs_of_nonneg rpos.le]526 _ = ‖f y - f x - A (y - x) - (f y - f x - (f' x) (y - x))‖ := by527 simp only [ya, add_sub_cancel_left, sub_sub_sub_cancel_left, FunLike.coe_sub,528 Pi.sub_apply, map_smul, smul_sub]529 _ ≤ ‖f y - f x - A (y - x)‖ + ‖f y - f x - (f' x) (y - x)‖ := norm_sub_le _ _530 _ ≤ δ * ‖y - x‖ + ε * ‖y - x‖ := (add_le_add (hf _ ys _ xs) (hρ ⟨rρ hy, ys⟩))531 _ = r * (δ + ε) * ‖a‖ := by532 simp only [ya, add_sub_cancel_left, norm_smul, Real.norm_eq_abs, abs_of_nonneg rpos.le]533 ring534 _ ≤ r * (δ + ε) * (‖z‖ + ε) := by gcongr535 calc536 ‖(f' x - A) z‖ = ‖(f' x - A) a + (f' x - A) (z - a)‖ := by537 congr 1538 simp only [FunLike.coe_sub, map_sub, Pi.sub_apply]539 abel540 _ ≤ ‖(f' x - A) a‖ + ‖(f' x - A) (z - a)‖ := norm_add_le _ _541 _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ := by542 apply add_le_add543 · rw [mul_assoc] at I; exact (mul_le_mul_iff_right₀ rpos).1 I544 · apply ContinuousLinearMap.le_opNorm545 _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε := by546 rw [mem_closedBall_iff_norm'] at az547 gcongr548549/-!550### Measure zero of the image, over non-measurable sets551552If a set has measure `0`, then its image under a differentiable map has measure zero. This doesn't553require the set to be measurable. In the same way, if `f` is differentiable on a set `s` with554non-invertible derivative everywhere, then `f '' s` has measure `0`, again without measurability555assumptions.556-/557558559/-- A differentiable function maps sets of measure zero to sets of measure zero. -/560theorem addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero (hf : DifferentiableOn ℝ f s)561 (hs : μ s = 0) : μ (f '' s) = 0 := by562 rw [← nonpos_iff_eq_zero]563 have :564 ∀ A : E →L[ℝ] E, ∃ δ : ℝ≥0, 0 < δ ∧565 ∀ (t : Set E), ApproximatesLinearOn f A t δ →566 μ (f '' t) ≤ (Real.toNNReal |A.det| + 1 : ℝ≥0) * μ t := by567 intro A568 let m : ℝ≥0 := Real.toNNReal |A.det| + 1569 have I : ENNReal.ofReal |A.det| < m := by570 simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, zero_lt_one, ENNReal.coe_lt_coe]571 rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩572 exact ⟨δ, h', fun t ht => h t f ht⟩573 choose δ hδ using this574 obtain ⟨t, A, _, _, t_cover, ht, -⟩ :575 ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),576 Pairwise (Disjoint on t) ∧577 (∀ n : ℕ, MeasurableSet (t n)) ∧578 (s ⊆ ⋃ n : ℕ, t n) ∧579 (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧580 (s.Nonempty → ∀ n, ∃ y ∈ s, A n = fderivWithin ℝ f s y) :=581 exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s (fderivWithin ℝ f s)582 (fun x xs => (hf x xs).hasFDerivWithinAt) δ fun A => (hδ A).1.ne'583 calc584 μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by585 apply measure_mono586 rw [← image_iUnion, ← inter_iUnion]587 exact Set.image_mono (subset_inter Subset.rfl t_cover)588 _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _589 _ ≤ ∑' n, (Real.toNNReal |(A n).det| + 1 : ℝ≥0) * μ (s ∩ t n) := by590 apply ENNReal.tsum_le_tsum fun n => ?_591 apply (hδ (A n)).2592 exact ht n593 _ ≤ ∑' n, ((Real.toNNReal |(A n).det| + 1 : ℝ≥0) : ℝ≥0∞) * 0 := by594 gcongr with n595 exact le_trans (measure_mono inter_subset_left) (le_of_eq hs)596 _ = 0 := by simp only [tsum_zero, mul_zero]597598/-- A version of **Sard's lemma** in fixed dimension: given a differentiable function from `E`599to `E` and a set where the differential is not invertible, then the image of this set has600zero measure. Here, we give an auxiliary statement towards this result. -/601theorem addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux602 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (R : ℝ) (hs : s ⊆ closedBall 0 R) (ε : ℝ≥0)603 (εpos : 0 < ε) (h'f' : ∀ x ∈ s, (f' x).det = 0) : μ (f '' s) ≤ ε * μ (closedBall 0 R) := by604 rcases eq_empty_or_nonempty s with (rfl | h's); · simp only [measure_empty, zero_le, image_empty]605 have :606 ∀ A : E →L[ℝ] E, ∃ δ : ℝ≥0, 0 < δ ∧607 ∀ (t : Set E), ApproximatesLinearOn f A t δ →608 μ (f '' t) ≤ (Real.toNNReal |A.det| + ε : ℝ≥0) * μ t := by609 intro A610 let m : ℝ≥0 := Real.toNNReal |A.det| + ε611 have I : ENNReal.ofReal |A.det| < m := by612 simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, ENNReal.coe_lt_coe]613 rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩614 exact ⟨δ, h', fun t ht => h t f ht⟩615 choose δ hδ using this616 obtain ⟨t, A, t_disj, t_meas, t_cover, ht, Af'⟩ :617 ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),618 Pairwise (Disjoint on t) ∧619 (∀ n : ℕ, MeasurableSet (t n)) ∧620 (s ⊆ ⋃ n : ℕ, t n) ∧621 (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧622 (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=623 exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'624 calc625 μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by626 rw [← image_iUnion, ← inter_iUnion]627 gcongr628 exact subset_inter Subset.rfl t_cover629 _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _630 _ ≤ ∑' n, (Real.toNNReal |(A n).det| + ε : ℝ≥0) * μ (s ∩ t n) := by631 gcongr632 exact (hδ (A _)).2 _ (ht _)633 _ = ∑' n, ε * μ (s ∩ t n) := by634 congr with n635 rcases Af' h's n with ⟨y, ys, hy⟩636 simp only [hy, h'f' y ys, Real.toNNReal_zero, abs_zero, zero_add]637 _ ≤ ε * ∑' n, μ (closedBall 0 R ∩ t n) := by638 rw [ENNReal.tsum_mul_left]639 gcongr640 _ = ε * μ (⋃ n, closedBall 0 R ∩ t n) := by641 rw [measure_iUnion]642 · exact pairwise_disjoint_mono t_disj fun n => inter_subset_right643 · intro n644 exact measurableSet_closedBall.inter (t_meas n)645 _ ≤ ε * μ (closedBall 0 R) := by grw [← inter_iUnion, inter_subset_left]646647/-- A version of Sard lemma in fixed dimension: given a differentiable function from `E` to `E` and648a set where the differential is not invertible, then the image of this set has zero measure. -/649theorem addHaar_image_eq_zero_of_det_fderivWithin_eq_zero650 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (h'f' : ∀ x ∈ s, (f' x).det = 0) :651 μ (f '' s) = 0 := by652 suffices H : ∀ R, μ (f '' (s ∩ closedBall 0 R)) = 0 by653 rw [← nonpos_iff_eq_zero, ← iUnion_inter_closedBall_nat s 0]654 calc655 μ (f '' ⋃ n : ℕ, s ∩ closedBall 0 n) ≤ ∑' n : ℕ, μ (f '' (s ∩ closedBall 0 n)) := by656 rw [image_iUnion]; exact measure_iUnion_le _657 _ ≤ 0 := by simp only [H, tsum_zero, nonpos_iff_eq_zero]658 intro R659 have A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ε * μ (closedBall 0 R) :=660 fun ε εpos =>661 addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux μ662 (fun x hx => (hf' x hx.1).mono inter_subset_left) R inter_subset_right ε εpos663 fun x hx => h'f' x hx.1664 have B : Tendsto (fun ε : ℝ≥0 => (ε : ℝ≥0∞) * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0) := by665 have :666 Tendsto (fun ε : ℝ≥0 => (ε : ℝ≥0∞) * μ (closedBall 0 R)) (𝓝 0)667 (𝓝 (((0 : ℝ≥0) : ℝ≥0∞) * μ (closedBall 0 R))) :=668 ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 tendsto_id)669 (Or.inr measure_closedBall_lt_top.ne)670 simp only [zero_mul, ENNReal.coe_zero] at this671 exact Tendsto.mono_left this nhdsWithin_le_nhds672 rw [← nonpos_iff_eq_zero]673 apply ge_of_tendsto B674 filter_upwards [self_mem_nhdsWithin]675 exact A676677/-!678### Weak measurability statements679680We show that the derivative of a function on a set is almost everywhere measurable, and that the681image `f '' s` is measurable if `f` is injective on `s`. The latter statement follows from the682Lusin-Souslin theorem.683-/684685686/-- The derivative of a function on a measurable set is almost everywhere measurable on this set687with respect to Lebesgue measure. Note that, in general, it is not genuinely measurable there,688as `f'` is not unique (but only on a set of measure `0`, as the argument shows). -/689theorem aemeasurable_fderivWithin (hs : MeasurableSet s)690 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) : AEMeasurable f' (μ.restrict s) := by691 /- It suffices to show that `f'` can be uniformly approximated by a measurable function.692 Fix `ε > 0`. Thanks to `exists_partition_approximatesLinearOn_of_hasFDerivWithinAt`, one693 can find a countable measurable partition of `s` into sets `s ∩ t n` on which `f` is well694 approximated by linear maps `A n`. On almost all of `s ∩ t n`, it follows from695 `ApproximatesLinearOn.norm_fderiv_sub_le` that `f'` is uniformly approximated by `A n`, which696 gives the conclusion. -/697 -- fix a precision `ε`698 refine aemeasurable_of_unif_approx fun ε εpos => ?_699 let δ : ℝ≥0 := ⟨ε, le_of_lt εpos⟩700 have δpos : 0 < δ := εpos701 -- partition `s` into sets `s ∩ t n` on which `f` is approximated by linear maps `A n`.702 obtain ⟨t, A, t_disj, t_meas, t_cover, ht, _⟩ :703 ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),704 Pairwise (Disjoint on t) ∧705 (∀ n : ℕ, MeasurableSet (t n)) ∧706 (s ⊆ ⋃ n : ℕ, t n) ∧707 (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) δ) ∧708 (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=709 exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' (fun _ => δ) fun _ =>710 δpos.ne'711 -- define a measurable function `g` which coincides with `A n` on `t n`.712 obtain ⟨g, g_meas, hg⟩ :713 ∃ g : E → E →L[ℝ] E, Measurable g ∧ ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n :=714 exists_measurable_piecewise t t_meas (fun n _ => A n) (fun n => measurable_const) <|715 t_disj.mono fun i j h => by simp only [h.inter_eq, eqOn_empty]716 refine ⟨g, g_meas.aemeasurable, ?_⟩717 -- reduce to checking that `f'` and `g` are close on almost all of `s ∩ t n`, for all `n`.718 suffices H : ∀ᵐ x : E ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε by719 have : μ.restrict s ≤ sum fun n => μ.restrict (s ∩ t n) := by720 have : s = ⋃ n, s ∩ t n := by721 rw [← inter_iUnion]722 exact Subset.antisymm (subset_inter Subset.rfl t_cover) inter_subset_left723 conv_lhs => rw [this]724 exact restrict_iUnion_le725 exact ae_mono this H726 -- fix such an `n`.727 refine ae_sum_iff.2 fun n => ?_728 -- on almost all `s ∩ t n`, `f' x` is close to `A n` thanks to729 -- `ApproximatesLinearOn.norm_fderiv_sub_le`.730 have E₁ : ∀ᵐ x : E ∂μ.restrict (s ∩ t n), ‖f' x - A n‖₊ ≤ δ :=731 (ht n).norm_fderiv_sub_le μ (hs.inter (t_meas n)) f' fun x hx =>732 (hf' x hx.1).mono inter_subset_left733 -- moreover, `g x` is equal to `A n` there.734 have E₂ : ∀ᵐ x : E ∂μ.restrict (s ∩ t n), g x = A n := by735 suffices H : ∀ᵐ x : E ∂μ.restrict (t n), g x = A n from736 ae_mono (restrict_mono inter_subset_right le_rfl) H737 filter_upwards [ae_restrict_mem (t_meas n)]738 exact hg n739 -- putting these two properties together gives the conclusion.740 filter_upwards [E₁, E₂] with x hx1 hx2741 rw [← nndist_eq_nnnorm] at hx1742 rw [hx2, dist_comm]743 exact hx1744745theorem aemeasurable_ofReal_abs_det_fderivWithin (hs : MeasurableSet s)746 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :747 AEMeasurable (fun x => ENNReal.ofReal |(f' x).det|) (μ.restrict s) := by748 apply ENNReal.measurable_ofReal.comp_aemeasurable749 refine continuous_abs.measurable.comp_aemeasurable ?_750 refine ContinuousLinearMap.continuous_det.measurable.comp_aemeasurable ?_751 exact aemeasurable_fderivWithin μ hs hf'752753theorem aemeasurable_toNNReal_abs_det_fderivWithin (hs : MeasurableSet s)754 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :755 AEMeasurable (fun x => |(f' x).det|.toNNReal) (μ.restrict s) := by756 apply measurable_real_toNNReal.comp_aemeasurable757 refine continuous_abs.measurable.comp_aemeasurable ?_758 refine ContinuousLinearMap.continuous_det.measurable.comp_aemeasurable ?_759 exact aemeasurable_fderivWithin μ hs hf'760761/-- If a function is differentiable and injective on a measurable set,762then the image is measurable. -/763theorem measurable_image_of_fderivWithin (hs : MeasurableSet s)764 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) : MeasurableSet (f '' s) :=765 haveI : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt766 hs.image_of_continuousOn_injOn (DifferentiableOn.continuousOn this) hf767768/-- If a function is differentiable and injective on a null measurable set,769then the image is null measurable. -/770theorem nullMeasurable_image_of_fderivWithin (hs : NullMeasurableSet s μ)771 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :772 NullMeasurableSet (f '' s) μ := by773 rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩774 have A : f '' s =ᵐ[μ] f '' t := by775 have : s = t ∪ (s \ t) := by simp [union_eq_self_of_subset_left ts]776 rw [this, image_union]777 refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)778 apply addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero _779 (fun x hx ↦ ?_) (ae_eq_set.1 t_eq_s).2780 exact (hf' x hx.1).differentiableWithinAt.mono sdiff_subset781 apply NullMeasurableSet.congr _ A.symm782 apply MeasurableSet.nullMeasurableSet783 apply measurable_image_of_fderivWithin ht _ (hf.mono ts) (f' := f')784 intro x hx785 exact (hf' x (ts hx)).mono ts786787/-- If a function is differentiable and injective on a measurable set `s`, then its restriction788to `s` is a measurable embedding. -/789theorem measurableEmbedding_of_fderivWithin (hs : MeasurableSet s)790 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :791 MeasurableEmbedding (s.restrict f) :=792 haveI : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt793 this.continuousOn.measurableEmbedding hs hf794795/-!796### Proving the estimate for the measure of the image797798We show the formula `∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ = μ (f '' s)`,799in `lintegral_abs_det_fderiv_eq_addHaar_image`. For this, we show both inequalities in both800directions, first up to controlled errors and then letting these errors tend to `0`.801-/802803804theorem addHaar_image_le_lintegral_abs_det_fderiv_aux1 (hs : MeasurableSet s)805 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) {ε : ℝ≥0} (εpos : 0 < ε) :806 μ (f '' s) ≤ (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * ε * μ s := by807 /- To bound `μ (f '' s)`, we cover `s` by sets where `f` is well-approximated by linear maps808 `A n` (and where `f'` is almost everywhere close to `A n`), and then use that `f` expands the809 measure of such a set by at most `(A n).det + ε`. -/810 have :811 ∀ A : E →L[ℝ] E,812 ∃ δ : ℝ≥0,813 0 < δ ∧814 (∀ B : E →L[ℝ] E, ‖B - A‖ ≤ δ → |B.det - A.det| ≤ ε) ∧815 ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t δ →816 μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ε) * μ t := by817 intro A818 let m : ℝ≥0 := Real.toNNReal |A.det| + ε819 have I : ENNReal.ofReal |A.det| < m := by820 simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, ENNReal.coe_lt_coe]821 rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, δpos⟩822 obtain ⟨δ', δ'pos, hδ'⟩ : ∃ (δ' : ℝ), 0 < δ' ∧ ∀ B, dist B A < δ' → dist B.det A.det < ↑ε := by823 refine continuousAt_iff.1 ?_ ε εpos824 exact ContinuousLinearMap.continuous_det.continuousAt825 let δ'' : ℝ≥0 := ⟨δ' / 2, (half_pos δ'pos).le⟩826 refine ⟨min δ δ'', lt_min δpos (half_pos δ'pos), ?_, ?_⟩827 · intro B hB828 rw [← Real.dist_eq]829 apply (hδ' B _).le830 rw [dist_eq_norm]831 calc832 ‖B - A‖ ≤ (min δ δ'' : ℝ≥0) := hB833 _ ≤ δ'' := by simp only [le_refl, NNReal.coe_min, min_le_iff, or_true]834 _ < δ' := half_lt_self δ'pos835 · intro t g htg836 exact h t g (htg.mono_num (min_le_left _ _))837 choose δ hδ using this838 obtain ⟨t, A, t_disj, t_meas, t_cover, ht, -⟩ :839 ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),840 Pairwise (Disjoint on t) ∧841 (∀ n : ℕ, MeasurableSet (t n)) ∧842 (s ⊆ ⋃ n : ℕ, t n) ∧843 (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧844 (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=845 exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'846 calc847 μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by848 apply measure_mono849 rw [← image_iUnion, ← inter_iUnion]850 exact Set.image_mono (subset_inter Subset.rfl t_cover)851 _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _852 _ ≤ ∑' n, (ENNReal.ofReal |(A n).det| + ε) * μ (s ∩ t n) := by853 apply ENNReal.tsum_le_tsum fun n => ?_854 apply (hδ (A n)).2.2855 exact ht n856 _ = ∑' n, ∫⁻ _ in s ∩ t n, ENNReal.ofReal |(A n).det| + ε ∂μ := by857 simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]858 _ ≤ ∑' n, ∫⁻ x in s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * ε ∂μ := by859 apply ENNReal.tsum_le_tsum fun n => ?_860 apply lintegral_mono_ae861 filter_upwards [(ht n).norm_fderiv_sub_le μ (hs.inter (t_meas n)) f' fun x hx =>862 (hf' x hx.1).mono inter_subset_left]863 intro x hx864 have I : |(A n).det| ≤ |(f' x).det| + ε :=865 calc866 |(A n).det| = |(f' x).det - ((f' x).det - (A n).det)| := by congr 1; abel867 _ ≤ |(f' x).det| + |(f' x).det - (A n).det| := abs_sub _ _868 _ ≤ |(f' x).det| + ε := add_le_add le_rfl ((hδ (A n)).2.1 _ hx)869 calc870 ENNReal.ofReal |(A n).det| + ε ≤ ENNReal.ofReal (|(f' x).det| + ε) + ε := by gcongr871 _ = ENNReal.ofReal |(f' x).det| + 2 * ε := by872 simp only [ENNReal.ofReal_add, abs_nonneg, two_mul, add_assoc, NNReal.zero_le_coe,873 ENNReal.ofReal_coe_nnreal]874 _ = ∫⁻ x in ⋃ n, s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * ε ∂μ := by875 have M : ∀ n : ℕ, MeasurableSet (s ∩ t n) := fun n => hs.inter (t_meas n)876 rw [lintegral_iUnion M]877 exact pairwise_disjoint_mono t_disj fun n => inter_subset_right878 _ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| + 2 * ε ∂μ := by879 rw [← inter_iUnion, inter_eq_self_of_subset_left t_cover]880 _ = (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * ε * μ s := by881 simp only [lintegral_add_right' _ aemeasurable_const, setLIntegral_const]882883theorem addHaar_image_le_lintegral_abs_det_fderiv_aux2 (hs : MeasurableSet s) (h's : μ s ≠ ∞)884 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :885 μ (f '' s) ≤ ∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ := by886 -- We just need to let the error tend to `0` in the previous lemma.887 have :888 Tendsto (fun ε : ℝ≥0 => (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * ε * μ s) (𝓝[>] 0)889 (𝓝 ((∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * (0 : ℝ≥0) * μ s)) := by890 apply Tendsto.mono_left _ nhdsWithin_le_nhds891 refine tendsto_const_nhds.add ?_892 refine ENNReal.Tendsto.mul_const ?_ (Or.inr h's)893 exact ENNReal.Tendsto.const_mul (ENNReal.tendsto_coe.2 tendsto_id) (Or.inr ENNReal.coe_ne_top)894 simp only [add_zero, zero_mul, mul_zero, ENNReal.coe_zero] at this895 apply ge_of_tendsto this896 filter_upwards [self_mem_nhdsWithin]897 intro ε εpos898 rw [mem_Ioi] at εpos899 exact addHaar_image_le_lintegral_abs_det_fderiv_aux1 μ hs hf' εpos900901theorem addHaar_image_le_lintegral_abs_det_fderiv (hs : MeasurableSet s)902 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :903 μ (f '' s) ≤ ∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ := by904 /- We already know the result for finite-measure sets. We cover `s` by finite-measure sets using905 `spanningSets μ`, and apply the previous result to each of these parts. -/906 let u n := disjointed (spanningSets μ) n907 have u_meas : ∀ n, MeasurableSet (u n) := by908 intro n909 apply MeasurableSet.disjointed fun i => ?_910 exact measurableSet_spanningSets μ i911 have A : s = ⋃ n, s ∩ u n := by912 rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]913 calc914 μ (f '' s) ≤ ∑' n, μ (f '' (s ∩ u n)) := by915 conv_lhs => rw [A, image_iUnion]916 exact measure_iUnion_le _917 _ ≤ ∑' n, ∫⁻ x in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ := by918 apply ENNReal.tsum_le_tsum fun n => ?_919 apply920 addHaar_image_le_lintegral_abs_det_fderiv_aux2 μ (hs.inter (u_meas n)) _ fun x hx =>921 (hf' x hx.1).mono inter_subset_left922 have : μ (u n) < ∞ :=923 lt_of_le_of_lt (measure_mono (disjointed_subset _ _)) (measure_spanningSets_lt_top μ n)924 exact ne_of_lt (lt_of_le_of_lt (measure_mono inter_subset_right) this)925 _ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ := by926 conv_rhs => rw [A]927 rw [lintegral_iUnion]928 · intro n; exact hs.inter (u_meas n)929 · exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right930931theorem lintegral_abs_det_fderiv_le_addHaar_image_aux1 (hs : MeasurableSet s)932 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) {ε : ℝ≥0} (εpos : 0 < ε) :933 (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) ≤ μ (f '' s) + 2 * ε * μ s := by934 /- To bound `∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ`, we cover `s` by sets where `f` is935 well-approximated by linear maps `A n` (and where `f'` is almost everywhere close to `A n`),936 and then use that `f` expands the measure of such a set by at least `(A n).det - ε`. -/937 have :938 ∀ A : E →L[ℝ] E,939 ∃ δ : ℝ≥0,940 0 < δ ∧941 (∀ B : E →L[ℝ] E, ‖B - A‖ ≤ δ → |B.det - A.det| ≤ ε) ∧942 ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t δ →943 ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ε * μ t := by944 intro A945 obtain ⟨δ', δ'pos, hδ'⟩ : ∃ (δ' : ℝ), 0 < δ' ∧ ∀ B, dist B A < δ' → dist B.det A.det < ↑ε := by946 refine continuousAt_iff.1 ?_ ε εpos947 exact ContinuousLinearMap.continuous_det.continuousAt948 let δ'' : ℝ≥0 := ⟨δ' / 2, (half_pos δ'pos).le⟩949 have I'' : ∀ B : E →L[ℝ] E, ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε := by950 intro B hB951 rw [← Real.dist_eq]952 apply (hδ' B _).le953 rw [dist_eq_norm]954 exact hB.trans_lt (half_lt_self δ'pos)955 rcases eq_or_ne A.det 0 with (hA | hA)956 · refine ⟨δ'', half_pos δ'pos, I'', ?_⟩957 simp only [hA, forall_const, zero_mul, ENNReal.ofReal_zero, imp_true_iff,958 zero_le, abs_zero]959 let m : ℝ≥0 := Real.toNNReal |A.det| - ε960 have I : (m : ℝ≥0∞) < ENNReal.ofReal |A.det| := by961 simp only [m, ENNReal.ofReal, ENNReal.coe_sub]962 apply ENNReal.sub_lt_self ENNReal.coe_ne_top963 · simpa only [abs_nonpos_iff, Real.toNNReal_eq_zero, ENNReal.coe_eq_zero, Ne] using hA964 · simp only [εpos.ne', ENNReal.coe_eq_zero, Ne, not_false_iff]965 rcases ((mul_le_addHaar_image_of_lt_det μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, δpos⟩966 refine ⟨min δ δ'', lt_min δpos (half_pos δ'pos), ?_, ?_⟩967 · intro B hB968 apply I'' _ (hB.trans _)969 simp only [le_refl, NNReal.coe_min, min_le_iff, or_true]970 · intro t g htg971 rcases eq_or_ne (μ t) ∞ with (ht | ht)972 · simp only [ht, εpos.ne', ENNReal.mul_top, ENNReal.coe_eq_zero, le_top, Ne,973 not_false_iff, _root_.add_top]974 have := h t g (htg.mono_num (min_le_left _ _))975 rwa [ENNReal.coe_sub, ENNReal.sub_mul, tsub_le_iff_right] at this976 simp only [ht, imp_true_iff, Ne, not_false_iff]977 choose δ hδ using this978 obtain ⟨t, A, t_disj, t_meas, t_cover, ht, -⟩ :979 ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),980 Pairwise (Disjoint on t) ∧981 (∀ n : ℕ, MeasurableSet (t n)) ∧982 (s ⊆ ⋃ n : ℕ, t n) ∧983 (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧984 (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=985 exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'986 have s_eq : s = ⋃ n, s ∩ t n := by987 rw [← inter_iUnion]988 exact Subset.antisymm (subset_inter Subset.rfl t_cover) inter_subset_left989 calc990 (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) =991 ∑' n, ∫⁻ x in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ := by992 conv_lhs => rw [s_eq]993 rw [lintegral_iUnion]994 · exact fun n => hs.inter (t_meas n)995 · exact pairwise_disjoint_mono t_disj fun n => inter_subset_right996 _ ≤ ∑' n, ∫⁻ _ in s ∩ t n, ENNReal.ofReal |(A n).det| + ε ∂μ := by997 apply ENNReal.tsum_le_tsum fun n => ?_998 apply lintegral_mono_ae999 filter_upwards [(ht n).norm_fderiv_sub_le μ (hs.inter (t_meas n)) f' fun x hx =>1000 (hf' x hx.1).mono inter_subset_left]1001 intro x hx1002 have I : |(f' x).det| ≤ |(A n).det| + ε :=1003 calc1004 |(f' x).det| = |(A n).det + ((f' x).det - (A n).det)| := by congr 1; abel1005 _ ≤ |(A n).det| + |(f' x).det - (A n).det| := abs_add_le _ _1006 _ ≤ |(A n).det| + ε := add_le_add le_rfl ((hδ (A n)).2.1 _ hx)1007 calc1008 ENNReal.ofReal |(f' x).det| ≤ ENNReal.ofReal (|(A n).det| + ε) :=1009 ENNReal.ofReal_le_ofReal I1010 _ = ENNReal.ofReal |(A n).det| + ε := by1011 simp only [ENNReal.ofReal_add, abs_nonneg, NNReal.zero_le_coe, ENNReal.ofReal_coe_nnreal]1012 _ = ∑' n, (ENNReal.ofReal |(A n).det| * μ (s ∩ t n) + ε * μ (s ∩ t n)) := by1013 simp only [setLIntegral_const, lintegral_add_right _ measurable_const]1014 _ ≤ ∑' n, (μ (f '' (s ∩ t n)) + ε * μ (s ∩ t n) + ε * μ (s ∩ t n)) := by1015 gcongr1016 exact (hδ (A _)).2.2 _ _ (ht _)1017 _ = μ (f '' s) + 2 * ε * μ s := by1018 conv_rhs => rw [s_eq]1019 rw [image_iUnion, measure_iUnion]; rotate_left1020 · intro i j hij1021 apply Disjoint.image _ hf inter_subset_left inter_subset_left1022 exact Disjoint.mono inter_subset_right inter_subset_right (t_disj hij)1023 · intro i1024 exact1025 measurable_image_of_fderivWithin (hs.inter (t_meas i))1026 (fun x hx => (hf' x hx.1).mono inter_subset_left)1027 (hf.mono inter_subset_left)1028 rw [measure_iUnion]; rotate_left1029 · exact pairwise_disjoint_mono t_disj fun i => inter_subset_right1030 · exact fun i => hs.inter (t_meas i)1031 rw [← ENNReal.tsum_mul_left, ← ENNReal.tsum_add]1032 congr 11033 ext1 i1034 rw [mul_assoc, two_mul, add_assoc]10351036theorem lintegral_abs_det_fderiv_le_addHaar_image_aux2 (hs : MeasurableSet s) (h's : μ s ≠ ∞)1037 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :1038 (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) ≤ μ (f '' s) := by1039 -- We just need to let the error tend to `0` in the previous lemma.1040 have :1041 Tendsto (fun ε : ℝ≥0 => μ (f '' s) + 2 * ε * μ s) (𝓝[>] 0)1042 (𝓝 (μ (f '' s) + 2 * (0 : ℝ≥0) * μ s)) := by1043 apply Tendsto.mono_left _ nhdsWithin_le_nhds1044 refine tendsto_const_nhds.add ?_1045 refine ENNReal.Tendsto.mul_const ?_ (Or.inr h's)1046 exact ENNReal.Tendsto.const_mul (ENNReal.tendsto_coe.2 tendsto_id) (Or.inr ENNReal.coe_ne_top)1047 simp only [add_zero, zero_mul, mul_zero, ENNReal.coe_zero] at this1048 apply ge_of_tendsto this1049 filter_upwards [self_mem_nhdsWithin]1050 intro ε εpos1051 rw [mem_Ioi] at εpos1052 exact lintegral_abs_det_fderiv_le_addHaar_image_aux1 μ hs hf' hf εpos10531054theorem lintegral_abs_det_fderiv_le_addHaar_image (hs : MeasurableSet s)1055 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :1056 (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) ≤ μ (f '' s) := by1057 /- We already know the result for finite-measure sets. We cover `s` by finite-measure sets using1058 `spanningSets μ`, and apply the previous result to each of these parts. -/1059 let u n := disjointed (spanningSets μ) n1060 have u_meas : ∀ n, MeasurableSet (u n) := by1061 intro n1062 apply MeasurableSet.disjointed fun i => ?_1063 exact measurableSet_spanningSets μ i1064 have A : s = ⋃ n, s ∩ u n := by1065 rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]1066 calc1067 (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) =1068 ∑' n, ∫⁻ x in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ := by1069 conv_lhs => rw [A]1070 rw [lintegral_iUnion]1071 · intro n; exact hs.inter (u_meas n)1072 · exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right1073 _ ≤ ∑' n, μ (f '' (s ∩ u n)) := by1074 apply ENNReal.tsum_le_tsum fun n => ?_1075 apply1076 lintegral_abs_det_fderiv_le_addHaar_image_aux2 μ (hs.inter (u_meas n)) _1077 (fun x hx => (hf' x hx.1).mono inter_subset_left) (hf.mono inter_subset_left)1078 have : μ (u n) < ∞ :=1079 lt_of_le_of_lt (measure_mono (disjointed_subset _ _)) (measure_spanningSets_lt_top μ n)1080 exact ne_of_lt (lt_of_le_of_lt (measure_mono inter_subset_right) this)1081 _ = μ (f '' s) := by1082 conv_rhs => rw [A, image_iUnion]1083 rw [measure_iUnion]1084 · intro i j hij1085 apply Disjoint.image _ hf inter_subset_left inter_subset_left1086 exact1087 Disjoint.mono inter_subset_right inter_subset_right1088 (disjoint_disjointed _ hij)1089 · intro i1090 exact1091 measurable_image_of_fderivWithin (hs.inter (u_meas i))1092 (fun x hx => (hf' x hx.1).mono inter_subset_left)1093 (hf.mono inter_subset_left)10941095/-- Change of variable formula for differentiable functions, set version: if a function `f` is1096injective and differentiable on a measurable set `s`, then the measure of `f '' s` is given by the1097integral of `|(f' x).det|` on `s`.1098Note that the measurability of `f '' s` is given by `measurable_image_of_fderivWithin`. -/1099theorem lintegral_abs_det_fderiv_eq_addHaar_image (hs : MeasurableSet s)1100 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :1101 (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) = μ (f '' s) :=1102 le_antisymm (lintegral_abs_det_fderiv_le_addHaar_image μ hs hf' hf)1103 (addHaar_image_le_lintegral_abs_det_fderiv μ hs hf')11041105/-- Change of variable formula for differentiable functions, set version: if a function `f` is1106injective and differentiable on a null measurable set `s`, then the measure of `f '' s` is given1107by the integral of `|(f' x).det|` on `s`.1108Note that the null-measurability of `f '' s` is given by `nullMeasurable_image_of_fderivWithin`. -/1109theorem lintegral_abs_det_fderiv_eq_addHaar_image₀ (hs : NullMeasurableSet s μ)1110 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :1111 (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) = μ (f '' s) := by1112 rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩1113 have A : μ (f '' s) = μ (f '' t) := by1114 apply measure_congr1115 have : s = t ∪ (s \ t) := by simp [union_eq_self_of_subset_left ts]1116 rw [this, image_union]1117 refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)1118 apply addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero _1119 (fun x hx ↦ ?_) (ae_eq_set.1 t_eq_s).21120 exact (hf' x hx.1).differentiableWithinAt.mono sdiff_subset1121 have B : (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ)1122 = (∫⁻ x in t, ENNReal.ofReal |(f' x).det| ∂μ) :=1123 setLIntegral_congr t_eq_s.symm1124 rw [A, B, lintegral_abs_det_fderiv_eq_addHaar_image _ ht _ (hf.mono ts)]1125 intro x hx1126 exact (hf' x (ts hx)).mono ts11271128/-- Change of variable formula for differentiable functions, set version: if a function `f` is1129injective and differentiable on a null measurable set `s`, then the pushforward of the measure with1130density `|(f' x).det|` on `s` is the Lebesgue measure on the image set. -/1131theorem map_withDensity_abs_det_fderiv_eq_addHaar (hs : NullMeasurableSet s μ)1132 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :1133 Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) =1134 μ.restrict (f '' s) := by1135 have h'f : AEMeasurable f (μ.restrict s) := by1136 apply ContinuousOn.aemeasurable₀ (fun x hx ↦ ?_) hs1137 exact (hf' x hx).differentiableWithinAt.continuousWithinAt1138 have h''f : AEMeasurable f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) := by1139 apply h'f.mono_ac1140 exact withDensity_absolutelyContinuous _ _1141 apply Measure.ext fun t ht => ?_1142 have h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s) := h'f.nullMeasurableSet_preimage ht1143 rw [map_apply_of_aemeasurable h''f ht, withDensity_apply₀ _ h't,1144 Measure.restrict_apply ht, restrict_restrict₀ h't,1145 lintegral_abs_det_fderiv_eq_addHaar_image₀ μ ((nullMeasurableSet_restrict hs).1 h't)1146 (fun x hx => (hf' x hx.2).mono inter_subset_right) (hf.mono inter_subset_right),1147 image_preimage_inter]11481149/-- Change of variable formula for differentiable functions, set version: if a function `f` is1150injective and differentiable on a measurable set `s`, then the pushforward of the measure with1151density `|(f' x).det|` on `s` is the Lebesgue measure on the image set. This version is expressed1152in terms of the restricted function `s.restrict f`.1153For a version for the original function, see `map_withDensity_abs_det_fderiv_eq_addHaar`.1154-/1155theorem restrict_map_withDensity_abs_det_fderiv_eq_addHaar (hs : MeasurableSet s)1156 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :1157 Measure.map (s.restrict f) (comap (↑) (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) =1158 μ.restrict (f '' s) := by1159 obtain ⟨u, u_meas, uf⟩ : ∃ u, Measurable u ∧ EqOn u f s := by1160 classical1161 refine ⟨piecewise s f 0, ?_, piecewise_eqOn _ _ _⟩1162 refine ContinuousOn.measurable_piecewise ?_ continuous_zero.continuousOn hs1163 have : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt1164 exact this.continuousOn1165 have u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x := fun x hx =>1166 (hf' x hx).congr (fun y hy => uf hy) (uf hx)1167 set F : s → E := u ∘ (↑) with hF1168 have A :1169 Measure.map F (comap (↑) (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) =1170 μ.restrict (u '' s) := by1171 rw [hF, ← Measure.map_map u_meas measurable_subtype_coe, map_comap_subtype_coe hs,1172 restrict_withDensity hs]1173 exact map_withDensity_abs_det_fderiv_eq_addHaar μ hs.nullMeasurableSet u' (hf.congr uf.symm)1174 rw [uf.image_eq] at A1175 have : F = s.restrict f := by1176 ext x1177 exact uf x.21178 rwa [this] at A11791180/-! ### Change of variable formulas in integrals -/118111821183/-- Change of variable formula for differentiable functions: if a function `f` is1184injective and differentiable on a measurable set `s`, then the Lebesgue integral of a function1185`g : E → ℝ≥0∞` on `f '' s` coincides with the integral of `|(f' x).det| * g ∘ f` on `s`.1186Note that the measurability of `f '' s` is given by `measurable_image_of_fderivWithin`. -/1187theorem lintegral_image_eq_lintegral_abs_det_fderiv_mul (hs : MeasurableSet s)1188 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) (g : E → ℝ≥0∞) :1189 ∫⁻ x in f '' s, g x ∂μ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ := by1190 rw [← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,1191 (measurableEmbedding_of_fderivWithin hs hf' hf).lintegral_map]1192 simp only [Set.restrict_apply, ← Function.comp_apply (f := g)]1193 rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs,1194 setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]1195 · simp only [Pi.mul_apply]1196 · simp only [eventually_true, ENNReal.ofReal_lt_top]1197 · exact aemeasurable_ofReal_abs_det_fderivWithin μ hs hf'11981199/-- Integrability in the change of variable formula for differentiable functions: if a1200function `f` is injective and differentiable on a measurable set `s`, then a function1201`g : E → F` is integrable on `f '' s` if and only if `|(f' x).det| • g ∘ f` is1202integrable on `s`. -/1203theorem integrableOn_image_iff_integrableOn_abs_det_fderiv_smul (hs : MeasurableSet s)1204 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) (g : E → F) :1205 IntegrableOn g (f '' s) μ ↔ IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ := by1206 rw [IntegrableOn, ← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,1207 (measurableEmbedding_of_fderivWithin hs hf' hf).integrable_map_iff]1208 simp only [Set.restrict_eq, ← Function.comp_assoc, ENNReal.ofReal]1209 rw [← (MeasurableEmbedding.subtype_coe hs).integrable_map_iff, map_comap_subtype_coe hs,1210 restrict_withDensity hs, integrable_withDensity_iff_integrable_coe_smul₀]1211 · simp_rw [IntegrableOn, Real.coe_toNNReal _ (abs_nonneg _), Function.comp_apply]1212 · exact aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf'12131214/-- Change of variable formula for differentiable functions: if a function `f` is1215injective and differentiable on a measurable set `s`, then the Bochner integral of a function1216`g : E → F` on `f '' s` coincides with the integral of `|(f' x).det| • g ∘ f` on `s`. -/1217theorem integral_image_eq_integral_abs_det_fderiv_smul (hs : MeasurableSet s)1218 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) (g : E → F) :1219 ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ := by1220 rw [← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,1221 (measurableEmbedding_of_fderivWithin hs hf' hf).integral_map]1222 simp only [Set.restrict_apply, ← Function.comp_apply (f := g), ENNReal.ofReal]1223 rw [← (MeasurableEmbedding.subtype_coe hs).integral_map, map_comap_subtype_coe hs,1224 setIntegral_withDensity_eq_setIntegral_smul₀1225 (aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf') _ hs]1226 congr with x1227 rw [NNReal.smul_def, Real.coe_toNNReal _ (abs_nonneg (f' x).det)]12281229theorem integral_target_eq_integral_abs_det_fderiv_smul {f : OpenPartialHomeomorph E E}1230 (hf' : ∀ x ∈ f.source, HasFDerivAt f (f' x) x) (g : E → F) :1231 ∫ x in f.target, g x ∂μ = ∫ x in f.source, |(f' x).det| • g (f x) ∂μ := by1232 have : f '' f.source = f.target := PartialEquiv.image_source_eq_target f.toPartialEquiv1233 rw [← this]1234 apply integral_image_eq_integral_abs_det_fderiv_smul μ f.open_source.measurableSet _ f.injOn1235 intro x hx1236 exact (hf' x hx).hasFDerivWithinAt12371238section withDensity12391240lemma _root_.MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul1241 (hs : MeasurableSet s) (hf : MeasurableEmbedding f)1242 {g : E → ℝ} (hg : ∀ᵐ x ∂μ, x ∈ f '' s → 0 ≤ g x) (hg_int : IntegrableOn g (f '' s) μ)1243 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :1244 (μ.withDensity (fun x ↦ ENNReal.ofReal (g x))).comap f s1245 = ENNReal.ofReal (∫ x in s, |(f' x).det| * g (f x) ∂μ) := by1246 rw [Measure.comap_apply f hf.injective (fun t ht ↦ hf.measurableSet_image' ht) _ hs,1247 withDensity_apply _ (hf.measurableSet_image' hs),1248 ← ofReal_integral_eq_lintegral_ofReal hg_int1249 ((ae_restrict_iff' (hf.measurableSet_image' hs)).mpr hg),1250 integral_image_eq_integral_abs_det_fderiv_smul μ hs hf' hf.injective.injOn]1251 simp_rw [smul_eq_mul]12521253lemma _root_.MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul1254 (hs : MeasurableSet s) (f : E ≃ᵐ E)1255 {g : E → ℝ} (hg : ∀ᵐ x ∂μ, x ∈ f '' s → 0 ≤ g x) (hg_int : IntegrableOn g (f '' s) μ)1256 (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :1257 (μ.withDensity (fun x ↦ ENNReal.ofReal (g x))).map f.symm s1258 = ENNReal.ofReal (∫ x in s, |(f' x).det| * g (f x) ∂μ) := by1259 rw [MeasurableEquiv.map_symm,1260 MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul μ hs1261 f.measurableEmbedding hg hg_int hf']12621263end withDensity12641265end MeasureTheory