Exact source: MathlibAnnex/Analysis/Calculus/BilipschitzOrientation/Constancy.lean
Pinned GitHub source · Raw UTF-8 source
Back to The signed Jacobian integral is a sign times target volume · Back to A common orientation sign for the radial derivative average
1import MathlibAnnex.Analysis.Calculus.BilipschitzOrientation.Piola2import MathlibAnnex.Analysis.Distribution.WeakGradient3import Mathlib.Tactic45/-!6# Degree-free orientation for global bi-Lipschitz data: constancy and volume78Target preconnectedness, positive measure, and finite measure are separated at9the exact steps where they are used:1011* preconnectedness glues local a.e. constants;12* positive measure forces the constant sign to be `+1` or `-1`;13* finite measure evaluates the integral of the constant.1415No assertion of one global sign is made on an arbitrary disconnected target.16This browser-produced source is `HANDWRITTEN_UNBUILT` until local elaboration.17-/1819noncomputable section2021open Set MeasureTheory Filter22open scoped BigOperators ENNReal2324namespace MathlibAnnex25namespace BilipschitzOrientation2627/-- The transported sign is locally integrable because it is measurable and28bounded in norm by one. -/29theorem locallyIntegrableOn_targetJacobianSign {n : ℕ}30 (D : BiLipschitzOpenData n) :31 LocallyIntegrableOn (targetJacobianSign D) D.target := by32 have hfderiv_meas : Measurable33 (fun x : Fin n → ℝ => fderiv ℝ D.f x) := measurable_fderiv ℝ D.f34 have hdet_meas : Measurable35 (fun x : Fin n → ℝ => (fderiv ℝ D.f x).det) :=36 ContinuousLinearMap.continuous_det.measurable.comp hfderiv_meas37 have hdomain_meas : Measurable (domainJacobianSign D) := by38 unfold domainJacobianSign39 exact Measurable.ite40 (measurableSet_Ici.preimage hdet_meas)41 measurable_const measurable_const42 have htarget_meas : Measurable (targetJacobianSign D) := by43 exact hdomain_meas.comp D.lipschitzWith_g.continuous.measurable44 refine (locallyIntegrableOn_const (μ := volume)45 (s := D.target) (1 : ℝ)).mono46 htarget_meas.aestronglyMeasurable ?_47 filter_upwards with y48 simp4950/-- On a preconnected open target, the transported Jacobian sign is a.e.51constant. This is the exact R05 weak-divergence-zero interface. -/52theorem targetJacobianSign_ae_const {n : ℕ}53 (D : BiLipschitzOpenData n) (hpre : IsPreconnected D.target) :54 ∃ c : ℝ, AEConstantOn volume (targetJacobianSign D) D.target c := by55 exact (weakDivergenceZero_targetJacobianSign D).exists_aeConstantOn56 D.isOpen_target hpre (locallyIntegrableOn_targetJacobianSign D)5758/-- Positive target measure excludes a vacuous a.e. constant and forces its59value to be exactly `+1` or `-1`. -/60theorem targetJacobianSign_const_is_pm_one {n : ℕ}61 (D : BiLipschitzOpenData n) {c : ℝ}62 (hc : AEConstantOn volume (targetJacobianSign D) D.target c)63 (hpos : 0 < volume D.target) : c = 1 ∨ c = -1 := by64 change ∀ᵐ y ∂volume.restrict D.target, targetJacobianSign D y = c at hc65 obtain ⟨y, hyT, hyc⟩ :=66 MeasureTheory.Measure.exists_mem_of_measure_ne_zero_of_ae67 (μ := volume) (s := D.target) (ne_of_gt hpos) hc68 have habs : |c| = 1 := by69 simpa [hyc] using abs_targetJacobianSign D y70 exact eq_or_eq_neg_of_abs_eq habs7172/-- The total signed Jacobian integral is one real orientation sign times the73finite target volume. The sign is returned as a real number with an explicit74`±1` certificate, rather than duplicating the SR-specific Plücker sign type. -/75theorem integral_det_fderiv_eq_signed_volume {n : ℕ}76 (D : BiLipschitzOpenData n) (hpre : IsPreconnected D.target)77 (hpos : 0 < volume D.target) (hfinite : volume D.target ≠ ∞) :78 ∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧79 ∫ x in D.source, (fderiv ℝ D.f x).det ∂volume =80 ε * (volume D.target).toReal := by81 obtain ⟨c, hc⟩ := targetJacobianSign_ae_const D hpre82 have hpm : c = 1 ∨ c = -1 :=83 targetJacobianSign_const_is_pm_one D hc hpos84 refine ⟨c, hpm, ?_⟩85 have htransfer := signed_area_transfer D86 (φ := fun _ => (1 : ℝ)) (by87 simpa using integrableOn_const (μ := volume) (C := (1 : ℝ)) hfinite)88 change ∀ᵐ y ∂volume.restrict D.target, targetJacobianSign D y = c at hc89 calc90 ∫ x in D.source, (fderiv ℝ D.f x).det ∂volume =91 ∫ y in D.target, targetJacobianSign D y ∂volume := by92 simpa using htransfer93 _ = ∫ y in D.target, c ∂volume := integral_congr_ae hc94 _ = c * (volume D.target).toReal := by95 rw [MeasureTheory.setIntegral_const]96 change (volume D.target).toReal * c = c * (volume D.target).toReal97 exact mul_comm _ _9899end BilipschitzOrientation100end MathlibAnnex