Exact source: MathlibAnnex/Analysis/Normed/Plucker/RadialAverage.lean
Pinned GitHub source · Raw UTF-8 source
Back to A common orientation sign for the radial derivative average
1import MathlibAnnex.Analysis.Normed.Plucker.Average2import MathlibAnnex.Analysis.Normed.Sphere.RadialJacobian3import MathlibAnnex.LinearAlgebra.Matrix.MaximalMinor4import MathlibAnnex.Analysis.Calculus.BilipschitzOrientation56/-! # Linear transport of radial derivative averages78Derivatives use the reference finite Pi norm. The radial extension goes from9`Space MX` to `Space MY`, and the linear map is composed on its left.10Increasing selected rows and the original Lebesgue ball volumes are fixed.11The signed integral uses the accepted degree-free orientation theorem, with12an explicit real scalar equal to `1` or `-1`. The pointwise composition formula13includes dimension zero; the radial integral and average keep `m + 1`.14-/1516noncomputable section17open Set Metric Function MeasureTheory18open scoped NNReal ENNReal BigOperators19namespace MathlibAnnex.Plucker20open EquivalentSeminorm Sphere2122-- Reference-coordinate adapters are reconstructed from the exact B2 source.23-- SR-SOURCE-B31: the superseded radial-map alias is private definitional glue.24private abbrev radialMap {n : ℕ}25 {MX MY : EquivalentSeminorm (Fin n → ℝ)}26 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)27 (x : Fin n → ℝ) : Fin n → ℝ :=28 show Fin n → ℝ from radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from x)2930@[simp] private theorem radialMap_p {n : ℕ}31 {MX MY : EquivalentSeminorm (Fin n → ℝ)}32 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x : Fin n → ℝ) :33 MY.p (radialMap Δ x) = MX.p x := radialExtension_norm Δ (show Space MX from x)3435private theorem radialMap_leftInverse {n : ℕ}36 {MX MY : EquivalentSeminorm (Fin n → ℝ)}37 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :38 LeftInverse (radialMap Δ.symm) (radialMap Δ) :=39 fun x => radialExtension_leftInverse Δ (show Space MX from x)4041private theorem radialMap_model_dist {n : ℕ}42 {MX MY : EquivalentSeminorm (Fin n → ℝ)}43 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x y : Fin n → ℝ) :44 MY.p (radialMap Δ x - radialMap Δ y) ≤ 3 * MX.p (x - y) := by45 have h := (lipschitzWith_radialExtension Δ).dist_le_mul46 (show Space MX from x) (show Space MX from y)47 simpa only [dist_space_eq, NNReal.coe_ofNat] using h4849private theorem lipschitzWith_radialMap {n : ℕ}50 {MX MY : EquivalentSeminorm (Fin n → ℝ)}51 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :52 LipschitzWith (3 * MX.upper / MY.lower).toNNReal (radialMap Δ) := by53 have hC : 0 ≤ 3 * MX.upper / MY.lower := div_nonneg (mul_nonneg (by norm_num) MX.upper_pos.le) MY.lower_pos.le54 refine LipschitzWith.of_dist_le_mul ?_55 intro x y56 have hlower := MY.lower_le (radialMap Δ x - radialMap Δ y)57 have hmodel := radialMap_model_dist Δ x y58 have hupper := MX.le_upper (x - y)59 rw [Real.coe_toNNReal _ hC, dist_eq_norm, dist_eq_norm]60 calc61 ‖radialMap Δ x - radialMap Δ y‖ ≤ (3 * MX.upper * ‖x - y‖) / MY.lower :=62 (le_div_iff₀ MY.lower_pos).2 (by nlinarith)63 _ = (3 * MX.upper / MY.lower) * ‖x - y‖ := by ring6465namespace Internal66private def referenceAntiConstant {n : ℕ} (MX MY : EquivalentSeminorm (Fin n → ℝ)) : ℝ :=67 MX.lower / (3 * MY.upper)6869private theorem referenceAntiConstant_pos {n : ℕ} (MX MY : EquivalentSeminorm (Fin n → ℝ)) :70 0 < referenceAntiConstant MX MY :=71 div_pos MX.lower_pos (mul_pos (by norm_num) MY.upper_pos)72end Internal73open Internal7475private theorem radialMap_lower {n : ℕ}76 {MX MY : EquivalentSeminorm (Fin n → ℝ)}77 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x y : Fin n → ℝ) :78 referenceAntiConstant MX MY * ‖x - y‖ ≤ ‖radialMap Δ x - radialMap Δ y‖ := by79 have hinv := radialMap_model_dist Δ.symm (radialMap Δ x) (radialMap Δ y)80 rw [radialMap_leftInverse Δ x, radialMap_leftInverse Δ y] at hinv81 have hlow := MX.lower_le (x - y)82 have hup := MY.le_upper (radialMap Δ x - radialMap Δ y)83 have hden : 0 < 3 * MY.upper := mul_pos (by norm_num) MY.upper_pos84 have hprod : MX.lower * ‖x - y‖ ≤ (3 * MY.upper) *85 ‖radialMap Δ x - radialMap Δ y‖ := by nlinarith86 dsimp [referenceAntiConstant]87 calc88 MX.lower / (3 * MY.upper) * ‖x - y‖ =89 (MX.lower * ‖x - y‖) / (3 * MY.upper) := by ring90 _ ≤ ‖radialMap Δ x - radialMap Δ y‖ :=91 (div_le_iff₀ hden).2 (by simpa only [mul_comm] using hprod)9293private theorem isOpen_openBall {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :94 IsOpen (M.p.ball 0 1) := by95 rw [Seminorm.ball_zero_eq]96 exact isOpen_lt M.continuous_p continuous_const9798private theorem convex_openBall {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :99 Convex ℝ (M.p.ball 0 1) := M.p.convex_ball 0 1100101private theorem isConnected_openBall {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :102 IsConnected (M.p.ball 0 1) := by103 refine (convex_openBall M).isConnected ?_104 exact ⟨0, by simp⟩105106private theorem ae_differentiableAt_radialMap {n : ℕ}107 {MX MY : EquivalentSeminorm (Fin n → ℝ)}108 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :109 ∀ᵐ x ∂volume, DifferentiableAt ℝ (radialMap Δ) x :=110 (lipschitzWith_radialMap Δ).ae_differentiableAt111112113-- SR-SOURCE-B32: the source alias equality is definitional.114example {n : ℕ} {MX MY : EquivalentSeminorm (Fin n → ℝ)}115 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :116 radialMap Δ = (fun x : Fin n → ℝ => (show Fin n → ℝ from117 radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from x))) := rfl118119-- SR-SOURCE-B48: expand the original existential Lipschitz abbreviation.120private theorem exists_lipschitzWith_radialMap {n : ℕ} {MX MY : EquivalentSeminorm (Fin n → ℝ)}121 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :122 ∃ C : ℝ≥0, LipschitzWith C (radialMap Δ) := ⟨_, lipschitzWith_radialMap Δ⟩123124-- SR-SOURCE-B211: retain the exact nonempty-open-set volume argument.125private theorem volume_pos_of_isOpen_of_nonempty {n : ℕ} {V : Set (Fin n → ℝ)}126 (hVo : IsOpen V) (hVne : V.Nonempty) : 0 < volume V := by127 exact Measure.measure_pos_of_nonempty_interior volume128 (by simpa [hVo.interior_eq] using hVne)129130-- SR-SOURCE-B53 and B54 remain private recovery support; the signed proof131-- itself uses the global orientation theorem without choosing a point.132private theorem exists_mem_openBall_differentiableAt_radialMap_of_pos {n : ℕ} (_hn : 0 < n)133 {MX MY : EquivalentSeminorm (Fin n → ℝ)}134 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :135 ∃ x ∈ MX.p.ball 0 1, DifferentiableAt ℝ (radialMap Δ) x := by136 have hopen := isOpen_openBall MX137 have hne : (MX.p.ball 0 1).Nonempty := ⟨0, by simp⟩138 have hpos : volume (MX.p.ball 0 1) ≠ 0 := (volume_pos_of_isOpen_of_nonempty hopen hne).ne'139 have hdiff : ∀ᵐ x ∂volume.restrict (MX.p.ball 0 1),140 DifferentiableAt ℝ (radialMap Δ) x := ae_restrict_of_ae (ae_differentiableAt_radialMap Δ)141 have hmem : ∀ᵐ x ∂volume.restrict (MX.p.ball 0 1), x ∈ MX.p.ball 0 1 :=142 ae_restrict_mem hopen.measurableSet143 haveI : (ae (volume.restrict (MX.p.ball 0 1))).NeBot :=144 MeasureTheory.ae_restrict_neBot.mpr hpos145 rcases (hmem.and hdiff).exists with ⟨x, hxmem, hxdiff⟩146 exact ⟨x, hxmem, hxdiff⟩147148private theorem exists_mem_openBall_differentiableAt_radialMap_succ {m : ℕ}149 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}150 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :151 ∃ x ∈ MX.p.ball 0 1, DifferentiableAt ℝ (radialMap Δ) x :=152 exists_mem_openBall_differentiableAt_radialMap_of_pos (Nat.succ_pos m) Δ153154-- SR-SOURCE-B243: the old coordinate vector is exactly Pi.single.155private theorem referenceMatrix_apply {n N : ℕ}156 (A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) (i : Fin N) (j : Fin n) :157 LinearMap.toMatrix' A.toLinearMap i j = A (Pi.single j 1) i := rfl158159namespace Internal160-- SR-SOURCE-B26: all original witness fields, with the accepted scalar sign.161private structure SignedRadialData {m : ℕ}162 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))163 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) where164 radial : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)165 lipschitz : ∃ C : ℝ≥0, LipschitzWith C radial166 radial_coe_unitSphere : ∀ u : MX.unitSphere,167 radial u.val = (show Fin (m + 1) → ℝ from168 (Δ ⟨(show Space MX from u.val), mem_sphere_zero_iff_norm.mpr u.property⟩).val)169 average_linear_comp : ∀ {N : ℕ}170 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)), MY.IsContraction A →171 ∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧172 derivativeAverage MX (fun x => A (radial x)) =173 ε • Matrix.ballVolumeScaledMaximalMinors MY A174end Internal175176/-- Linear composition multiplies each derivative generator coordinate by the177signed square determinant of the inner derivative. Valid also for `n = 0`. -/178theorem derivativeGenerator_comp_linear_apply {n N : ℕ}179 (MX : EquivalentSeminorm (Fin n → ℝ))180 (A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ))181 (H : (Fin n → ℝ) → (Fin n → ℝ)) (x : Fin n → ℝ)182 (s : Matrix.MaximalMinorIndex n (Fin N)) (hH : DifferentiableAt ℝ H x) :183 derivativeGenerator MX (fun z => A (H z)) x s =184 MX.closedUnitBallVolume * Matrix.maximalMinor (LinearMap.toMatrix' A.toLinearMap) s *185 ContinuousLinearMap.det (fderiv ℝ H x) := by186 have hcomp : fderiv ℝ (fun z => A (H z)) x = A.comp (fderiv ℝ H x) :=187 (A.hasFDerivAt.comp x hH.hasFDerivAt).fderiv188 change MX.closedUnitBallVolume * Matrix.maximalMinor189 (LinearMap.toMatrix' (fderiv ℝ (fun z => A (H z)) x).toLinearMap) s = _190 rw [hcomp]191 change MX.closedUnitBallVolume * Matrix.maximalMinor192 (LinearMap.toMatrix' (A.toLinearMap.comp (fderiv ℝ H x).toLinearMap)) s = _193 rw [LinearMap.toMatrix'_comp, Matrix.maximalMinor_mul, LinearMap.det_toMatrix']194 simp only [ContinuousLinearMap.det, mul_assoc]195196namespace Internal197private theorem derivativePlucker_linear_radial_apply_ae {m N : ℕ}198 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}199 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)200 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ))201 (s : Matrix.MaximalMinorIndex (m + 1) (Fin N)) :202 ∀ᵐ x ∂volume.restrict MX.closedUnitBall,203 derivativeGenerator MX (fun z => A (radialMap Δ z)) x s =204 MX.closedUnitBallVolume * Matrix.maximalMinor (LinearMap.toMatrix' A.toLinearMap) s *205 ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x) := by206 have hae : ∀ᵐ x ∂volume.restrict MX.closedUnitBall,207 DifferentiableAt ℝ (radialMap Δ) x :=208 (lipschitzWith_radialMap Δ).ae_differentiableAt.filter_mono ae_restrict_le209 filter_upwards [hae] with x hx210 exact derivativeGenerator_comp_linear_apply MX A (radialMap Δ) x s hx211212private theorem sphereSet_null {m : ℕ} (M : EquivalentSeminorm (Fin (m + 1) → ℝ)) :213 volume {x | M.p x = 1} = 0 := by214 have hsphere : {x | M.p x = 1} = frontier (M.p.ball 0 1) := by215 ext x216 change M.p x = 1 ↔ x ∈ frontier (M.p.ball 0 1)217 rw [← congrFun M.p.gauge_ball x]218 exact gauge_eq_one_iff_mem_frontier (M.p.convex_ball 0 1)219 (M.p.ball_mem_nhds M.continuous_p zero_lt_one)220 rw [hsphere]221 exact (M.p.convex_ball 0 1).addHaar_frontier volume222223private theorem integral_coordDet_unitBall_eq_openBall {m : ℕ}224 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}225 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :226 ∫ x in MX.closedUnitBall, ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x) ∂volume =227 ∫ x in MX.p.ball 0 1, ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x) ∂volume := by228 apply setIntegral_congr_set229 filter_upwards [measure_eq_zero_iff_ae_notMem.mp (sphereSet_null MX)] with x hx230 have hne : MX.p x ≠ 1 := hx231 apply propext232 change x ∈ MX.closedUnitBall ↔ x ∈ MX.p.ball 0 1233 rw [EquivalentSeminorm.mem_closedUnitBall, Seminorm.mem_ball_zero]234 exact ⟨fun h => lt_of_le_of_ne h hne, le_of_lt⟩235end Internal236open Internal237238/-- Each coordinate of the radial derivative average is the corresponding239linear maximal minor times the signed determinant integral over the source ball. -/240theorem derivativeAverage_comp_linear_radial_apply {m N : ℕ}241 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}242 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)243 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ))244 (q : Matrix.MaximalMinorIndex (m + 1) (Fin N)) :245 derivativeAverage MX (fun x => A (show Fin (m + 1) → ℝ from246 radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from x))) q =247 Matrix.maximalMinor (LinearMap.toMatrix' A.toLinearMap) q *248 ∫ x in MX.p.ball 0 1,249 ContinuousLinearMap.det (fderiv ℝ (fun y : Fin (m + 1) → ℝ =>250 (show Fin (m + 1) → ℝ from radialExtension (X := Space MX) (Y := Space MY) Δ251 (show Space MX from y))) x) ∂volume := by252 change derivativeAverage MX (fun x => A (radialMap Δ x)) q =253 Matrix.maximalMinor (LinearMap.toMatrix' A.toLinearMap) q *254 ∫ x in MX.p.ball 0 1, ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x) ∂volume255 have hcongr :256 (∫ x in MX.closedUnitBall, derivativeGenerator MX (fun z => A (radialMap Δ z)) x q ∂volume) =257 ∫ x in MX.closedUnitBall,258 (MX.closedUnitBallVolume * Matrix.maximalMinor (LinearMap.toMatrix' A.toLinearMap) q) *259 ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x) ∂volume := by260 apply integral_congr_ae261 exact (derivativePlucker_linear_radial_apply_ae Δ A q).mono262 (fun _ hx => by simpa [mul_assoc] using hx)263 have hint := integrableOn_derivativeGenerator_compact MX264 ⟨_, A.lipschitz.comp (lipschitzWith_radialMap Δ)⟩ MX.isCompact_closedUnitBall265 have hcoord : ∀ t : Matrix.MaximalMinorIndex (m + 1) (Fin N),266 Integrable (fun x => derivativeGenerator MX (fun z => A (radialMap Δ z)) x t)267 (volume.restrict MX.closedUnitBall) := fun t => hint.eval t268 rw [derivativeAverage, setAverage_eq, Pi.smul_apply,269 MeasureTheory.eval_integral hcoord q, hcongr,270 integral_const_mul, integral_coordDet_unitBall_eq_openBall Δ]271 change MX.closedUnitBallVolume⁻¹ * (MX.closedUnitBallVolume *272 Matrix.maximalMinor (LinearMap.toMatrix' A.toLinearMap) q *273 (∫ x in MX.p.ball 0 1, ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x) ∂volume)) = _274 rw [mul_assoc MX.closedUnitBallVolume, ← mul_assoc MX.closedUnitBallVolume⁻¹,275 inv_mul_cancel₀ (ne_of_gt MX.closedUnitBallVolume_pos), one_mul]276277private theorem modelOpenBall_volume_eq_ballVolume {m : ℕ}278 (M : EquivalentSeminorm (Fin (m + 1) → ℝ)) :279 (volume (M.p.ball 0 1)).toReal = M.closedUnitBallVolume := by280 have hsphere : {x | M.p x = 1} = frontier (M.p.ball 0 1) := by281 ext x282 change M.p x = 1 ↔ x ∈ frontier (M.p.ball 0 1)283 rw [← congrFun M.p.gauge_ball x]284 exact gauge_eq_one_iff_mem_frontier (M.p.convex_ball 0 1)285 (M.p.ball_mem_nhds M.continuous_p zero_lt_one)286 have hnull : volume {x | M.p x = 1} = 0 := by287 rw [hsphere]288 exact (M.p.convex_ball 0 1).addHaar_frontier volume289 unfold EquivalentSeminorm.closedUnitBallVolume290 apply congrArg ENNReal.toReal291 exact measure_congr (by292 filter_upwards [measure_eq_zero_iff_ae_notMem.mp hnull] with x hx293 have hne : M.p x ≠ 1 := hx294 apply propext295 change x ∈ M.p.ball 0 1 ↔ x ∈ M.closedUnitBall296 simp only [Seminorm.mem_ball_zero, EquivalentSeminorm.mem_closedUnitBall]297 exact ⟨le_of_lt, fun h => lt_of_le_of_ne h hne⟩)298299namespace Internal300private def radialOpenData {m : ℕ}301 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}302 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :303 BilipschitzOrientation.BiLipschitzOpenData (m + 1) where304 source := MX.p.ball 0 1305 target := MY.p.ball 0 1306 isOpen_source := isOpen_openBall MX307 isOpen_target := isOpen_openBall MY308 f := radialMap Δ309 g := radialMap Δ.symm310 mapsTo_f := by intro x hx; simpa using hx311 mapsTo_g := by intro x hx; simpa using hx312 left_inv := by intro x _; exact radialMap_leftInverse Δ x313 right_inv := by intro x _; exact radialMap_leftInverse Δ.symm x314 fConstant := (3 * MX.upper / MY.lower).toNNReal315 lipschitzWith_f := lipschitzWith_radialMap Δ316 gConstant := (3 * MY.upper / MX.lower).toNNReal317 lipschitzWith_g := lipschitzWith_radialMap Δ.symm318 lower := referenceAntiConstant MX MY319 lower_pos := referenceAntiConstant_pos MX MY320 anti := radialMap_lower Δ321322private theorem isConnected_piolaData {m : ℕ}323 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}324 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :325 IsConnected (radialOpenData Δ).source ∧326 IsConnected (radialOpenData Δ).target :=327 ⟨isConnected_openBall MX, isConnected_openBall MY⟩328end Internal329330331/-- The full radial average is exactly one orientation sign times the target332generator. No contraction hypothesis on the linear map is introduced. -/333theorem derivativeAverage_comp_linear_radial {m N : ℕ}334 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}335 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)336 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) :337 ∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧338 derivativeAverage MX (fun x => A (show Fin (m + 1) → ℝ from339 radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from x))) =340 ε • Matrix.ballVolumeScaledMaximalMinors MY A := by341 let D := radialOpenData Δ342 have hpos : 0 < volume D.target := by343 change 0 < volume (MY.p.ball 0 1)344 exact volume_pos_of_isOpen_of_nonempty (isOpen_openBall MY) ⟨0, by simp⟩345 have hfinite : volume D.target ≠ ∞ :=346 ne_top_of_le_ne_top MY.isCompact_closedUnitBall.measure_ne_top347 (measure_mono (by348 intro x hx349 exact MY.mem_closedUnitBall.mpr (le_of_lt (by simpa [D, radialOpenData] using hx))))350 obtain ⟨ε, hε, hs⟩ := BilipschitzOrientation.integral_det_fderiv_eq_signed_volume351 D (isConnected_piolaData Δ).2.isPreconnected hpos hfinite352 change (∫ x in MX.p.ball 0 1, ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x) ∂volume) =353 ε * (volume (MY.p.ball 0 1)).toReal at hs354 rw [modelOpenBall_volume_eq_ballVolume MY] at hs355 refine ⟨ε, hε, ?_⟩356 ext q357 rw [derivativeAverage_comp_linear_radial_apply Δ A q]358 change Matrix.maximalMinor (LinearMap.toMatrix' A.toLinearMap) q *359 (∫ x in MX.p.ball 0 1, ContinuousLinearMap.det (fderiv ℝ (radialMap Δ) x) ∂volume) = _360 rw [hs]361 simp only [Pi.smul_apply, Matrix.ballVolumeScaledMaximalMinors,362 Matrix.maximalMinors, smul_eq_mul]363 ring364365namespace Internal366private def piolaOrientationConcreteSignedRadialData {m : ℕ}367 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))368 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :369 SignedRadialData MX MY Δ where370 radial := radialMap Δ371 lipschitz := exists_lipschitzWith_radialMap Δ372 radial_coe_unitSphere := by373 intro u374 exact radialExtension_on_sphere Δ375 ⟨(show Space MX from u.val), mem_sphere_zero_iff_norm.mpr u.property⟩376 average_linear_comp := by377 intro N A _hA378 exact derivativeAverage_comp_linear_radial Δ A379end Internal380end MathlibAnnex.Plucker