Exact source: MathlibAnnex/Analysis/Normed/Sphere/RadialJacobian.lean
Pinned GitHub source · Raw UTF-8 source
Back to The absolute Jacobian integral of a radial sphere extension
1import MathlibAnnex.Analysis.Normed.Sphere.RadialBall2import MathlibAnnex.MeasureTheory.Integral.MaximalMinor3import MathlibAnnex.Analysis.Calculus.BilipschitzOrientation4import MathlibAnnex.MeasureTheory.Measure.EquivalentSeminormBall5import Mathlib.MeasureTheory.Function.Jacobian6import Mathlib.Analysis.Convex.Measure7import Mathlib.Analysis.Convex.Gauge89/-! # Absolute radial Jacobian integral10The derivative is taken in the reference finite Pi norm, with source `MX` and11target `MY`. The integral of the absolute determinant equals the target closed12unit ball's original Lebesgue volume. The public integral theorem retains the13source positive dimension `m + 1`; no signed integral is asserted.14Private model witnesses are reconstructed locally from the accepted providers.15-/1617noncomputable section18open Set Metric Function MeasureTheory19open scoped NNReal ENNReal20namespace MathlibAnnex.Sphere21open EquivalentSeminorm2223private abbrev radialMap {n : ℕ}24 {MX MY : EquivalentSeminorm (Fin n → ℝ)}25 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)26 (x : Fin n → ℝ) : Fin n → ℝ :=27 show Fin n → ℝ from radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from x)2829@[simp] private theorem radialMap_p {n : ℕ}30 {MX MY : EquivalentSeminorm (Fin n → ℝ)}31 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x : Fin n → ℝ) :32 MY.p (radialMap Δ x) = MX.p x := radialExtension_norm Δ (show Space MX from x)3334private theorem radialMap_leftInverse {n : ℕ}35 {MX MY : EquivalentSeminorm (Fin n → ℝ)}36 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :37 LeftInverse (radialMap Δ.symm) (radialMap Δ) :=38 fun x => radialExtension_leftInverse Δ (show Space MX from x)3940private theorem radialMap_model_dist {n : ℕ}41 {MX MY : EquivalentSeminorm (Fin n → ℝ)}42 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x y : Fin n → ℝ) :43 MY.p (radialMap Δ x - radialMap Δ y) ≤ 3 * MX.p (x - y) := by44 have h := (lipschitzWith_radialExtension Δ).dist_le_mul45 (show Space MX from x) (show Space MX from y)46 simpa only [dist_space_eq, NNReal.coe_ofNat] using h4748private theorem lipschitzWith_radialMap {n : ℕ}49 {MX MY : EquivalentSeminorm (Fin n → ℝ)}50 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :51 LipschitzWith (3 * MX.upper / MY.lower).toNNReal (radialMap Δ) := by52 have hC : 0 ≤ 3 * MX.upper / MY.lower := div_nonneg (mul_nonneg (by norm_num) MX.upper_pos.le) MY.lower_pos.le53 refine LipschitzWith.of_dist_le_mul ?_54 intro x y55 have hlower := MY.lower_le (radialMap Δ x - radialMap Δ y)56 have hmodel := radialMap_model_dist Δ x y57 have hupper := MX.le_upper (x - y)58 rw [Real.coe_toNNReal _ hC, dist_eq_norm, dist_eq_norm]59 calc60 ‖radialMap Δ x - radialMap Δ y‖ ≤ (3 * MX.upper * ‖x - y‖) / MY.lower :=61 (le_div_iff₀ MY.lower_pos).2 (by nlinarith)62 _ = (3 * MX.upper / MY.lower) * ‖x - y‖ := by ring6364namespace Internal65private def referenceAntiConstant {n : ℕ} (MX MY : EquivalentSeminorm (Fin n → ℝ)) : ℝ :=66 MX.lower / (3 * MY.upper)6768private theorem referenceAntiConstant_pos {n : ℕ} (MX MY : EquivalentSeminorm (Fin n → ℝ)) :69 0 < referenceAntiConstant MX MY :=70 div_pos MX.lower_pos (mul_pos (by norm_num) MY.upper_pos)71end Internal72open Internal7374private theorem radialMap_lower {n : ℕ}75 {MX MY : EquivalentSeminorm (Fin n → ℝ)}76 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x y : Fin n → ℝ) :77 referenceAntiConstant MX MY * ‖x - y‖ ≤ ‖radialMap Δ x - radialMap Δ y‖ := by78 have hinv := radialMap_model_dist Δ.symm (radialMap Δ x) (radialMap Δ y)79 rw [radialMap_leftInverse Δ x, radialMap_leftInverse Δ y] at hinv80 have hlow := MX.lower_le (x - y)81 have hup := MY.le_upper (radialMap Δ x - radialMap Δ y)82 have hden : 0 < 3 * MY.upper := mul_pos (by norm_num) MY.upper_pos83 have hprod : MX.lower * ‖x - y‖ ≤ (3 * MY.upper) *84 ‖radialMap Δ x - radialMap Δ y‖ := by nlinarith85 dsimp [referenceAntiConstant]86 calc87 MX.lower / (3 * MY.upper) * ‖x - y‖ =88 (MX.lower * ‖x - y‖) / (3 * MY.upper) := by ring89 _ ≤ ‖radialMap Δ x - radialMap Δ y‖ :=90 (div_le_iff₀ hden).2 (by simpa only [mul_comm] using hprod)9192private theorem isOpen_openBall {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :93 IsOpen (M.p.ball 0 1) := by94 rw [Seminorm.ball_zero_eq]95 exact isOpen_lt M.continuous_p continuous_const9697private theorem convex_openBall {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :98 Convex ℝ (M.p.ball 0 1) := M.p.convex_ball 0 199100private theorem isConnected_openBall {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :101 IsConnected (M.p.ball 0 1) := by102 refine (convex_openBall M).isConnected ?_103 exact ⟨0, by simp⟩104105private theorem ae_differentiableAt_radialMap {n : ℕ}106 {MX MY : EquivalentSeminorm (Fin n → ℝ)}107 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :108 ∀ᵐ x ∂volume, DifferentiableAt ℝ (radialMap Δ) x :=109 (lipschitzWith_radialMap Δ).ae_differentiableAt110111namespace Internal112private def radialGoodSet {n : ℕ} {MX MY : EquivalentSeminorm (Fin n → ℝ)}113 (Δ : (sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)) : Set ((Fin n → ℝ)) :=114 (MX.p.ball 0 1) ∩ {x | DifferentiableAt ℝ (radialMap Δ) x}115end Internal116open Internal117private theorem radial_badSet_null {n : ℕ} {MX MY : EquivalentSeminorm (Fin n → ℝ)}118 (Δ : (sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)) :119 volume ((MX.p.ball 0 1) \ radialGoodSet Δ) = 0 := by120 -- [R15-API-CHECK:SJ-AREA-001]121 have hC := lipschitzWith_radialMap Δ122 have hdiff : ∀ᵐ x ∂volume.restrict ((MX.p.ball 0 1)),123 DifferentiableAt ℝ (radialMap Δ) x :=124 ae_restrict_of_ae hC.ae_differentiableAt125 have hfull : ∀ᵐ x ∂volume,126 x ∈ (MX.p.ball 0 1) →127 DifferentiableAt ℝ (radialMap Δ) x :=128 (ae_restrict_iff' (isOpen_openBall MX).measurableSet).mp hdiff129 have hset : (MX.p.ball 0 1) \ radialGoodSet Δ =130 {x | ¬(x ∈ (MX.p.ball 0 1) →131 DifferentiableAt ℝ (radialMap Δ) x)} := by132 ext x133 simp [radialGoodSet]134 rw [hset]135 exact ae_iff.mp hfull136137private theorem radial_image_badSet_null {n : ℕ}138 {MX MY : EquivalentSeminorm (Fin n → ℝ)}139 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :140 volume (radialMap Δ '' (MX.p.ball 0 1 \ radialGoodSet Δ)) = 0 :=141 BilipschitzOrientation.volume_image_eq_zero_of_lipschitzWith142 (lipschitzWith_radialMap Δ) (radial_badSet_null Δ)143144private theorem integrableOn_radial_abs_det {m : ℕ}145 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}146 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :147 IntegrableOn (fun x => |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)|)148 MX.closedUnitBall volume := by149 let s := Matrix.MaximalMinorIndex.ofOrderEmbedding150 (OrderIso.refl (Fin (m + 1))).toOrderEmbedding151 have h := NullLagrangian.integrableOn_maximalMinor_fderiv_of_lipschitzWith152 s (lipschitzWith_radialMap Δ) MX.isCompact_closedUnitBall153 have hsel (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ)) :154 ContinuousLinearMap.selectedSquare s A = A := by155 ext x i156 simp [ContinuousLinearMap.selectedSquare, s]157 have heq : NullLagrangian.maximalMinorIntegrand s (radialMap Δ) =158 (fun x => ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)) := by159 funext x160 unfold NullLagrangian.maximalMinorIntegrand161 rw [hsel]162 rw [heq] at h163 simpa only [IntegrableOn, Real.norm_eq_abs] using h.norm164165private theorem radial_lintegral_abs_det_eq_openBall_volume {m : ℕ}166 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)} (Δ : (sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)) :167 (∫⁻ x in (MX.p.ball 0 1),168 ENNReal.ofReal |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)| ∂volume) =169 volume ((MY.p.ball 0 1)) := by170 -- [R15-API-CHECK:SJ-AREA-003]171 let G := radialGoodSet Δ172 have hGmeas : MeasurableSet G := by173 exact (isOpen_openBall MX).measurableSet.inter174 (measurableSet_of_differentiableAt ℝ (radialMap Δ))175 have hder : ∀ x ∈ G,176 HasFDerivWithinAt (radialMap Δ)177 (fderiv ℝ (radialMap Δ) x) G x := by178 intro x hx179 exact hx.2.hasFDerivAt.hasFDerivWithinAt180 have hinj : Set.InjOn (radialMap Δ) G :=181 (radialMap_leftInverse Δ).injective.injOn182 have harea := MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image183 volume hGmeas hder hinj184 have hdomain :185 (∫⁻ x in (MX.p.ball 0 1),186 ENNReal.ofReal |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)| ∂volume) =187 ∫⁻ x in G,188 ENNReal.ofReal |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)| ∂volume := by189 apply setLIntegral_congr190 apply ae_eq_set.mpr191 constructor192 · simpa only [G] using radial_badSet_null Δ193 · have hempty : G \ (MX.p.ball 0 1) = ∅ := by194 ext x195 constructor196 · intro hx197 exact (hx.2 hx.1.1).elim198 · intro hx199 exact hx.elim200 rw [hempty, measure_empty]201 have himage : volume (radialMap Δ '' G) =202 volume ((MY.p.ball 0 1)) := by203 rw [← radialExtension_image_ball Δ]204 have hsplit : radialMap Δ '' (MX.p.ball 0 1) =205 radialMap Δ '' G ∪206 radialMap Δ '' ((MX.p.ball 0 1) \ radialGoodSet Δ) := by207 rw [← Set.image_union]208 congr 1209 ext x210 simp [G, radialGoodSet]211 rw [hsplit]212 exact measure_congr (union_ae_eq_left_of_ae_eq_empty213 (ae_eq_empty.mpr (radial_image_badSet_null Δ))).symm214 calc215 (∫⁻ x in (MX.p.ball 0 1),216 ENNReal.ofReal |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)| ∂volume) =217 ∫⁻ x in G,218 ENNReal.ofReal |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)| ∂volume := hdomain219 _ = volume (radialMap Δ '' G) := by220 simpa only [ContinuousLinearMap.det] using harea221 _ = volume ((MY.p.ball 0 1)) := himage222223private theorem modelOpenBall_volume_eq_ballVolume {m : ℕ}224 (M : EquivalentSeminorm (Fin (m + 1) → ℝ)) :225 (volume (M.p.ball 0 1)).toReal = M.closedUnitBallVolume := by226 have hsphere : {x | M.p x = 1} = frontier (M.p.ball 0 1) := by227 ext x228 change M.p x = 1 ↔ x ∈ frontier (M.p.ball 0 1)229 rw [← congrFun M.p.gauge_ball x]230 exact gauge_eq_one_iff_mem_frontier (M.p.convex_ball 0 1)231 (M.p.ball_mem_nhds M.continuous_p zero_lt_one)232 have hnull : volume {x | M.p x = 1} = 0 := by233 rw [hsphere]234 exact (M.p.convex_ball 0 1).addHaar_frontier volume235 unfold EquivalentSeminorm.closedUnitBallVolume236 apply congrArg ENNReal.toReal237 exact measure_congr (by238 filter_upwards [measure_eq_zero_iff_ae_notMem.mp hnull] with x hx239 have hne : M.p x ≠ 1 := hx240 apply propext241 change x ∈ M.p.ball 0 1 ↔ x ∈ M.closedUnitBall242 simp only [Seminorm.mem_ball_zero, EquivalentSeminorm.mem_closedUnitBall]243 exact ⟨le_of_lt, fun h => lt_of_le_of_ne h hne⟩)244245/-- Absolute Jacobian area identity in reference coordinates and the fixed246Lebesgue normalization, retaining the exact positive-dimensional source bound. -/247theorem radialExtension_integral_abs_det {m : ℕ}248 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}249 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :250 ∫ x in MX.p.ball 0 1,251 |ContinuousLinearMap.det (fderiv ℝ (fun y : Fin (m + 1) → ℝ =>252 (show Fin (m + 1) → ℝ from radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from y))) x)|253 ∂volume = MY.closedUnitBallVolume := by254 change (∫ x in MX.p.ball 0 1,255 |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)| ∂volume) = _256 have hlin := radial_lintegral_abs_det_eq_openBall_volume Δ257 have hint : IntegrableOn258 (fun x => |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)|)259 (MX.p.ball 0 1) volume :=260 (integrableOn_radial_abs_det Δ).mono_set261 (by intro x hx; exact MX.mem_closedUnitBall.mpr (le_of_lt (by simpa using hx)))262 have hnonneg_ae : 0 ≤ᵐ[volume.restrict (MX.p.ball 0 1)]263 fun x => |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)| :=264 ae_of_all _ fun x => abs_nonneg _265 rw [← ofReal_integral_eq_lintegral_ofReal hint hnonneg_ae] at hlin266 have hto := congrArg ENNReal.toReal hlin267 have hnonneg : 0 ≤ ∫ x in MX.p.ball 0 1,268 |ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x)| ∂volume :=269 integral_nonneg_of_ae hnonneg_ae270 rw [ENNReal.toReal_ofReal hnonneg] at hto271 exact hto.trans (modelOpenBall_volume_eq_ballVolume MY)272273namespace Internal274private def piolaOrientationModelRadialData {m : ℕ}275 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}276 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :277 BilipschitzOrientation.BiLipschitzOpenData (m + 1) where278 source := MX.p.ball 0 1279 target := MY.p.ball 0 1280 isOpen_source := isOpen_openBall MX281 isOpen_target := isOpen_openBall MY282 f := radialMap Δ283 g := radialMap Δ.symm284 mapsTo_f := by intro x hx; simpa using hx285 mapsTo_g := by intro x hx; simpa using hx286 left_inv := by intro x _; exact radialMap_leftInverse Δ x287 right_inv := by intro x _; exact radialMap_leftInverse Δ.symm x288 fConstant := (3 * MX.upper / MY.lower).toNNReal289 lipschitzWith_f := lipschitzWith_radialMap Δ290 gConstant := (3 * MY.upper / MX.lower).toNNReal291 lipschitzWith_g := lipschitzWith_radialMap Δ.symm292 lower := referenceAntiConstant MX MY293 lower_pos := referenceAntiConstant_pos MX MY294 anti := radialMap_lower Δ295296private theorem isConnected_piolaData {m : ℕ}297 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}298 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :299 IsConnected (piolaOrientationModelRadialData Δ).source ∧300 IsConnected (piolaOrientationModelRadialData Δ).target :=301 ⟨isConnected_openBall MX, isConnected_openBall MY⟩302end Internal303304private theorem volume_openBall_pos {m : ℕ} (M : EquivalentSeminorm (Fin (m + 1) → ℝ)) :305 0 < volume (M.p.ball 0 1) := by306 have hreal : 0 < (volume (M.p.ball 0 1)).toReal := by307 rw [modelOpenBall_volume_eq_ballVolume M]308 exact M.closedUnitBallVolume_pos309 exact (ENNReal.toReal_pos_iff.mp hreal).1310311private theorem volume_openBall_ne_top {m : ℕ} (M : EquivalentSeminorm (Fin (m + 1) → ℝ)) :312 volume (M.p.ball 0 1) ≠ ∞ := by313 exact ne_top_of_le_ne_top M.isCompact_closedUnitBall.measure_ne_top314 (measure_mono (by315 intro x hx316 exact M.mem_closedUnitBall.mpr (le_of_lt (by simpa using hx))))317318end MathlibAnnex.Sphere