Exact source: MathlibAnnex/Analysis/Normed/Operator/PluckerSupport.lean
Pinned GitHub source · Raw UTF-8 source
Back to The chosen support slice consists of almost-isometric generators
1import MathlibAnnex.Analysis.Normed.Operator.FiniteSup2import MathlibAnnex.LinearAlgebra.Matrix.VolumeScaledMaximalMinor3import MathlibAnnex.LinearAlgebra.Matrix.MaximalMinor4import MathlibAnnex.LinearAlgebra.Matrix.MaximalMinorFactorization56noncomputable section7set_option autoImplicit false8open Set Module9open scoped BigOperators NNReal10namespace MathlibAnnex.PluckerSupport11universe u12open Satellite13private abbrev Coord (n : ℕ) := Fin n → ℝ14private abbrev NormModel (n : ℕ) := EquivalentSeminorm (Coord n)15private abbrev DualFrame (n : ℕ) := DeterminantFrame.Frame n (Coord n)16private abbrev dualFrameMatrix {n : ℕ} := DeterminantFrame.frameMatrix (Pi.basisFun ℝ (Fin n))17private abbrev frameDet {n : ℕ} := DeterminantFrame.frameDeterminant (Pi.basisFun ℝ (Fin n))18private abbrev replacementDet {n : ℕ} := DeterminantFrame.replacementDeterminant (Pi.basisFun ℝ (Fin n))19private abbrev frameCoordinates {n : ℕ} := @DeterminantFrame.frameCoordinates n (Coord n) _ _20private abbrev framePreimage {n : ℕ} (B : DualFrame n) (c : Coord n) := (dualFrameMatrix B)⁻¹.mulVec c21private abbrev IsDualContraction {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) := ∀ x, |r x| ≤ M.p x22private abbrev dualRowSet {n : ℕ} (M : NormModel n) := {r : Coord n →L[ℝ] ℝ | IsDualContraction M r}23private abbrev dualFrameSet {n : ℕ} (M : NormModel n) := {B : DualFrame n | ∀ i, IsDualContraction M (B i)}2425private instance modelFiniteDimensional {n : ℕ} (M : NormModel n) : FiniteDimensional ℝ (EquivalentSeminorm.Space M) :=26 inferInstanceAs (FiniteDimensional ℝ (Coord n))2728private def modelBasis {n : ℕ} (M : NormModel n) : Basis (Fin n) ℝ (EquivalentSeminorm.Space M) :=29 Pi.basisFun ℝ (Fin n)3031private def toModelRow {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :32 EquivalentSeminorm.Space M →L[ℝ] ℝ :=33 LinearMap.toContinuousLinearMap (show EquivalentSeminorm.Space M →ₗ[ℝ] ℝ from r.toLinearMap)3435private def fromModelRow {n : ℕ} (M : NormModel n) (r : EquivalentSeminorm.Space M →L[ℝ] ℝ) :36 Coord n →L[ℝ] ℝ :=37 LinearMap.toContinuousLinearMap (show Coord n →ₗ[ℝ] ℝ from r.toLinearMap)3839private theorem toModelRow_mem_iff {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :40 toModelRow M r ∈ DeterminantFrame.unitRowSet (EquivalentSeminorm.Space M) ↔ IsDualContraction M r := by41 rw [DeterminantFrame.mem_unitRowSet]42 constructor43 · intro h x44 have := (toModelRow M r).le_opNorm (show EquivalentSeminorm.Space M from x)45 change |r x| ≤ ‖toModelRow M r‖ * M.p x at this46 exact this.trans (by nlinarith [apply_nonneg M.p x])47 · intro h48 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one49 intro x50 change |r (show Coord n from x)| ≤ 1 * M.p (show Coord n from x)51 simpa only [one_mul] using h (show Coord n from x)5253private abbrev detMax {n : ℕ} (M : NormModel n) := DeterminantFrame.determinantMaximum (modelBasis M)54private abbrev NearMaxInverseBound {n : ℕ} (M : NormModel n) := DeterminantFrame.NearMaxInverseBound (modelBasis M)55private abbrev nearMaxFrames {n : ℕ} (M : NormModel n) (η : ℝ) := {B : DualFrame n | B ∈ dualFrameSet M ∧ detMax M - η ≤ |frameDet B|}5657private theorem toModelFrame_mem {n : ℕ} (M : NormModel n) {B : DualFrame n} (h : B ∈ dualFrameSet M) :58 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.unitFrameSet n (EquivalentSeminorm.Space M) := by59 intro i60 exact (toModelRow_mem_iff M (B i)).mpr (h i)6162private theorem toModelFrame_near {n : ℕ} (M : NormModel n) {η : ℝ} {B : DualFrame n} (h : B ∈ nearMaxFrames M η) :63 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.nearMaxFrames (modelBasis M) η :=64 ⟨toModelFrame_mem M h.1, h.2⟩6566private theorem seminorm_framePreimage_le {n : ℕ} (M : NormModel n) {η : ℝ} (H : NearMaxInverseBound M η) {B : DualFrame n}67 (h : B ∈ nearMaxFrames M η) (c : Coord n) : M.p (framePreimage B c) ≤ H.boundConstant * ‖c‖ := by68 exact H.bound (toModelFrame_near M h) c6970private theorem detMax_pos {n : ℕ} (M : NormModel n) : 0 < detMax M :=71 DeterminantFrame.determinantMaximum_pos (modelBasis M)7273private theorem nearMaxFrame_det_ne_zero {n : ℕ} (M : NormModel n) {η : ℝ}74 (hη : η < detMax M) {B : DualFrame n} (hB : B ∈ nearMaxFrames M η) : frameDet B ≠ 0 :=75 DeterminantFrame.nearMaxFrame_det_ne_zero (modelBasis M) hη (toModelFrame_near M hB)7677private theorem inverse_mulVec_frameCoordinates {n : ℕ} (M : NormModel n) {η : ℝ}78 (hη : η < detMax M) {B : DualFrame n} (hB : B ∈ nearMaxFrames M η) (x : Coord n) :79 framePreimage B (frameCoordinates B x) = x := by80 exact DeterminantFrame.inverse_mulVec_frameCoordinates (modelBasis M) hη (toModelFrame_near M hB) (show EquivalentSeminorm.Space M from x)8182private theorem abs_replacementDet_le_detMax {n : ℕ} (M : NormModel n) {B : DualFrame n} (hB : B ∈ dualFrameSet M)83 (i : Fin n) {r : Coord n →L[ℝ] ℝ} (hr : IsDualContraction M r) : |replacementDet B i r| ≤ detMax M := by84 have h := DeterminantFrame.abs_replacementDeterminant_le_maximum (modelBasis M) (toModelFrame_mem M hB) i ((toModelRow_mem_iff M r).mpr hr)85 have heq : (fun j => toModelRow M ((DeterminantFrame.replaceRow B i r) j)) =86 DeterminantFrame.replaceRow (fun j => toModelRow M (B j)) i (toModelRow M r) := by87 funext j88 by_cases hj : j = i <;> simp [DeterminantFrame.replaceRow, hj]89 change |DeterminantFrame.frameDeterminant (modelBasis M)90 (fun j => toModelRow M ((DeterminantFrame.replaceRow B i r) j))| ≤ detMax M91 rw [heq]92 exact h9394private def maxFrame {n : ℕ} (M : NormModel n) : DualFrame n :=95 fun i => fromModelRow M (DeterminantFrame.maximizingFrame (modelBasis M) i)9697private theorem maxFrame_det {n : ℕ} (M : NormModel n) : |frameDet (maxFrame M)| = detMax M := rfl9899private theorem maxFrame_mem {n : ℕ} (M : NormModel n) : maxFrame M ∈ dualFrameSet M := by100 intro i101 apply (toModelRow_mem_iff M _).mp102 have h := DeterminantFrame.maximizingFrame_mem (modelBasis M) i103 convert h using 1104 ext x105 rfl106107108private abbrev replaceFrameRow {n : ℕ} := @DeterminantFrame.replaceRow n (Coord n) _ _109private abbrev functionalRow {n : ℕ} := DeterminantFrame.functionalCoordinates (Pi.basisFun ℝ (Fin n))110private theorem continuous_frameDet {n : ℕ} : Continuous (frameDet : DualFrame n → ℝ) :=111 DeterminantFrame.continuous_frameDeterminant (Pi.basisFun ℝ (Fin n))112private theorem dualFrameMatrix_replaceFrameRow {n : ℕ} (B : DualFrame n) (i : Fin n) (r : Coord n →L[ℝ] ℝ) :113 dualFrameMatrix (replaceFrameRow B i r) = (dualFrameMatrix B).updateRow i (functionalRow r) :=114 DeterminantFrame.frameMatrix_replaceRow (Pi.basisFun ℝ (Fin n)) B i r115private theorem sum_mul_replacementDet {n : ℕ} (B : DualFrame n) (hB : frameDet B ≠ 0) (r : Coord n →L[ℝ] ℝ) (c : Coord n) :116 (∑ i : Fin n, c i * replacementDet B i r) = frameDet B * r (framePreimage B c) :=117 DeterminantFrame.sum_mul_replacementDeterminant (Pi.basisFun ℝ (Fin n)) B hB r c118119private theorem isCompact_dualRowSet {n : ℕ} (M : NormModel n) : IsCompact (dualRowSet M) := by120 have hc : IsClosed (dualRowSet M) := by121 have heq : dualRowSet M = (⋂ x : Coord n, {r : Coord n →L[ℝ] ℝ | |r x| ≤ M.p x}) := by ext r; simp [dualRowSet, IsDualContraction]122 rw [heq]123 exact isClosed_iInter fun x => isClosed_le (by fun_prop) continuous_const124 have hb : Bornology.IsBounded (dualRowSet M) := by125 apply (Metric.isBounded_iff_subset_closedBall (0 : Coord n →L[ℝ] ℝ)).2126 refine ⟨M.upper, ?_⟩127 intro r hr128 rw [Metric.mem_closedBall, dist_zero_right]129 apply ContinuousLinearMap.opNorm_le_bound _ M.upper_pos.le130 intro x131 exact (hr x).trans (M.le_upper x)132 exact Metric.isCompact_of_isClosed_isBounded hc hb133134private theorem isCompact_dualFrameSet {n : ℕ} (M : NormModel n) : IsCompact (dualFrameSet M) := by135 have heq : dualFrameSet M = Set.univ.pi (fun _ : Fin n => dualRowSet M) := by ext B; simp [dualFrameSet, dualRowSet]136 rw [heq]137 exact isCompact_univ_pi fun _ => isCompact_dualRowSet M138139140private abbrev SupCoord (n : ℕ) := Fin n → ℝ141142open FiniteSup FiniteSup.Bridge143namespace Internal144end Internal145open Internal146147private abbrev MinorIndex (n N : ℕ) := MathlibAnnex.Matrix.MaximalMinorIndex n (Fin N)148private abbrev PluckerCoord (n N : ℕ) := MinorIndex n N → ℝ149private abbrev clmMatrix {n N : ℕ} (A : Coord n →L[ℝ] SupCoord N) := LinearMap.toMatrix' A.toLinearMap150private abbrev maximalMinor := @MathlibAnnex.Matrix.maximalMinor151private abbrev maximalMinors := @MathlibAnnex.Matrix.maximalMinors152private abbrev selectedSubmatrix := @MathlibAnnex.Matrix.maximalSubmatrix153private abbrev minorIndexOfOrderEmbedding := @MathlibAnnex.Matrix.MaximalMinorIndex.ofOrderEmbedding154private abbrev selectedSubmatrix_minorIndexOfOrderEmbedding := @MathlibAnnex.Matrix.maximalSubmatrix_ofOrderEmbedding155private abbrev maximalMinor_minorIndexOfOrderEmbedding := @MathlibAnnex.Matrix.maximalMinor_ofOrderEmbedding156private abbrev normalizedPlucker := @MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors157private def pluckerFunctional {n N : ℕ} (w : PluckerCoord n N) : PluckerCoord n N →L[ℝ] ℝ :=158 ∑ i, w i • ContinuousLinearMap.proj i159private theorem pluckerFunctional_apply {n N : ℕ} (w z : PluckerCoord n N) : pluckerFunctional w z = dotProduct w z := by160 simp [pluckerFunctional, dotProduct]161variable {m : ℕ} {J : Type u} [Fintype J]162163private abbrev positiveSatelliteAmbientDim (m : ℕ) (J : Type u) [Fintype J] : ℕ :=164 (m + 1) + Fintype.card J165166private def baseRowIndex (J : Type u) [Fintype J] (i : Fin (m + 1)) :167 Fin (positiveSatelliteAmbientDim m J) :=168 Fin.castAdd (Fintype.card J) i169170private noncomputable def satelliteRowIndex (m : ℕ) (J : Type u) [Fintype J] (a : J) :171 Fin (positiveSatelliteAmbientDim m J) :=172 Fin.natAdd (m + 1) (Fintype.equivFin J a)173174private noncomputable def baseRowOrderEmb (m : ℕ) (J : Type u) [Fintype J] :175 Fin (m + 1) ↪o Fin (positiveSatelliteAmbientDim m J) :=176 Fin.castAddOrderEmb (Fintype.card J)177178@[simp] private theorem baseRowOrderEmb_apply (i : Fin (m + 1)) :179 baseRowOrderEmb m J i = baseRowIndex J i := by180 rfl181182private def replacementSortedRow (i : Fin (m + 1)) (a : J) :183 Fin (m + 1) → Fin (positiveSatelliteAmbientDim m J) :=184 Fin.snoc185 (fun k : Fin m => baseRowIndex J (i.succAbove k))186 (satelliteRowIndex m J a)187188private theorem replacementSortedRow_strictMono (i : Fin (m + 1)) (a : J) :189 StrictMono (replacementSortedRow i a) := by190 intro x y hxy191 cases y using Fin.lastCases with192 | last =>193 cases x using Fin.lastCases with194 | last => exact (lt_irrefl _ hxy).elim195 | cast x =>196 simp [replacementSortedRow, baseRowIndex, satelliteRowIndex,197 Fin.lt_def]198 omega199 | cast y =>200 have hxlast : x ≠ Fin.last m := ne_of_lt (hxy.trans_le (Fin.le_last _))201 obtain ⟨x', hx⟩ := Fin.eq_castSucc_of_ne_last hxlast202 subst x203 have hbase :204 (baseRowOrderEmb m J) (i.succAbove x') <205 (baseRowOrderEmb m J) (i.succAbove y) :=206 (baseRowOrderEmb m J).lt_iff_lt.mpr207 ((i.succAboveOrderEmb).lt_iff_lt.mpr208 (Fin.castSucc_lt_castSucc_iff.mp hxy))209 simpa only [replacementSortedRow, Fin.snoc_castSucc,210 baseRowOrderEmb_apply] using hbase211212private noncomputable def replacementSortedOrderEmb (i : Fin (m + 1)) (a : J) :213 Fin (m + 1) ↪o Fin (positiveSatelliteAmbientDim m J) :=214 OrderEmbedding.ofStrictMono (replacementSortedRow i a)215 (replacementSortedRow_strictMono i a)216217private noncomputable def baseMinorIndex :218 MinorIndex (m + 1) (positiveSatelliteAmbientDim m J) :=219 minorIndexOfOrderEmbedding (baseRowOrderEmb m J)220221private noncomputable def replacementMinorIndex (i : Fin (m + 1)) (a : J) :222 MinorIndex (m + 1) (positiveSatelliteAmbientDim m J) :=223 minorIndexOfOrderEmbedding (replacementSortedOrderEmb i a)224225private noncomputable def replacementMovePerm (i : Fin (m + 1)) :226 Equiv.Perm (Fin (m + 1)) :=227 (Fin.cycleIcc i (Fin.last m)).symm228229private noncomputable def replacementParity (i : Fin (m + 1)) : ℝ :=230 (((Equiv.Perm.sign (replacementMovePerm i) : Units ℤ) : ℤ) : ℝ)231232@[simp] private theorem replacementParity_abs (i : Fin (m + 1)) :233 |replacementParity i| = 1 := by234 unfold replacementParity235 have hsign :236 |(((Equiv.Perm.sign (replacementMovePerm i) : Units ℤ) : ℤ))| = 1 :=237 Equiv.Perm.sign_abs (replacementMovePerm i)238 exact_mod_cast hsign239240private theorem maximalMinor_configurationFinMap_base241 (C : SatelliteConfiguration (m + 1) J) :242 maximalMinor (clmMatrix (configurationFinMap C))243 (baseMinorIndex (m := m) (J := J)) = frameDet C.1 := by244 unfold baseMinorIndex245 unfold maximalMinor minorIndexOfOrderEmbedding246 rw [MathlibAnnex.Matrix.maximalMinor_ofOrderEmbedding]247 congr 1248 ext i j249 simp [baseRowOrderEmb, clmMatrix, dualFrameMatrix, DeterminantFrame.frameMatrix, Pi.basisFun_apply, frameDet, DeterminantFrame.frameDeterminant]250251@[simp] private theorem replacementMovePerm_apply_self (i : Fin (m + 1)) :252 replacementMovePerm i i = Fin.last m := by253 unfold replacementMovePerm254 apply (Fin.cycleIcc i (Fin.last m)).injective255 simp only [Equiv.apply_symm_apply]256 exact (Fin.cycleIcc_of_last (Fin.le_last i)).symm257258@[simp] private theorem replacementMovePerm_apply_succAbove259 (i : Fin (m + 1)) (k : Fin m) :260 replacementMovePerm i (i.succAbove k) = Fin.castSucc k := by261 unfold replacementMovePerm262 apply (Fin.cycleIcc i (Fin.last m)).injective263 simp only [Equiv.apply_symm_apply]264 have hcycle := congrFun265 (Fin.cycleIcc_comp_succAbove i (Fin.last m) (Fin.le_last i)) k266 simpa [Function.comp_apply] using hcycle.symm267268private theorem replaceFrame_matrix_eq_permuted_selected269 (C : SatelliteConfiguration (m + 1) J)270 (i : Fin (m + 1)) (a : J) :271 dualFrameMatrix (replaceFrameRow C.1 i (C.2 a)) =272 (selectedSubmatrix (clmMatrix (configurationFinMap C))273 (replacementMinorIndex i a)).submatrix274 (replacementMovePerm i) id := by275 unfold replacementMinorIndex276 unfold selectedSubmatrix minorIndexOfOrderEmbedding277 rw [MathlibAnnex.Matrix.maximalSubmatrix_ofOrderEmbedding]278 ext k j279 simp only [replacementSortedOrderEmb, OrderEmbedding.coe_ofStrictMono,280 Matrix.submatrix_apply, id_eq]281 simp only [dualFrameMatrix, DeterminantFrame.frameMatrix, Pi.basisFun_apply]282 change283 (replaceFrameRow C.1 i (C.2 a) k) (Pi.single j 1) =284 configurationFinMap C (Pi.single j 1)285 (replacementSortedRow i a (replacementMovePerm i k))286 by_cases hki : k = i287 · subst k288 simp [replaceFrameRow, DeterminantFrame.replaceRow, replacementSortedRow, satelliteRowIndex]289 · obtain ⟨r, rfl⟩ := Fin.exists_succAbove_eq hki290 simp [replaceFrameRow, DeterminantFrame.replaceRow, replacementSortedRow, baseRowIndex]291292private theorem replacementParity_mul_maximalMinor293 (C : SatelliteConfiguration (m + 1) J)294 (i : Fin (m + 1)) (a : J) :295 replacementParity i *296 maximalMinor (clmMatrix (configurationFinMap C))297 (replacementMinorIndex i a) =298 replacementDet C.1 i (C.2 a) := by299 have hperm := Matrix.det_permute (replacementMovePerm i)300 (selectedSubmatrix (clmMatrix (configurationFinMap C))301 (replacementMinorIndex i a))302 rw [← replaceFrame_matrix_eq_permuted_selected C i a] at hperm303 simpa [replacementParity, replacementDet, frameDet, maximalMinor, MathlibAnnex.Matrix.maximalMinor, selectedSubmatrix, DeterminantFrame.replacementDeterminant, DeterminantFrame.frameDeterminant] using hperm.symm304305noncomputable def satellitePluckerCoefficients306 (weight : ℝ) (coeff : J → Coord (m + 1)) :307 PluckerCoord (m + 1) (positiveSatelliteAmbientDim m J) :=308 weight • Pi.single (baseMinorIndex (m := m) (J := J)) 1 +309 ∑ a : J, ∑ i : Fin (m + 1),310 (coeff a i * replacementParity i) •311 Pi.single (replacementMinorIndex i a) 1312313theorem pluckerPairing_satelliteCoefficients_maximalMinors314 (weight : ℝ) (coeff : J → Coord (m + 1))315 (C : SatelliteConfiguration (m + 1) J) :316 dotProduct (satellitePluckerCoefficients weight coeff)317 (maximalMinors (clmMatrix (configurationFinMap C))) =318 configurationPolynomial weight coeff C := by319 classical320 simp only [satellitePluckerCoefficients, add_dotProduct,321 smul_dotProduct, single_dotProduct, one_mul]322 change weight * maximalMinor (clmMatrix (configurationFinMap C))323 (baseMinorIndex (m := m) (J := J)) +324 dotProduct325 (∑ a : J, ∑ i : Fin (m + 1),326 (coeff a i * replacementParity i) •327 Pi.single (replacementMinorIndex i a) 1)328 (maximalMinors (clmMatrix (configurationFinMap C))) =329 configurationPolynomial weight coeff C330 rw [maximalMinor_configurationFinMap_base C]331 simp only [configurationPolynomial, satellitePolynomial]332 congr 1333 have pair_sum_left_J334 (ω : J → PluckerCoord (m + 1) (positiveSatelliteAmbientDim m J))335 (z : PluckerCoord (m + 1) (positiveSatelliteAmbientDim m J)) :336 dotProduct (∑ a : J, ω a) z =337 ∑ a : J, dotProduct (ω a) z := by338 unfold dotProduct339 simp only [Finset.sum_apply, Finset.sum_mul]340 rw [Finset.sum_comm]341 have pair_sum_left_Fin342 (ω : Fin (m + 1) →343 PluckerCoord (m + 1) (positiveSatelliteAmbientDim m J))344 (z : PluckerCoord (m + 1) (positiveSatelliteAmbientDim m J)) :345 dotProduct (∑ i : Fin (m + 1), ω i) z =346 ∑ i : Fin (m + 1), dotProduct (ω i) z := by347 unfold dotProduct348 simp only [Finset.sum_apply, Finset.sum_mul]349 rw [Finset.sum_comm]350 calc351 dotProduct352 (∑ a : J, ∑ i : Fin (m + 1),353 (coeff a i * replacementParity i) •354 Pi.single (replacementMinorIndex i a) 1)355 (maximalMinors (clmMatrix (configurationFinMap C))) =356 ∑ a : J, dotProduct357 (∑ i : Fin (m + 1),358 (coeff a i * replacementParity i) •359 Pi.single (replacementMinorIndex i a) 1)360 (maximalMinors (clmMatrix (configurationFinMap C))) := by361 exact pair_sum_left_J362 (fun a : J => ∑ i : Fin (m + 1),363 (coeff a i * replacementParity i) •364 Pi.single (replacementMinorIndex i a) 1)365 (maximalMinors (clmMatrix (configurationFinMap C)))366 _ = ∑ a : J, ∑ i : Fin (m + 1), dotProduct367 ((coeff a i * replacementParity i) •368 Pi.single (replacementMinorIndex i a) 1)369 (maximalMinors (clmMatrix (configurationFinMap C))) := by370 apply Finset.sum_congr rfl371 intro a _ha372 exact pair_sum_left_Fin373 (fun i : Fin (m + 1) =>374 (coeff a i * replacementParity i) •375 Pi.single (replacementMinorIndex i a) 1)376 (maximalMinors (clmMatrix (configurationFinMap C)))377 _ = ∑ a : J, ∑ i : Fin (m + 1),378 coeff a i * replacementDet C.1 i (C.2 a) := by379 apply Finset.sum_congr rfl380 intro a _ha381 apply Finset.sum_congr rfl382 intro i _hi383 rw [smul_dotProduct, single_dotProduct, one_mul]384 change coeff a i * replacementParity i *385 maximalMinor (clmMatrix (configurationFinMap C))386 (replacementMinorIndex i a) =387 coeff a i * replacementDet C.1 i (C.2 a)388 rw [mul_assoc, replacementParity_mul_maximalMinor C i a]389390theorem pluckerFunctional_normalized_configurationFinMap391 (M : NormModel (m + 1)) (weight : ℝ)392 (coeff : J → Coord (m + 1))393 (C : SatelliteConfiguration (m + 1) J) :394 pluckerFunctional (satellitePluckerCoefficients weight coeff)395 (normalizedPlucker M (configurationFinMap C)) =396 M.closedUnitBallVolume * configurationPolynomial weight coeff C := by397 rw [pluckerFunctional_apply, MathlibAnnex.Matrix.pairing_ballVolumeScaledMaximalMinors,398 pluckerPairing_satelliteCoefficients_maximalMinors]399400private def Internal.supportOrientation (t : ℝ) : ℝ := if 0 ≤ t then 1 else -1401402@[simp] private theorem Internal.supportOrientation_mem (t : ℝ) :403 supportOrientation t = 1 ∨ supportOrientation t = -1 := by404 by_cases ht : 0 ≤ t405 · exact Or.inl (by simp [supportOrientation, ht])406 · exact Or.inr (by simp [supportOrientation, ht])407408private theorem Internal.supportOrientation_mul (t : ℝ) :409 supportOrientation t * t = |t| := by410 by_cases ht : 0 ≤ t411 · simp [supportOrientation, ht, abs_of_nonneg ht]412 · have ht' : t ≤ 0 := le_of_not_ge ht413 simp [supportOrientation, ht, abs_of_nonpos ht']414415noncomputable def orientedSatelliteSupport416 (weight : ℝ) (coeff : J → Coord (m + 1))417 (Cstar : SatelliteConfiguration (m + 1) J) :418 PluckerCoord (m + 1) (positiveSatelliteAmbientDim m J) →L[ℝ] ℝ :=419 supportOrientation (configurationPolynomial weight coeff Cstar) •420 pluckerFunctional (satellitePluckerCoefficients weight coeff)421422theorem orientedSatelliteSupport_configuration423 (M : NormModel (m + 1)) (weight : ℝ)424 (coeff : J → Coord (m + 1))425 (Cstar C : SatelliteConfiguration (m + 1) J) :426 orientedSatelliteSupport weight coeff Cstar427 (normalizedPlucker M (configurationFinMap C)) =428 M.closedUnitBallVolume *429 (supportOrientation (configurationPolynomial weight coeff Cstar) *430 configurationPolynomial weight coeff C) := by431 change supportOrientation (configurationPolynomial weight coeff Cstar) *432 pluckerFunctional (satellitePluckerCoefficients weight coeff)433 (normalizedPlucker M (configurationFinMap C)) =434 M.closedUnitBallVolume *435 (supportOrientation (configurationPolynomial weight coeff Cstar) *436 configurationPolynomial weight coeff C)437 rw [pluckerFunctional_normalized_configurationFinMap]438 ring439440theorem orientedSatelliteSupport_self441 (M : NormModel (m + 1)) (weight : ℝ)442 (coeff : J → Coord (m + 1))443 (Cstar : SatelliteConfiguration (m + 1) J) :444 orientedSatelliteSupport weight coeff Cstar445 (normalizedPlucker M (configurationFinMap Cstar)) =446 M.closedUnitBallVolume * |configurationPolynomial weight coeff Cstar| := by447 rw [orientedSatelliteSupport_configuration, supportOrientation_mul]448449end MathlibAnnex.PluckerSupport