Exact source: MathlibAnnex/Analysis/Calculus/BilipschitzOrientation/Piola.lean
Pinned GitHub source · Raw UTF-8 source
Back to The transported Jacobian sign has zero weak gradient · Back to Weak Piola identity for a compactly supported test field
1import MathlibAnnex.Analysis.Calculus.BilipschitzOrientation.Basic2import MathlibAnnex.MeasureTheory.Integral.MaximalMinor3import MathlibAnnex.Analysis.Distribution.WeakGradient.Basic4import Mathlib.Tactic56/-!7# Degree-free orientation for global bi-Lipschitz data: weak Piola layer89The public output of this file is the weak Piola identity and the resulting10`WeakDivergenceZero` statement for the target Jacobian sign. Coordinate11rank-one perturbations are implementation details and stay private. The12whole-space determinant-difference identity is supplied by the exact R0413maximal-minor null-Lagrangian theorem; compact C¹ test fields and divergence14come from the exact repaired R05 API.1516This browser-produced source is `HANDWRITTEN_UNBUILT` until local elaboration.17-/1819noncomputable section2021open Set MeasureTheory Filter22open scoped BigOperators ENNReal NNReal Topology2324namespace MathlibAnnex25namespace BilipschitzOrientation2627private def basisVector {n : ℕ} (i : Fin n) : Fin n → ℝ := Pi.single i 12829private noncomputable def coordinateProjector {n : ℕ} (i : Fin n) :30 (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) :=31 (ContinuousLinearMap.proj i).smulRight (basisVector i)3233@[simp] private theorem coordinateProjector_apply {n : ℕ} (i : Fin n)34 (x : Fin n → ℝ) :35 coordinateProjector i x = x i • basisVector i := by36 rfl3738private def clmMatrix {n : ℕ}39 (A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) : Matrix (Fin n) (Fin n) ℝ :=40 fun i j => A (Pi.single j 1) i4142private theorem clmMatrix_eq_toMatrix' {n : ℕ}43 (A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) :44 clmMatrix A = LinearMap.toMatrix' A.toLinearMap := by45 ext i j46 rfl4748private noncomputable def coordDet {n : ℕ}49 (A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) : ℝ :=50 Matrix.det (clmMatrix A)5152@[simp] private theorem coordDet_eq_det {n : ℕ}53 (A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) :54 coordDet A = A.det := by55 rw [coordDet, clmMatrix_eq_toMatrix']56 exact LinearMap.det_toMatrix' A.toLinearMap5758private theorem coordDet_comp {n : ℕ}59 (A B : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) :60 coordDet (A.comp B) = coordDet A * coordDet B := by61 simp only [coordDet_eq_det]62 change LinearMap.det (A.toLinearMap.comp B.toLinearMap) =63 LinearMap.det A.toLinearMap * LinearMap.det B.toLinearMap64 exact LinearMap.det_comp A.toLinearMap B.toLinearMap6566private def coordinatePerturbation {n : ℕ} (D : BiLipschitzOpenData n)67 (W : CompactC1VectorField (Fin n → ℝ)) (i : Fin n)68 (x : Fin n → ℝ) : Fin n → ℝ :=69 coordinateProjector i (W (D.f x))7071private def coordinatePiolaTerm {n : ℕ} (D : BiLipschitzOpenData n)72 (W : CompactC1VectorField (Fin n → ℝ)) (i : Fin n)73 (x : Fin n → ℝ) : ℝ :=74 (fderiv ℝ W (D.f x) (basisVector i)) i * coordDet (fderiv ℝ D.f x)7576private theorem divergence_mul_coordDet {n : ℕ}77 (D : BiLipschitzOpenData n)78 (W : CompactC1VectorField (Fin n → ℝ)) (x : Fin n → ℝ) :79 divergence W (D.f x) * coordDet (fderiv ℝ D.f x) =80 ∑ i : Fin n, coordinatePiolaTerm D W i x := by81 rw [divergence_pi]82 simp [coordinatePiolaTerm, basisVector, Finset.sum_mul]8384private def oneRowPerturbationMatrix {n : ℕ} (i : Fin n)85 (B : Matrix (Fin n) (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ :=86 (1 : Matrix (Fin n) (Fin n) ℝ).updateRow i87 ((1 : Matrix (Fin n) (Fin n) ℝ) i + B i)8889private theorem row_eq_sum_stdBasis {n : ℕ}90 (B : Matrix (Fin n) (Fin n) ℝ) (i : Fin n) :91 B i = ∑ j : Fin n, B i j • (1 : Matrix (Fin n) (Fin n) ℝ) j := by92 funext j93 simp [Matrix.one_apply]9495private theorem det_oneRowPerturbationMatrix {n : ℕ} (i : Fin n)96 (B : Matrix (Fin n) (Fin n) ℝ) :97 Matrix.det (oneRowPerturbationMatrix i B) = 1 + B i i := by98 rw [oneRowPerturbationMatrix, Matrix.det_updateRow_add]99 rw [Matrix.updateRow_eq_self, Matrix.det_one]100 rw [row_eq_sum_stdBasis B i, Matrix.det_updateRow_sum]101 simp [Matrix.det_one, Matrix.one_apply]102103private theorem clmMatrix_one_add_coordinateProjector_comp {n : ℕ}104 (i : Fin n) (B : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) :105 clmMatrix ((ContinuousLinearMap.id ℝ (Fin n → ℝ)) +106 (coordinateProjector i).comp B) =107 oneRowPerturbationMatrix i (clmMatrix B) := by108 classical109 ext r c110 by_cases hri : r = i111 · subst r112 simp [oneRowPerturbationMatrix, coordinateProjector, basisVector,113 clmMatrix, Matrix.updateRow, Matrix.one_apply, Pi.single_apply]114 · simp [oneRowPerturbationMatrix, coordinateProjector, basisVector,115 clmMatrix, Matrix.updateRow, Matrix.one_apply, Pi.single_apply, hri]116117private theorem coordDet_one_add_coordinateProjector_comp {n : ℕ}118 (i : Fin n) (B : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) :119 coordDet ((ContinuousLinearMap.id ℝ (Fin n → ℝ)) +120 (coordinateProjector i).comp B) =121 1 + (B (basisVector i)) i := by122 rw [coordDet, clmMatrix_one_add_coordinateProjector_comp,123 det_oneRowPerturbationMatrix]124 simp [clmMatrix, basisVector]125126private theorem compactField_exists_fderiv_bound {n : ℕ}127 (W : CompactC1VectorField (Fin n → ℝ)) :128 ∃ C : ℝ≥0, ∀ y, ‖fderiv ℝ W y‖₊ ≤ C := by129 have hcont : Continuous (fun y => ‖fderiv ℝ W y‖₊) :=130 (W.contDiff.continuous_fderiv (by norm_num)).nnnorm131 obtain ⟨C, hC⟩ := W.isCompact_carrier.bddAbove_image hcont.continuousOn132 refine ⟨C, fun y => ?_⟩133 by_cases hy : y ∈ W.carrier134 · exact hC ⟨y, hy, rfl⟩135 · rw [W.fderiv_eq_zero_of_not_mem_carrier hy]136 simp137138private theorem exists_lipschitzWith_compactField {n : ℕ}139 (W : CompactC1VectorField (Fin n → ℝ)) : ∃ K : ℝ≥0, LipschitzWith K W := by140 obtain ⟨C, hC⟩ := compactField_exists_fderiv_bound W141 exact ⟨C, lipschitzWith_of_nnnorm_fderiv_le142 (W.contDiff.differentiable (by norm_num)) hC⟩143144private theorem preimage_eq_g_image {n : ℕ} (D : BiLipschitzOpenData n)145 {K : Set (Fin n → ℝ)} (hK : K ⊆ D.target) :146 D.f ⁻¹' K = D.g '' K := by147 ext x148 constructor149 · intro hx150 let y := D.f x151 have hyT : y ∈ D.target := hK hx152 have hright : D.f (D.g y) = y := D.right_inv hyT153 have hxg : x = D.g y := D.f_injective (by simpa [y] using hright.symm)154 exact ⟨y, hx, hxg.symm⟩155 · rintro ⟨y, hyK, rfl⟩156 simpa [D.right_inv (hK hyK)] using hyK157158private theorem isCompact_preimage_carrier {n : ℕ}159 (D : BiLipschitzOpenData n)160 (W : CompactC1VectorField (Fin n → ℝ))161 (hW : W.carrier ⊆ D.target) :162 IsCompact (D.f ⁻¹' W.carrier) := by163 rw [preimage_eq_g_image D hW]164 exact W.isCompact_carrier.image D.lipschitzWith_g.continuous165166private theorem exists_lipschitzWith_coordinatePerturbation {n : ℕ}167 (D : BiLipschitzOpenData n)168 (W : CompactC1VectorField (Fin n → ℝ)) (i : Fin n) :169 ∃ K : ℝ≥0, LipschitzWith K (coordinatePerturbation D W i) := by170 obtain ⟨KW, hKW⟩ := exists_lipschitzWith_compactField W171 exact ⟨‖coordinateProjector i‖₊ * (KW * D.fConstant), by172 change LipschitzWith (‖coordinateProjector i‖₊ * (KW * D.fConstant))173 (fun x => coordinateProjector i (W (D.f x)))174 exact (coordinateProjector i).lipschitz.comp175 (hKW.comp D.lipschitzWith_f)⟩176177private theorem coordinatePerturbation_support_subset_preimage {n : ℕ}178 (D : BiLipschitzOpenData n)179 (W : CompactC1VectorField (Fin n → ℝ)) (i : Fin n) :180 Function.support (coordinatePerturbation D W i) ⊆ D.f ⁻¹' W.carrier := by181 intro x hx182 by_contra hnot183 have hzero : W (D.f x) = 0 := by184 by_contra hnz185 exact hnot (W.support_subset hnz)186 exact hx (by simp [coordinatePerturbation, hzero])187188private theorem hasCompactSupport_coordinatePerturbation {n : ℕ}189 (D : BiLipschitzOpenData n)190 (W : CompactC1VectorField (Fin n → ℝ))191 (hW : W.carrier ⊆ D.target) (i : Fin n) :192 HasCompactSupport (coordinatePerturbation D W i) := by193 exact (isCompact_preimage_carrier D W hW).of_isClosed_subset194 (isClosed_tsupport _)195 (closure_minimal (coordinatePerturbation_support_subset_preimage D W i)196 (isCompact_preimage_carrier D W hW).isClosed)197198private theorem coordinatePiolaTerm_eq_zero_of_image_not_mem_carrier {n : ℕ}199 (D : BiLipschitzOpenData n)200 (W : CompactC1VectorField (Fin n → ℝ)) (i : Fin n)201 {x : Fin n → ℝ} (hx : D.f x ∉ W.carrier) :202 coordinatePiolaTerm D W i x = 0 := by203 rw [coordinatePiolaTerm, W.fderiv_eq_zero_of_not_mem_carrier hx]204 simp205206private theorem coordinatePiolaTerm_eq_zero_of_not_mem_source {n : ℕ}207 (D : BiLipschitzOpenData n)208 (W : CompactC1VectorField (Fin n → ℝ))209 (hW : W.carrier ⊆ D.target) (i : Fin n)210 {x : Fin n → ℝ} (hx : x ∉ D.source) :211 coordinatePiolaTerm D W i x = 0 := by212 apply coordinatePiolaTerm_eq_zero_of_image_not_mem_carrier D W i213 intro hfx214 have hpre : x ∈ D.f ⁻¹' W.carrier := hfx215 rw [preimage_eq_g_image D hW] at hpre216 rcases hpre with ⟨y, hy, rfl⟩217 exact hx (D.mapsTo_g (hW hy))218219private theorem fderiv_coordinatePerturbation {n : ℕ}220 (D : BiLipschitzOpenData n)221 (W : CompactC1VectorField (Fin n → ℝ)) (i : Fin n)222 {x : Fin n → ℝ} (hdf : DifferentiableAt ℝ D.f x) :223 fderiv ℝ (coordinatePerturbation D W i) x =224 ((coordinateProjector i).comp (fderiv ℝ W (D.f x))).comp225 (fderiv ℝ D.f x) := by226 have hWdiff : DifferentiableAt ℝ W (D.f x) :=227 (W.contDiff.differentiable (by norm_num)) (D.f x)228 have hcomp :=229 ((coordinateProjector i).hasFDerivAt.comp x230 (hWdiff.hasFDerivAt.comp x hdf.hasFDerivAt)).fderiv231 change fderiv ℝ (⇑(coordinateProjector i) ∘ W ∘ D.f) x = _232 rw [hcomp]233 ext v234 rfl235236private theorem fderiv_add_coordinatePerturbation {n : ℕ}237 (D : BiLipschitzOpenData n)238 (W : CompactC1VectorField (Fin n → ℝ)) (i : Fin n)239 {x : Fin n → ℝ} (hdf : DifferentiableAt ℝ D.f x) :240 fderiv ℝ (fun y => D.f y + coordinatePerturbation D W i y) x =241 ((ContinuousLinearMap.id ℝ (Fin n → ℝ)) +242 (coordinateProjector i).comp (fderiv ℝ W (D.f x))).comp243 (fderiv ℝ D.f x) := by244 have hWdiff : DifferentiableAt ℝ W (D.f x) :=245 (W.contDiff.differentiable (by norm_num)) (D.f x)246 have hudiff : DifferentiableAt ℝ (coordinatePerturbation D W i) x :=247 (coordinateProjector i).differentiableAt.comp x (hWdiff.comp x hdf)248 calc249 fderiv ℝ (fun y => D.f y + coordinatePerturbation D W i y) x =250 fderiv ℝ D.f x + fderiv ℝ (coordinatePerturbation D W i) x := by251 change fderiv ℝ (D.f + coordinatePerturbation D W i) x = _252 exact (hdf.hasFDerivAt.add hudiff.hasFDerivAt).fderiv253 _ = ((ContinuousLinearMap.id ℝ (Fin n → ℝ)) +254 (coordinateProjector i).comp (fderiv ℝ W (D.f x))).comp255 (fderiv ℝ D.f x) := by256 rw [fderiv_coordinatePerturbation D W i hdf]257 ext v258 simp259260private theorem coordDet_difference_eq_coordinatePiolaTerm {n : ℕ}261 (D : BiLipschitzOpenData n)262 (W : CompactC1VectorField (Fin n → ℝ)) (i : Fin n)263 {x : Fin n → ℝ} (hdf : DifferentiableAt ℝ D.f x) :264 coordDet (fderiv ℝ (fun y => D.f y + coordinatePerturbation D W i y) x) -265 coordDet (fderiv ℝ D.f x) = coordinatePiolaTerm D W i x := by266 rw [fderiv_add_coordinatePerturbation D W i hdf]267 rw [coordDet_comp, coordDet_one_add_coordinateProjector_comp]268 simp [coordinatePiolaTerm, basisVector]269 ring270271private theorem coordDet_difference_eq_coordinatePiolaTerm_ae {n : ℕ}272 (D : BiLipschitzOpenData n)273 (W : CompactC1VectorField (Fin n → ℝ)) (i : Fin n) :274 ∀ᵐ x ∂volume,275 coordDet (fderiv ℝ (fun y => D.f y + coordinatePerturbation D W i y) x) -276 coordDet (fderiv ℝ D.f x) = coordinatePiolaTerm D W i x := by277 filter_upwards [D.lipschitzWith_f.ae_differentiableAt] with x hx278 exact coordDet_difference_eq_coordinatePiolaTerm D W i hx279280private noncomputable def identityMinorIndex (n : ℕ) :281 Matrix.MaximalMinorIndex n (Fin n) :=282 Matrix.MaximalMinorIndex.ofOrderEmbedding (OrderIso.refl (Fin n)).toOrderEmbedding283284private theorem selectedSquare_identity {n : ℕ}285 (A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) :286 ContinuousLinearMap.selectedSquare (identityMinorIndex n) A = A := by287 ext x i288 simp [ContinuousLinearMap.selectedSquare, identityMinorIndex]289290@[simp] private theorem maximalMinorIntegrand_identity {n : ℕ}291 (f : (Fin n → ℝ) → (Fin n → ℝ)) (x : Fin n → ℝ) :292 NullLagrangian.maximalMinorIntegrand (identityMinorIndex n) f x =293 coordDet (fderiv ℝ f x) := by294 unfold NullLagrangian.maximalMinorIntegrand295 rw [selectedSquare_identity]296 exact (coordDet_eq_det (fderiv ℝ f x)).symm297298private theorem integral_coordDet_add_sub_eq_zero_of_lipschitzWith299 {m : ℕ} {g u : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)}300 {Cg Cu : ℝ≥0} (hg : LipschitzWith Cg g) (hu : LipschitzWith Cu u)301 (huc : HasCompactSupport u) :302 ∫ x, (coordDet (fderiv ℝ (fun y => g y + u y) x) -303 coordDet (fderiv ℝ g x)) = 0 := by304 simpa only [maximalMinorIntegrand_identity] using305 (NullLagrangian.integral_maximalMinor_fderiv_add_sub_eq_zero_of_lipschitzWith306 (identityMinorIndex (m + 1)) hg hu huc)307308private theorem integrable_coordDet_difference_of_lipschitzWith309 {m : ℕ} {g u : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)}310 {Cg Cu : ℝ≥0} (hg : LipschitzWith Cg g) (hu : LipschitzWith Cu u)311 (huc : HasCompactSupport u) :312 Integrable (fun x =>313 coordDet (fderiv ℝ (fun y => g y + u y) x) -314 coordDet (fderiv ℝ g x)) := by315 let s := identityMinorIndex (m + 1)316 let K : Set (Fin (m + 1) → ℝ) := tsupport u317 let q := fun x =>318 NullLagrangian.maximalMinorIntegrand s (fun y => g y + u y) x -319 NullLagrangian.maximalMinorIntegrand s g x320 have hK : IsCompact K := huc321 have hplus : LipschitzWith (Cg + Cu) (fun x => g x + u x) := hg.add hu322 have hplusInt :=323 NullLagrangian.integrableOn_maximalMinor_fderiv_of_lipschitzWith s hplus hK324 have hgInt :=325 NullLagrangian.integrableOn_maximalMinor_fderiv_of_lipschitzWith s hg hK326 have hqOn : IntegrableOn q K := hplusInt.sub hgInt327 have hind : Integrable (K.indicator q) :=328 hqOn.integrable_indicator hK.measurableSet329 have heq : K.indicator q = q := by330 funext x331 by_cases hx : x ∈ K332 · simp [hx]333 · have hz :=334 NullLagrangian.topMinor_difference_eq_zero_of_not_mem_tsupport s (g := g) hx335 simp [hx, q, hz]336 rw [heq] at hind337 simpa only [q, s, maximalMinorIntegrand_identity] using hind338339private theorem integrable_coordinatePiolaTerm {m : ℕ}340 (D : BiLipschitzOpenData (m + 1))341 (W : CompactC1VectorField (Fin (m + 1) → ℝ))342 (hW : W.carrier ⊆ D.target) (i : Fin (m + 1)) :343 Integrable (coordinatePiolaTerm D W i) := by344 let u := coordinatePerturbation D W i345 obtain ⟨Cu, hu⟩ := exists_lipschitzWith_coordinatePerturbation D W i346 have huc : HasCompactSupport u := hasCompactSupport_coordinatePerturbation D W hW i347 have hdiff := integrable_coordDet_difference_of_lipschitzWith348 D.lipschitzWith_f hu huc349 exact hdiff.congr (coordDet_difference_eq_coordinatePiolaTerm_ae D W i)350351private theorem coordinate_weak_piola {m : ℕ}352 (D : BiLipschitzOpenData (m + 1))353 (W : CompactC1VectorField (Fin (m + 1) → ℝ))354 (hW : W.carrier ⊆ D.target) (i : Fin (m + 1)) :355 ∫ x in D.source, coordinatePiolaTerm D W i x ∂volume = 0 := by356 let u := coordinatePerturbation D W i357 obtain ⟨Cu, hu⟩ := exists_lipschitzWith_coordinatePerturbation D W i358 have huc : HasCompactSupport u := hasCompactSupport_coordinatePerturbation D W hW i359 have hNL := integral_coordDet_add_sub_eq_zero_of_lipschitzWith360 D.lipschitzWith_f hu huc361 have hglobal : ∫ x, coordinatePiolaTerm D W i x = 0 := by362 rw [← integral_congr_ae363 (coordDet_difference_eq_coordinatePiolaTerm_ae D W i)]364 exact hNL365 have houtside : ∀ᵐ x ∂volume.restrict D.sourceᶜ,366 coordinatePiolaTerm D W i x = 0 := by367 filter_upwards [ae_restrict_mem D.isOpen_source.measurableSet.compl] with x hx368 exact coordinatePiolaTerm_eq_zero_of_not_mem_source D W hW i hx369 have hint := integrable_coordinatePiolaTerm D W hW i370 have hsplit := integral_add_compl D.isOpen_source.measurableSet hint371 have hcompl : ∫ x in D.sourceᶜ, coordinatePiolaTerm D W i x = 0 :=372 MeasureTheory.integral_eq_zero_of_ae houtside373 linarith [hglobal, hsplit, hcompl]374375/-- Weak Piola identity for the forward map. Dimension zero is the empty-sum376case; positive dimension uses R04's exact maximal-minor null-Lagrangian API. -/377theorem weak_piola {n : ℕ} (D : BiLipschitzOpenData n)378 (W : CompactC1VectorField (Fin n → ℝ)) (hW : W.carrier ⊆ D.target) :379 ∫ x in D.source,380 divergence W (D.f x) * (fderiv ℝ D.f x).det ∂volume = 0 := by381 cases n with382 | zero =>383 simp [divergence_pi]384 | succ m =>385 have hint : ∀ i : Fin (m + 1),386 IntegrableOn (coordinatePiolaTerm D W i) D.source := by387 intro i388 exact (integrable_coordinatePiolaTerm D W hW i).integrableOn389 rw [show (fun x => divergence W (D.f x) * (fderiv ℝ D.f x).det) =390 (fun x => ∑ i : Fin (m + 1), coordinatePiolaTerm D W i x) by391 funext x392 rw [← coordDet_eq_det]393 exact divergence_mul_coordDet D W x]394 rw [MeasureTheory.integral_finsetSum _ (fun i _ => hint i)]395 exact Finset.sum_eq_zero fun i _ => coordinate_weak_piola D W hW i396397private theorem integrable_divergence {n : ℕ}398 (W : CompactC1VectorField (Fin n → ℝ)) : Integrable (divergence W) := by399 have hdiv_cont : Continuous (divergence W) := by400 have hfd_cont : Continuous (fun y => fderiv ℝ W y) :=401 W.contDiff.continuous_fderiv (by norm_num)402 have hrepr : (fun y => divergence W y) =403 (fun y => ∑ i : Fin n, (fderiv ℝ W y (Pi.single i 1)) i) := by404 funext y405 exact divergence_pi W y406 change Continuous (fun y => divergence W y)407 rw [hrepr]408 apply continuous_finsetSum409 intro i hi410 have heval : Continuous (fun A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) =>411 (A (Pi.single i 1)) i) := by fun_prop412 exact heval.comp hfd_cont413 have hcarrier : IntegrableOn (divergence W) W.carrier :=414 ContinuousOn.integrableOn_compact W.isCompact_carrier hdiv_cont.continuousOn415 have hind : Integrable (W.carrier.indicator (divergence W)) :=416 hcarrier.integrable_indicator W.isCompact_carrier.measurableSet417 have heq : W.carrier.indicator (divergence W) = divergence W := by418 funext y419 by_cases hy : y ∈ W.carrier420 · simp [hy]421 · have hfd := W.fderiv_eq_zero_of_not_mem_carrier hy422 have hdivzero : divergence W y = 0 := by423 rw [divergence_pi, hfd]424 simp425 simp [hy, hdivzero]426 rw [heq] at hind427 exact hind428429/-- Weak Piola plus signed transfer gives zero weak divergence for the target430Jacobian sign. -/431theorem weakDivergenceZero_targetJacobianSign {n : ℕ}432 (D : BiLipschitzOpenData n) :433 WeakDivergenceZero volume D.target (targetJacobianSign D) := by434 intro W hW435 have hp := weak_piola D W hW436 have ht := signed_area_transfer D437 (φ := divergence W) (integrable_divergence W).integrableOn438 calc439 (∫ y in D.target, targetJacobianSign D y * divergence W y ∂volume) =440 ∫ y in D.target, divergence W y * targetJacobianSign D y ∂volume := by441 apply integral_congr_ae442 exact Filter.Eventually.of_forall fun y => by443 simpa only using (mul_comm (targetJacobianSign D y) (divergence W y))444 _ = ∫ x in D.source,445 divergence W (D.f x) * (fderiv ℝ D.f x).det ∂volume := ht.symm446 _ = 0 := hp447448end BilipschitzOrientation449end MathlibAnnex