Exact source: MathlibAnnex/Analysis/Normed/Plucker/BodyInvariance.lean
Pinned GitHub source · Raw UTF-8 source
Back to Sphere isometries preserve the Plücker body
1import MathlibAnnex.Analysis.Normed.Plucker.BoundaryExtension2import MathlibAnnex.Analysis.Normed.Plucker.RadialAverage3import MathlibAnnex.MeasureTheory.Integral.MaximalMinorBoundary4import MathlibAnnex.Analysis.Convex.PluckerBody56/-! # Plücker bodies are invariant under sphere isometries78The boundary extension supplies source-body membership. The accepted boundary9null-Lagrangian theorem transfers its derivative average to the radial map.10The radial average gives an explicit scalar sign, removed using generator sign11symmetry. Equality uses both inclusions, the first from the inverse isometry.12The source positive-dimension boundary `m + 1` is retained throughout.13-/1415noncomputable section16open Set Metric Function MeasureTheory17open scoped NNReal ENNReal BigOperators18namespace MathlibAnnex.PluckerBody19open EquivalentSeminorm Sphere Plucker2021-- Exact private coordinate adapters from the accepted B1/B2 sources.22private abbrev radialMap {n : ℕ}23 {MX MY : EquivalentSeminorm (Fin n → ℝ)}24 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)25 (x : Fin n → ℝ) : Fin n → ℝ :=26 show Fin n → ℝ from radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from x)2728@[simp] private theorem radialMap_p {n : ℕ}29 {MX MY : EquivalentSeminorm (Fin n → ℝ)}30 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x : Fin n → ℝ) :31 MY.p (radialMap Δ x) = MX.p x := radialExtension_norm Δ (show Space MX from x)3233private theorem radialMap_leftInverse {n : ℕ}34 {MX MY : EquivalentSeminorm (Fin n → ℝ)}35 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :36 LeftInverse (radialMap Δ.symm) (radialMap Δ) :=37 fun x => radialExtension_leftInverse Δ (show Space MX from x)3839private theorem radialMap_model_dist {n : ℕ}40 {MX MY : EquivalentSeminorm (Fin n → ℝ)}41 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x y : Fin n → ℝ) :42 MY.p (radialMap Δ x - radialMap Δ y) ≤ 3 * MX.p (x - y) := by43 have h := (lipschitzWith_radialExtension Δ).dist_le_mul44 (show Space MX from x) (show Space MX from y)45 simpa only [dist_space_eq, NNReal.coe_ofNat] using h4647private theorem lipschitzWith_radialMap {n : ℕ}48 {MX MY : EquivalentSeminorm (Fin n → ℝ)}49 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :50 LipschitzWith (3 * MX.upper / MY.lower).toNNReal (radialMap Δ) := by51 have hC : 0 ≤ 3 * MX.upper / MY.lower := div_nonneg (mul_nonneg (by norm_num) MX.upper_pos.le) MY.lower_pos.le52 refine LipschitzWith.of_dist_le_mul ?_53 intro x y54 have hlower := MY.lower_le (radialMap Δ x - radialMap Δ y)55 have hmodel := radialMap_model_dist Δ x y56 have hupper := MX.le_upper (x - y)57 rw [Real.coe_toNNReal _ hC, dist_eq_norm, dist_eq_norm]58 calc59 ‖radialMap Δ x - radialMap Δ y‖ ≤ (3 * MX.upper * ‖x - y‖) / MY.lower :=60 (le_div_iff₀ MY.lower_pos).2 (by nlinarith)61 _ = (3 * MX.upper / MY.lower) * ‖x - y‖ := by ring6263private def coordinateBoundaryData {m N : ℕ}64 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}65 (Δ : Metric.sphere (0 : Space MX) 1 ≃ᵢ Metric.sphere (0 : Space MY) 1)66 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) : MX.unitSphere → (Fin N → ℝ) :=67 fun u => A (show Fin (m + 1) → ℝ from68 (Δ ⟨(show Space MX from u.val), mem_sphere_zero_iff_norm.mpr u.property⟩).val)6970private theorem norm_coordinateBoundaryData_sub_le_seminorm_sub {m N : ℕ}71 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}72 (Δ : Metric.sphere (0 : Space MX) 1 ≃ᵢ Metric.sphere (0 : Space MY) 1)73 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) (hA : MY.IsContraction A) :74 ∀ u v, ‖coordinateBoundaryData Δ A u - coordinateBoundaryData Δ A v‖ ≤75 MX.p ((u : Fin (m + 1) → ℝ) - (v : Fin (m + 1) → ℝ)) := by76 intro u v77 let u' : Metric.sphere (0 : Space MX) 1 :=78 ⟨(show Space MX from u.val), mem_sphere_zero_iff_norm.mpr u.property⟩79 let v' : Metric.sphere (0 : Space MX) 1 :=80 ⟨(show Space MX from v.val), mem_sphere_zero_iff_norm.mpr v.property⟩81 have chord : MY.p ((show Fin (m + 1) → ℝ from (Δ u').val) -82 (show Fin (m + 1) → ℝ from (Δ v').val)) = MX.p (u.val - v.val) := by83 simpa only [Subtype.dist_eq, dist_space_eq] using Δ.isometry.dist_eq u' v'84 calc85 ‖coordinateBoundaryData Δ A u - coordinateBoundaryData Δ A v‖ =86 ‖A ((show Fin (m + 1) → ℝ from (Δ u').val) -87 (show Fin (m + 1) → ℝ from (Δ v').val))‖ := by88 simp [coordinateBoundaryData, u', v', map_sub]89 _ ≤ MY.p ((show Fin (m + 1) → ℝ from (Δ u').val) -90 (show Fin (m + 1) → ℝ from (Δ v').val)) := hA _91 _ = MX.p (u.val - v.val) := chord929394private theorem derivativeGenerator_apply_eq {n N : ℕ}95 (M : EquivalentSeminorm (Fin n → ℝ))96 (s : Matrix.MaximalMinorIndex n (Fin N))97 (f : (Fin n → ℝ) → (Fin N → ℝ)) (x : Fin n → ℝ) :98 derivativeGenerator M f x s =99 M.closedUnitBallVolume * NullLagrangian.maximalMinorIntegrand s f x := by100 simp only [derivativeGenerator, Matrix.ballVolumeScaledMaximalMinors,101 Pi.smul_apply, Matrix.maximalMinors, smul_eq_mul,102 NullLagrangian.maximalMinorIntegrand, ContinuousLinearMap.det_selectedSquare]103104private theorem average_apply_eq_integral {n N : ℕ}105 (M : EquivalentSeminorm (Fin n → ℝ))106 (s : Matrix.MaximalMinorIndex n (Fin N)) (f : (Fin n → ℝ) → (Fin N → ℝ))107 (hint : IntegrableOn (derivativeGenerator M f) M.closedUnitBall volume) :108 derivativeAverage M f s =109 ∫ x in M.closedUnitBall, NullLagrangian.maximalMinorIntegrand s f x := by110 have hcoord : ∀ t : Matrix.MaximalMinorIndex n (Fin N),111 Integrable (fun x => derivativeGenerator M f x t)112 (volume.restrict M.closedUnitBall) := fun t => hint.eval t113 rw [derivativeAverage, setAverage_eq, Pi.smul_apply, MeasureTheory.eval_integral hcoord s]114 simp_rw [derivativeGenerator_apply_eq M s f]115 rw [integral_const_mul]116 change M.closedUnitBallVolume⁻¹ * (M.closedUnitBallVolume *117 (∫ x in M.closedUnitBall, NullLagrangian.maximalMinorIntegrand s f x)) = _118 rw [← mul_assoc, inv_mul_cancel₀ (ne_of_gt M.closedUnitBallVolume_pos), one_mul]119120private theorem average_eq_of_trace {m N : ℕ}121 (M : EquivalentSeminorm (Fin (m + 1) → ℝ))122 {F G : (Fin (m + 1) → ℝ) → (Fin N → ℝ)} {CF CG : ℝ≥0}123 (hF : LipschitzWith CF F) (hG : LipschitzWith CG G)124 (htrace : ∀ x, M.p x = 1 → F x = G x) :125 derivativeAverage M F = derivativeAverage M G := by126 ext s127 rw [average_apply_eq_integral M s F128 (integrableOn_derivativeGenerator_compact M ⟨CF, hF⟩ M.isCompact_closedUnitBall),129 average_apply_eq_integral M s G130 (integrableOn_derivativeGenerator_compact M ⟨CG, hG⟩ M.isCompact_closedUnitBall)]131 exact NullLagrangian.integral_maximalMinor_eq_of_pointwise_boundary_eq132 M.p M.continuous_p M.isCompact_closedUnitBall s hF hG htrace133134/-- A normalized target generator belongs to the source body under a unit-sphere isometry. -/135theorem normalizedGenerator_mem_of_sphereIsometry {m N : ℕ}136 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}137 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)138 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) (hA : MY.IsContraction A) :139 Matrix.ballVolumeScaledMaximalMinors MY A ∈ body MX N := by140 let g := coordinateBoundaryData Δ A141 -- SR-SOURCE-B72: obtain exactly the public existential's average-membership field.142 obtain ⟨f, hf, htrace, _hderiv, _hint, hmem⟩ :=143 exists_extension_with_derivativeAverage_mem MX g144 (norm_coordinateBoundaryData_sub_le_seminorm_sub Δ A hA)145 have hfl : LipschitzWith ⟨MX.upper, MX.upper_pos.le⟩ f := by146 refine LipschitzWith.of_dist_le_mul ?_147 intro x y148 change ‖f x - f y‖ ≤ MX.upper * ‖x - y‖149 exact (hf x y).trans (MX.le_upper (x - y))150 have hgl := A.lipschitz.comp (lipschitzWith_radialMap Δ)151 have hboundary : ∀ x, MX.p x = 1 → f x = A (radialMap Δ x) := by152 intro x hx153 rw [htrace ⟨x, hx⟩]154 dsimp [g, coordinateBoundaryData]155 congr 1156 exact (radialExtension_on_sphere Δ157 ⟨(show Space MX from x), mem_sphere_zero_iff_norm.mpr hx⟩).symm158 have havg := average_eq_of_trace MX hfl hgl hboundary159 obtain ⟨ε, hε, hs⟩ := derivativeAverage_comp_linear_radial Δ A160 have hs' : derivativeAverage MX (fun x => A (radialMap Δ x)) =161 ε • Matrix.ballVolumeScaledMaximalMinors MY A := hs162 have hsigned : ε • Matrix.ballVolumeScaledMaximalMinors MY A ∈ body MX N := by163 exact (havg.trans hs') ▸ hmem164 rcases hε with rfl | rfl165 · simpa only [one_smul] using hsigned166 · have hn : -Matrix.ballVolumeScaledMaximalMinors MY A ∈ body MX N := by167 simpa only [neg_one_smul] using hsigned168 simpa only [neg_neg] using body_neg MX hn169170/-- Both signs of every raw target generator belong to the source body. -/171theorem rawGenerators_subset_of_sphereIsometry {m N : ℕ}172 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}173 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :174 generators MY N ⊆ body MX N := by175 rintro z ⟨A, hA, rfl | rfl⟩176 · exact normalizedGenerator_mem_of_sphereIsometry Δ A hA177 · exact body_neg MX (normalizedGenerator_mem_of_sphereIsometry Δ A hA)178179/-- The target body is contained in the source body. -/180theorem subset_of_sphereIsometry {m N : ℕ}181 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}182 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :183 body MY N ⊆ body MX N := by184 exact convexHull_min (rawGenerators_subset_of_sphereIsometry Δ)185 (convex_convexHull ℝ (generators MX N))186187/-- Equality follows from the two inclusions furnished by the isometry and its inverse. -/188theorem eq_of_sphereIsometry {m N : ℕ}189 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}190 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :191 body MX N = body MY N := by192 apply Set.Subset.antisymm193 · exact subset_of_sphereIsometry Δ.symm194 · exact subset_of_sphereIsometry Δ195196end MathlibAnnex.PluckerBody