Exact source: MathlibAnnex/Analysis/Calculus/BilipschitzOrientation/Basic.lean
Pinned GitHub source · Raw UTF-8 source
Back to Inverse maps on open sets with global metric bounds
1import MathlibAnnex.Analysis.Normed.Operator.Determinant2import Mathlib.MeasureTheory.Function.Jacobian3import Mathlib.MeasureTheory.Measure.Hausdorff4import Mathlib.Analysis.Calculus.Rademacher5import Mathlib.Analysis.Calculus.FDeriv.Comp6import Mathlib.Topology.MetricSpace.Antilipschitz7import Mathlib.Tactic89/-!10# Degree-free orientation for global bi-Lipschitz data: basic layer1112This candidate isolates the absolute-area-formula part of the argument. It is13intentionally written on the standard finite Pi space used by Mathlib's14Jacobian theorem. Source and target connectedness are not fields of the data:15no connectivity is needed for signed transfer, and target preconnectedness is16supplied only at the later constancy theorem.1718This browser-produced source is a proof seed. Its returned status remains19`HANDWRITTEN_UNBUILT` until the exact local Lean lane elaborates and qualifies20it.21-/2223noncomputable section2425open Set MeasureTheory Filter26open scoped ENNReal NNReal Topology2728namespace MathlibAnnex29namespace BilipschitzOrientation3031/-- Global equal-dimensional open-set bi-Lipschitz data. The explicit32`LipschitzWith` constants avoid a route-local existential Lipschitz wrapper.33Connectivity is deliberately not stored here. -/34structure BiLipschitzOpenData (n : ℕ) where35 source : Set (Fin n → ℝ)36 target : Set (Fin n → ℝ)37 isOpen_source : IsOpen source38 isOpen_target : IsOpen target39 f : (Fin n → ℝ) → (Fin n → ℝ)40 g : (Fin n → ℝ) → (Fin n → ℝ)41 mapsTo_f : MapsTo f source target42 mapsTo_g : MapsTo g target source43 left_inv : Set.LeftInvOn g f source44 right_inv : Set.RightInvOn g f target45 fConstant : ℝ≥046 lipschitzWith_f : LipschitzWith fConstant f47 gConstant : ℝ≥048 lipschitzWith_g : LipschitzWith gConstant g49 lower : ℝ50 lower_pos : 0 < lower51 anti : ∀ x y, lower * ‖x - y‖ ≤ ‖f x - f y‖5253namespace BiLipschitzOpenData5455/-- The forward map admits a Mathlib Lipschitz constant. -/56theorem lipschitz_f {n : ℕ} (D : BiLipschitzOpenData n) :57 ∃ K : ℝ≥0, LipschitzWith K D.f :=58 ⟨D.fConstant, D.lipschitzWith_f⟩5960/-- The inverse map admits a Mathlib Lipschitz constant. -/61theorem lipschitz_g {n : ℕ} (D : BiLipschitzOpenData n) :62 ∃ K : ℝ≥0, LipschitzWith K D.g :=63 ⟨D.gConstant, D.lipschitzWith_g⟩6465/-- The global lower bound makes the ambient map injective. -/66theorem f_injective {n : ℕ} (D : BiLipschitzOpenData n) :67 Function.Injective D.f := by68 intro x y hxy69 have hle : D.lower * ‖x - y‖ ≤ 0 := by70 simpa [hxy] using D.anti x y71 have hnonneg : 0 ≤ D.lower * ‖x - y‖ :=72 mul_nonneg D.lower_pos.le (norm_nonneg _)73 have hzero : D.lower * ‖x - y‖ = 0 := le_antisymm hle hnonneg74 have hnorm : ‖x - y‖ = 0 :=75 (mul_eq_zero.mp hzero).resolve_left (ne_of_gt D.lower_pos)76 exact sub_eq_zero.mp (norm_eq_zero.mp hnorm)7778end BiLipschitzOpenData7980/-- In equal finite dimension, a Lipschitz image of a Haar-null set is81Haar-null. The self-map type is intentional; this theorem does not claim an82unequal-dimensional result. -/83theorem volume_image_eq_zero_of_lipschitzWith {n : ℕ}84 {f : (Fin n → ℝ) → (Fin n → ℝ)} {C : ℝ≥0}85 (hf : LipschitzWith C f) {s : Set (Fin n → ℝ)} (hs : volume s = 0) :86 volume (f '' s) = 0 := by87 have hmeasure :88 (μH[(n : ℝ)] : Measure (Fin n → ℝ)) = volume := by89 simpa [Fintype.card_fin] using90 (MeasureTheory.hausdorffMeasure_pi_real (ι := Fin n))91 rw [← hmeasure] at hs ⊢92 apply le_antisymm ?_ bot_le93 calc94 μH[(n : ℝ)] (f '' s)95 ≤ ((C : ℝ≥0∞) ^ (n : ℝ)) * μH[(n : ℝ)] s :=96 hf.hausdorffMeasure_image_le (by positivity) s97 _ = 0 := by rw [hs, mul_zero]9899/-- Difference quotients retain a positive global lower bound in the100Fréchet-derivative limit. -/101private theorem fderiv_lower_bound_of_global_lower {n : ℕ}102 {f : (Fin n → ℝ) → (Fin n → ℝ)} {x : Fin n → ℝ}103 {A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)} {c : ℝ}104 (_hc : 0 < c)105 (hanti : ∀ u v, c * ‖u - v‖ ≤ ‖f u - f v‖)106 (hfd : HasFDerivAt f A x) (v : Fin n → ℝ) :107 c * ‖v‖ ≤ ‖A v‖ := by108 have hquot : ∀ t : ℝ, t ≠ 0 →109 c * ‖v‖ ≤ ‖t⁻¹ • (f (x + t • v) - f x)‖ := by110 intro t ht111 have h := hanti (x + t • v) x112 simpa [norm_smul, Real.norm_eq_abs, abs_inv, abs_mul, ht,113 mul_assoc, mul_left_comm, mul_comm] using114 (mul_le_mul_of_nonneg_left h (inv_nonneg.mpr (abs_nonneg t)))115 have htend :116 Tendsto (fun t : ℝ => t⁻¹ • (f (x + t • v) - f x))117 (𝓝[≠] 0) (𝓝 (A v)) := by118 simpa using (hfd.hasLineDerivAt v).tendsto_slope_zero119 have hevent : ∀ᶠ t : ℝ in 𝓝[≠] 0,120 c * ‖v‖ ≤ ‖t⁻¹ • (f (x + t • v) - f x)‖ := by121 filter_upwards [self_mem_nhdsWithin] with t ht122 exact hquot t (by simpa using ht)123 exact ge_of_tendsto ((continuous_norm.tendsto (A v)).comp htend) hevent124125private theorem injective_of_positive_lower_bound {n : ℕ}126 (A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) {c : ℝ} (hc : 0 < c)127 (hA : ∀ v, c * ‖v‖ ≤ ‖A v‖) : Function.Injective A := by128 intro u v huv129 have hzero : A (u - v) = 0 := by rw [map_sub, huv, sub_self]130 have h := hA (u - v)131 rw [hzero, norm_zero] at h132 have : ‖u - v‖ = 0 := by nlinarith [norm_nonneg (u - v)]133 exact sub_eq_zero.mp (norm_eq_zero.mp this)134135/-- Every existing derivative of the forward map has the recorded lower136bound. -/137theorem fderiv_lower_bound {n : ℕ} (D : BiLipschitzOpenData n)138 {x : Fin n → ℝ} (hdf : DifferentiableAt ℝ D.f x) (v : Fin n → ℝ) :139 D.lower * ‖v‖ ≤ ‖(fderiv ℝ D.f x) v‖ := by140 exact fderiv_lower_bound_of_global_lower D.lower_pos D.anti141 hdf.hasFDerivAt v142143/-- Every existing derivative of the forward map is injective. -/144theorem fderiv_injective {n : ℕ} (D : BiLipschitzOpenData n)145 {x : Fin n → ℝ} (hdf : DifferentiableAt ℝ D.f x) :146 Function.Injective (fderiv ℝ D.f x) := by147 exact injective_of_positive_lower_bound (fderiv ℝ D.f x) D.lower_pos148 (fderiv_lower_bound D hdf)149150/-- The derivative determinant is nonzero at differentiability points. -/151theorem det_fderiv_ne_zero {n : ℕ} (D : BiLipschitzOpenData n)152 {x : Fin n → ℝ} (hdf : DifferentiableAt ℝ D.f x) :153 (fderiv ℝ D.f x).det ≠ 0 := by154 change LinearMap.det (fderiv ℝ D.f x).toLinearMap ≠ 0155 intro hdet156 have hker := LinearMap.det_eq_zero_iff_ker_ne_bot.mp hdet157 exact hker (LinearMap.ker_eq_bot.mpr (fderiv_injective D hdf))158159/-- Totalized sign of the forward Jacobian. At exceptional points the value160`+1` is harmless. -/161def domainJacobianSign {n : ℕ} (D : BiLipschitzOpenData n)162 (x : Fin n → ℝ) : ℝ :=163 if 0 ≤ (fderiv ℝ D.f x).det then 1 else -1164165/-- Jacobian sign transported to the target through the specified inverse. -/166def targetJacobianSign {n : ℕ} (D : BiLipschitzOpenData n)167 (y : Fin n → ℝ) : ℝ :=168 domainJacobianSign D (D.g y)169170@[simp] theorem abs_domainJacobianSign {n : ℕ}171 (D : BiLipschitzOpenData n) (x : Fin n → ℝ) :172 |domainJacobianSign D x| = 1 := by173 unfold domainJacobianSign174 split <;> norm_num175176@[simp] theorem abs_targetJacobianSign {n : ℕ}177 (D : BiLipschitzOpenData n) (y : Fin n → ℝ) :178 |targetJacobianSign D y| = 1 := by179 simp [targetJacobianSign]180181/-- The totalized sign restores the signed determinant at each182 differentiability point. -/183theorem det_eq_domainSign_mul_abs {n : ℕ}184 (D : BiLipschitzOpenData n) {x : Fin n → ℝ}185 (hdf : DifferentiableAt ℝ D.f x) :186 (fderiv ℝ D.f x).det =187 domainJacobianSign D x * |(fderiv ℝ D.f x).det| := by188 have hnz := det_fderiv_ne_zero D hdf189 unfold domainJacobianSign190 split_ifs with hnonneg191 · have hpos : 0 < (fderiv ℝ D.f x).det :=192 lt_of_le_of_ne hnonneg (Ne.symm hnz)193 rw [abs_of_pos hpos]194 simp195 · have hneg : (fderiv ℝ D.f x).det < 0 := lt_of_not_ge hnonneg196 rw [abs_of_neg hneg]197 simp198199/-- The target image of the Rademacher exceptional set is null. -/200theorem target_exceptional_null {n : ℕ} (D : BiLipschitzOpenData n) :201 volume (D.f '' {x | ¬ DifferentiableAt ℝ D.f x}) = 0 := by202 apply volume_image_eq_zero_of_lipschitzWith D.lipschitzWith_f203 exact ae_iff.mp D.lipschitzWith_f.ae_differentiableAt204205/-- Signed transfer is derived from Mathlib's injective absolute Jacobian area206formula. No signed change-of-variables primitive and no degree theory is used. -/207theorem signed_area_transfer {n : ℕ} (D : BiLipschitzOpenData n)208 {φ : (Fin n → ℝ) → ℝ} (_hφ : IntegrableOn φ D.target) :209 ∫ x in D.source, φ (D.f x) * (fderiv ℝ D.f x).det ∂volume =210 ∫ y in D.target, φ y * targetJacobianSign D y ∂volume := by211 let G : Set (Fin n → ℝ) :=212 D.source ∩ {x | DifferentiableAt ℝ D.f x}213 have hdiff : ∀ᵐ x ∂volume, DifferentiableAt ℝ D.f x :=214 D.lipschitzWith_f.ae_differentiableAt215 have hGmeas : MeasurableSet G := by216 exact D.isOpen_source.measurableSet.inter217 (measurableSet_of_differentiableAt ℝ D.f)218 have hder : ∀ x ∈ G,219 HasFDerivWithinAt D.f (fderiv ℝ D.f x) G x := by220 intro x hx221 exact hx.2.hasFDerivAt.hasFDerivWithinAt222 have hinj : Set.InjOn D.f G := by223 intro x hx y hy hxy224 exact D.left_inv.injOn hx.1 hy.1 hxy225 have hsign_point : ∀ x ∈ G,226 (fderiv ℝ D.f x).det =227 domainJacobianSign D x * |(fderiv ℝ D.f x).det| := by228 intro x hx229 exact det_eq_domainSign_mul_abs D hx.2230 have hsource_sets : D.source =ᵐ[volume] G := by231 filter_upwards [hdiff] with x hx232 apply propext233 constructor234 · intro hxS235 exact ⟨hxS, hx⟩236 · intro hxG237 exact hxG.1238 have htarget_sets : D.target =ᵐ[volume] D.f '' G := by239 have hbad : ∀ᵐ y ∂volume,240 y ∉ D.f '' {x | ¬ DifferentiableAt ℝ D.f x} := by241 apply ae_iff.mpr242 rw [show {y | ¬ y ∉ D.f '' {x | ¬ DifferentiableAt ℝ D.f x}} =243 D.f '' {x | ¬ DifferentiableAt ℝ D.f x} by ext z; simp]244 exact target_exceptional_null D245 filter_upwards [hbad] with y hybad246 apply propext247 constructor248 · intro hyT249 have hxS : D.g y ∈ D.source := D.mapsTo_g hyT250 have hfx : D.f (D.g y) = y := D.right_inv hyT251 have hxdiff : DifferentiableAt ℝ D.f (D.g y) := by252 by_contra hnot253 exact hybad ⟨D.g y, hnot, hfx⟩254 exact ⟨D.g y, ⟨hxS, hxdiff⟩, hfx⟩255 · rintro ⟨x, hx, rfl⟩256 exact D.mapsTo_f hx.1257 have hdomain_integrand :258 (∫ x in G, φ (D.f x) * (fderiv ℝ D.f x).det ∂volume) =259 ∫ x in G, |(fderiv ℝ D.f x).det| •260 (φ (D.f x) * targetJacobianSign D (D.f x)) ∂volume := by261 apply integral_congr_ae262 filter_upwards [ae_restrict_mem hGmeas] with x hx263 rw [hsign_point x hx]264 simp [targetJacobianSign, D.left_inv hx.1,265 mul_assoc, mul_left_comm, mul_comm]266 have harea :=267 MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul268 volume hGmeas hder hinj269 (fun y => φ y * targetJacobianSign D y)270 calc271 (∫ x in D.source, φ (D.f x) * (fderiv ℝ D.f x).det ∂volume) =272 ∫ x in G, φ (D.f x) * (fderiv ℝ D.f x).det ∂volume :=273 setIntegral_congr_set hsource_sets274 _ = ∫ x in G, |(fderiv ℝ D.f x).det| •275 (φ (D.f x) * targetJacobianSign D (D.f x)) ∂volume :=276 hdomain_integrand277 _ = ∫ y in D.f '' G, φ y * targetJacobianSign D y ∂volume :=278 harea.symm279 _ = ∫ y in D.target, φ y * targetJacobianSign D y ∂volume :=280 (setIntegral_congr_set htarget_sets).symm281282end BilipschitzOrientation283end MathlibAnnex