Exact source: MathlibAnnex/Analysis/Convex/PluckerBody.lean
Pinned GitHub source · Raw UTF-8 source
Back to The symmetric convex body of contraction minors · Back to Sphere isometries preserve the Plücker body · Back to A target contraction generator lies in the source body
1import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Topology2import MathlibAnnex.LinearAlgebra.Matrix.VolumeScaledMaximalMinor3import MathlibAnnex.Analysis.Convex.CompactHull45/-!6# The symmetric convex body of volume-scaled maximal minors78The generators consist exactly of both signs of every model contraction's9scaled maximal-minor vector. The body is their real convex hull.10-/1112noncomputable section1314namespace MathlibAnnex.PluckerBody1516open Set Matrix1718/-- Both signs of the volume-scaled minors of each model contraction. -/19def generators {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) (N : ℕ) :20 Set (Matrix.MaximalMinorIndex n (Fin N) → ℝ) :=21 {z | ∃ A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ),22 M.IsContraction A ∧23 (z = Matrix.ballVolumeScaledMaximalMinors M A ∨24 z = -Matrix.ballVolumeScaledMaximalMinors M A)}2526/-- The convex hull of all signed model-contraction generators. -/27def body {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) (N : ℕ) :28 Set (Matrix.MaximalMinorIndex n (Fin N) → ℝ) := convexHull ℝ (generators M N)2930theorem generators_nonempty {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :31 (generators M N).Nonempty := by32 exact ⟨Matrix.ballVolumeScaledMaximalMinors M 0, 0, M.isContraction_zero, Or.inl rfl⟩3334theorem generators_neg {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))35 {z : Matrix.MaximalMinorIndex n (Fin N) → ℝ} (hz : z ∈ generators M N) :36 -z ∈ generators M N := by37 rcases hz with ⟨A, hA, hpos | hneg⟩38 · refine ⟨A, hA, Or.inr ?_⟩; simp [hpos]39 · refine ⟨A, hA, Or.inl ?_⟩; simp [hneg]4041theorem body_neg {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))42 {z : Matrix.MaximalMinorIndex n (Fin N) → ℝ} (hz : z ∈ body M N) :43 -z ∈ body M N := by44 change z ∈ convexHull ℝ (generators M N) at hz45 have hsub : generators M N ⊆ -body M N := by46 intro w hw47 exact Set.mem_neg.mpr (subset_convexHull ℝ _ (generators_neg M hw))48 have hzneg : z ∈ -body M N :=49 convexHull_min hsub (convex_convexHull ℝ (generators M N)).neg hz50 exact Set.mem_neg.mp hzneg5152theorem generators_eq_image_union {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :53 generators M N =54 Matrix.ballVolumeScaledMaximalMinors M '' M.contractionSet (Fin N → ℝ) ∪55 (fun z : Matrix.MaximalMinorIndex n (Fin N) → ℝ => -z) ''56 (Matrix.ballVolumeScaledMaximalMinors M '' M.contractionSet (Fin N → ℝ)) := by57 ext z58 constructor59 · rintro ⟨A, hA, rfl | rfl⟩60 · exact Or.inl ⟨A, hA, rfl⟩61 · exact Or.inr ⟨Matrix.ballVolumeScaledMaximalMinors M A, ⟨A, hA, rfl⟩, rfl⟩62 · rintro (⟨A, hA, rfl⟩ | ⟨w, ⟨A, hA, rfl⟩, rfl⟩)63 · exact ⟨A, hA, Or.inl rfl⟩64 · exact ⟨A, hA, Or.inr rfl⟩6566/-- The generator set is compact at every pair of finite dimensions. -/67theorem isCompact_generators {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :68 IsCompact (generators M N) := by69 rw [generators_eq_image_union]70 have hclosed : IsClosed (M.contractionSet (Fin N → ℝ)) := by71 have heq : M.contractionSet (Fin N → ℝ) =72 ⋂ x : Fin n → ℝ, {A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ) | ‖A x‖ ≤ M.p x} := by73 ext A74 simp [EquivalentSeminorm.contractionSet, EquivalentSeminorm.IsContraction]75 rw [heq]76 apply isClosed_iInter77 intro x78 apply isClosed_le _ continuous_const79 fun_prop80 have hbounded : Bornology.IsBounded (M.contractionSet (Fin N → ℝ)) := by81 refine (Metric.isBounded_iff_subset_closedBall (0 : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ))).2 ?_82 refine ⟨M.upper, ?_⟩83 intro A hA84 have hnorm : ‖A‖ ≤ M.upper :=85 ContinuousLinearMap.opNorm_le_bound A M.upper_pos.le (fun x => (hA x).trans (M.le_upper x))86 simpa [Metric.mem_closedBall, dist_eq_norm] using hnorm87 have hC : IsCompact (M.contractionSet (Fin N → ℝ)) :=88 Metric.isCompact_of_isClosed_isBounded hclosed hbounded89 have hpos := hC.image (Matrix.continuous_ballVolumeScaledMaximalMinors M)90 exact hpos.union (hpos.image continuous_neg)9192end MathlibAnnex.PluckerBody