Exact source: MathlibAnnex/Analysis/Normed/Operator/FiniteRecovery.lean
Pinned GitHub source · Raw UTF-8 source
Back to Equal Plücker bodies yield matching generators with an almost-isometric representative · Back to The chosen support slice consists of almost-isometric generators
1import MathlibAnnex.Analysis.Normed.Operator.PluckerSupport2import MathlibAnnex.Analysis.Convex.PluckerBody3import MathlibAnnex.Analysis.Convex.LexicographicSelection45noncomputable section6set_option autoImplicit false7open Set Module8open scoped BigOperators NNReal9namespace MathlibAnnex.FiniteRecovery10universe u11open Satellite12private abbrev Coord (n : ℕ) := Fin n → ℝ13private abbrev NormModel (n : ℕ) := EquivalentSeminorm (Coord n)14private abbrev DualFrame (n : ℕ) := DeterminantFrame.Frame n (Coord n)15private abbrev dualFrameMatrix {n : ℕ} := DeterminantFrame.frameMatrix (Pi.basisFun ℝ (Fin n))16private abbrev frameDet {n : ℕ} := DeterminantFrame.frameDeterminant (Pi.basisFun ℝ (Fin n))17private abbrev replacementDet {n : ℕ} := DeterminantFrame.replacementDeterminant (Pi.basisFun ℝ (Fin n))18private abbrev frameCoordinates {n : ℕ} := @DeterminantFrame.frameCoordinates n (Coord n) _ _19private abbrev framePreimage {n : ℕ} (B : DualFrame n) (c : Coord n) := (dualFrameMatrix B)⁻¹.mulVec c20private abbrev IsDualContraction {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) := ∀ x, |r x| ≤ M.p x21private abbrev dualRowSet {n : ℕ} (M : NormModel n) := {r : Coord n →L[ℝ] ℝ | IsDualContraction M r}22private abbrev dualFrameSet {n : ℕ} (M : NormModel n) := {B : DualFrame n | ∀ i, IsDualContraction M (B i)}2324private instance modelFiniteDimensional {n : ℕ} (M : NormModel n) : FiniteDimensional ℝ (EquivalentSeminorm.Space M) :=25 inferInstanceAs (FiniteDimensional ℝ (Coord n))2627private def modelBasis {n : ℕ} (M : NormModel n) : Basis (Fin n) ℝ (EquivalentSeminorm.Space M) :=28 Pi.basisFun ℝ (Fin n)2930private def toModelRow {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :31 EquivalentSeminorm.Space M →L[ℝ] ℝ :=32 LinearMap.toContinuousLinearMap (show EquivalentSeminorm.Space M →ₗ[ℝ] ℝ from r.toLinearMap)3334private def fromModelRow {n : ℕ} (M : NormModel n) (r : EquivalentSeminorm.Space M →L[ℝ] ℝ) :35 Coord n →L[ℝ] ℝ :=36 LinearMap.toContinuousLinearMap (show Coord n →ₗ[ℝ] ℝ from r.toLinearMap)3738private theorem toModelRow_mem_iff {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :39 toModelRow M r ∈ DeterminantFrame.unitRowSet (EquivalentSeminorm.Space M) ↔ IsDualContraction M r := by40 rw [DeterminantFrame.mem_unitRowSet]41 constructor42 · intro h x43 have := (toModelRow M r).le_opNorm (show EquivalentSeminorm.Space M from x)44 change |r x| ≤ ‖toModelRow M r‖ * M.p x at this45 exact this.trans (by nlinarith [apply_nonneg M.p x])46 · intro h47 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one48 intro x49 change |r (show Coord n from x)| ≤ 1 * M.p (show Coord n from x)50 simpa only [one_mul] using h (show Coord n from x)5152private abbrev detMax {n : ℕ} (M : NormModel n) := DeterminantFrame.determinantMaximum (modelBasis M)53private abbrev NearMaxInverseBound {n : ℕ} (M : NormModel n) := DeterminantFrame.NearMaxInverseBound (modelBasis M)54private abbrev nearMaxFrames {n : ℕ} (M : NormModel n) (η : ℝ) := {B : DualFrame n | B ∈ dualFrameSet M ∧ detMax M - η ≤ |frameDet B|}5556private theorem toModelFrame_mem {n : ℕ} (M : NormModel n) {B : DualFrame n} (h : B ∈ dualFrameSet M) :57 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.unitFrameSet n (EquivalentSeminorm.Space M) := by58 intro i59 exact (toModelRow_mem_iff M (B i)).mpr (h i)6061private theorem toModelFrame_near {n : ℕ} (M : NormModel n) {η : ℝ} {B : DualFrame n} (h : B ∈ nearMaxFrames M η) :62 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.nearMaxFrames (modelBasis M) η :=63 ⟨toModelFrame_mem M h.1, h.2⟩6465private theorem seminorm_framePreimage_le {n : ℕ} (M : NormModel n) {η : ℝ} (H : NearMaxInverseBound M η) {B : DualFrame n}66 (h : B ∈ nearMaxFrames M η) (c : Coord n) : M.p (framePreimage B c) ≤ H.boundConstant * ‖c‖ := by67 exact H.bound (toModelFrame_near M h) c6869private theorem detMax_pos {n : ℕ} (M : NormModel n) : 0 < detMax M :=70 DeterminantFrame.determinantMaximum_pos (modelBasis M)7172private theorem nearMaxFrame_det_ne_zero {n : ℕ} (M : NormModel n) {η : ℝ}73 (hη : η < detMax M) {B : DualFrame n} (hB : B ∈ nearMaxFrames M η) : frameDet B ≠ 0 :=74 DeterminantFrame.nearMaxFrame_det_ne_zero (modelBasis M) hη (toModelFrame_near M hB)7576private theorem inverse_mulVec_frameCoordinates {n : ℕ} (M : NormModel n) {η : ℝ}77 (hη : η < detMax M) {B : DualFrame n} (hB : B ∈ nearMaxFrames M η) (x : Coord n) :78 framePreimage B (frameCoordinates B x) = x := by79 exact DeterminantFrame.inverse_mulVec_frameCoordinates (modelBasis M) hη (toModelFrame_near M hB) (show EquivalentSeminorm.Space M from x)8081private theorem abs_replacementDet_le_detMax {n : ℕ} (M : NormModel n) {B : DualFrame n} (hB : B ∈ dualFrameSet M)82 (i : Fin n) {r : Coord n →L[ℝ] ℝ} (hr : IsDualContraction M r) : |replacementDet B i r| ≤ detMax M := by83 have h := DeterminantFrame.abs_replacementDeterminant_le_maximum (modelBasis M) (toModelFrame_mem M hB) i ((toModelRow_mem_iff M r).mpr hr)84 have heq : (fun j => toModelRow M ((DeterminantFrame.replaceRow B i r) j)) =85 DeterminantFrame.replaceRow (fun j => toModelRow M (B j)) i (toModelRow M r) := by86 funext j87 by_cases hj : j = i <;> simp [DeterminantFrame.replaceRow, hj]88 change |DeterminantFrame.frameDeterminant (modelBasis M)89 (fun j => toModelRow M ((DeterminantFrame.replaceRow B i r) j))| ≤ detMax M90 rw [heq]91 exact h9293private def maxFrame {n : ℕ} (M : NormModel n) : DualFrame n :=94 fun i => fromModelRow M (DeterminantFrame.maximizingFrame (modelBasis M) i)9596private theorem maxFrame_det {n : ℕ} (M : NormModel n) : |frameDet (maxFrame M)| = detMax M := rfl9798private theorem maxFrame_mem {n : ℕ} (M : NormModel n) : maxFrame M ∈ dualFrameSet M := by99 intro i100 apply (toModelRow_mem_iff M _).mp101 have h := DeterminantFrame.maximizingFrame_mem (modelBasis M) i102 convert h using 1103 ext x104 rfl105106107private abbrev replaceFrameRow {n : ℕ} := @DeterminantFrame.replaceRow n (Coord n) _ _108private abbrev functionalRow {n : ℕ} := DeterminantFrame.functionalCoordinates (Pi.basisFun ℝ (Fin n))109private theorem continuous_frameDet {n : ℕ} : Continuous (frameDet : DualFrame n → ℝ) :=110 DeterminantFrame.continuous_frameDeterminant (Pi.basisFun ℝ (Fin n))111private theorem dualFrameMatrix_replaceFrameRow {n : ℕ} (B : DualFrame n) (i : Fin n) (r : Coord n →L[ℝ] ℝ) :112 dualFrameMatrix (replaceFrameRow B i r) = (dualFrameMatrix B).updateRow i (functionalRow r) :=113 DeterminantFrame.frameMatrix_replaceRow (Pi.basisFun ℝ (Fin n)) B i r114private theorem sum_mul_replacementDet {n : ℕ} (B : DualFrame n) (hB : frameDet B ≠ 0) (r : Coord n →L[ℝ] ℝ) (c : Coord n) :115 (∑ i : Fin n, c i * replacementDet B i r) = frameDet B * r (framePreimage B c) :=116 DeterminantFrame.sum_mul_replacementDeterminant (Pi.basisFun ℝ (Fin n)) B hB r c117118private theorem isCompact_dualRowSet {n : ℕ} (M : NormModel n) : IsCompact (dualRowSet M) := by119 have hc : IsClosed (dualRowSet M) := by120 have heq : dualRowSet M = (⋂ x : Coord n, {r : Coord n →L[ℝ] ℝ | |r x| ≤ M.p x}) := by ext r; simp [dualRowSet, IsDualContraction]121 rw [heq]122 exact isClosed_iInter fun x => isClosed_le (by fun_prop) continuous_const123 have hb : Bornology.IsBounded (dualRowSet M) := by124 apply (Metric.isBounded_iff_subset_closedBall (0 : Coord n →L[ℝ] ℝ)).2125 refine ⟨M.upper, ?_⟩126 intro r hr127 rw [Metric.mem_closedBall, dist_zero_right]128 apply ContinuousLinearMap.opNorm_le_bound _ M.upper_pos.le129 intro x130 exact (hr x).trans (M.le_upper x)131 exact Metric.isCompact_of_isClosed_isBounded hc hb132133private theorem isCompact_dualFrameSet {n : ℕ} (M : NormModel n) : IsCompact (dualFrameSet M) := by134 have heq : dualFrameSet M = Set.univ.pi (fun _ : Fin n => dualRowSet M) := by ext B; simp [dualFrameSet, dualRowSet]135 rw [heq]136 exact isCompact_univ_pi fun _ => isCompact_dualRowSet M137138139private abbrev SupCoord (n : ℕ) := Fin n → ℝ140141variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}142private noncomputable instance centerFintype (C : FiniteCoefficientNet (n := n) K ρ) :143 Fintype C.centers :=144 C.finite_centers.fintype145146147148variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}149private def centerValue (C : FiniteCoefficientNet (n := n) K ρ) (c : C.centers) :150 Coord n := c.1151152private def satelliteRadius (ε K : ℝ) : ℝ := min ε 1 / (8 * K)153154private theorem satelliteRadius_pos {ε K : ℝ} (hε : 0 < ε) (hK : 0 < K) :155 0 < satelliteRadius ε K := by156 exact div_pos (lt_min hε zero_lt_one) (mul_pos (by norm_num) hK)157158private theorem two_mul_bound_mul_satelliteRadius_lt_half {ε K : ℝ}159 (hε : 0 < ε) (hK : 0 < K) :160 2 * K * satelliteRadius ε K < ε / 2 := by161 have hden : 0 < 8 * K := mul_pos (by norm_num) hK162 have hmin : min ε 1 ≤ ε := min_le_left _ _163 unfold satelliteRadius164 calc165 2 * K * (min ε 1 / (8 * K)) = min ε 1 / 4 := by field_simp; ring166 _ ≤ ε / 4 := by linarith167 _ < ε / 2 := by linarith168169private theorem satelliteRadius_lt_half_inv {ε K : ℝ}170 (_hε : 0 < ε) (hK : 0 < K) :171 satelliteRadius ε K < 1 / (2 * K) := by172 have hmin : min ε 1 ≤ 1 := min_le_right _ _173 unfold satelliteRadius174 have hK2 : 0 < 2 * K := mul_pos (by norm_num) hK175 have hK8 : 0 < 8 * K := mul_pos (by norm_num) hK176 calc177 min ε 1 / (8 * K) ≤ 1 / (8 * K) :=178 div_le_div_of_nonneg_right hmin hK8.le179 _ < 1 / (2 * K) := by180 apply one_div_lt_one_div_of_lt hK2181 nlinarith182183private noncomputable def satelliteRadiusNNReal (ε K : ℝ) (hε : 0 < ε) (hK : 0 < K) :184 ℝ≥0 :=185 ⟨satelliteRadius ε K, (satelliteRadius_pos hε hK).le⟩186187@[simp] private theorem coe_satelliteRadiusNNReal (ε K : ℝ) (hε : 0 < ε) (hK : 0 < K) :188 (satelliteRadiusNNReal ε K hε hK : ℝ) = satelliteRadius ε K := rfl189190private theorem satelliteRadiusNNReal_ne_zero {ε K : ℝ} (hε : 0 < ε) (hK : 0 < K) :191 satelliteRadiusNNReal ε K hε hK ≠ 0 := by192 exact ne_of_gt (by193 change 0 < satelliteRadius ε K194 exact satelliteRadius_pos hε hK)195196private theorem isCompact_satelliteRowsSet {n : ℕ} (M : NormModel n)197 (J : Type u) [Fintype J] :198 IsCompact (satelliteRowsSet M J) := by199 have heq : satelliteRowsSet M J =200 Set.univ.pi (fun _ : J => dualRowSet M) := by201 ext sat202 simp [satelliteRowsSet, dualRowSet]203 rw [heq]204 exact isCompact_univ_pi fun _ => isCompact_dualRowSet M205206private theorem isCompact_satelliteConfigurationSet {n : ℕ} (M : NormModel n)207 (J : Type u) [Fintype J] :208 IsCompact (satelliteConfigurationSet M J) := by209 exact (isCompact_dualFrameSet M).prod (isCompact_satelliteRowsSet M J)210211private theorem satelliteConfigurationSet_nonempty {n : ℕ} (M : NormModel n)212 (J : Type u) :213 (satelliteConfigurationSet M J).Nonempty := by214 refine ⟨((fun _ => 0), fun _ => 0), ?_⟩215 constructor216 · intro i x217 simpa only [zero_apply, abs_zero] using (apply_nonneg M.p x)218 · intro a x219 simpa only [zero_apply, abs_zero] using (apply_nonneg M.p x)220221private theorem continuous_configurationPolynomial {n : ℕ} {J : Type u} [Fintype J]222 (weight : ℝ) (coeff : J → Coord n) :223 Continuous (configurationPolynomial weight coeff) := by224 change Continuous fun C : SatelliteConfiguration n J =>225 weight * frameDet C.1 +226 ∑ a : J, ∑ i : Fin n,227 coeff a i * replacementDet C.1 i (C.2 a)228 have hreplacement : ∀ (a : J) (i : Fin n),229 Continuous fun C : SatelliteConfiguration n J =>230 replacementDet C.1 i (C.2 a) := by231 intro a i232 unfold replacementDet DeterminantFrame.replacementDeterminant DeterminantFrame.frameDeterminant233 apply Continuous.matrix_det234 apply continuous_matrix235 intro k j236 simp only [DeterminantFrame.frameMatrix, Pi.basisFun_apply]237 change Continuous fun C : SatelliteConfiguration n J =>238 (replaceFrameRow C.1 i (C.2 a)) k (Pi.single j 1)239 by_cases hki : k = i240 · subst k241 simpa [replaceFrameRow, DeterminantFrame.replaceRow] using242 (show Continuous fun C : SatelliteConfiguration n J =>243 C.2 a (Pi.single j 1) by fun_prop)244 · simpa [replaceFrameRow, DeterminantFrame.replaceRow, hki] using245 (show Continuous fun C : SatelliteConfiguration n J =>246 C.1 k (Pi.single j 1) by fun_prop)247 apply Continuous.add248 · exact continuous_const.mul (continuous_frameDet.comp continuous_fst)249 · exact continuous_finsetSum Finset.univ fun a _ =>250 continuous_finsetSum Finset.univ fun i _ =>251 continuous_const.mul (hreplacement a i)252253private theorem exists_maxSatelliteConfiguration {n : ℕ} (M : NormModel n)254 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n) :255 ∃ C ∈ satelliteConfigurationSet M J,256 ∀ D ∈ satelliteConfigurationSet M J,257 |configurationPolynomial weight coeff D| ≤258 |configurationPolynomial weight coeff C| := by259 rcases (isCompact_satelliteConfigurationSet M J).exists_isMaxOn260 (satelliteConfigurationSet_nonempty M J)261 (continuous_configurationPolynomial weight coeff).abs.continuousOn with262 ⟨C, hC, hmax⟩263 exact ⟨C, hC, hmax⟩264265private theorem maxSatelliteConfiguration_mem {n : ℕ} (M : NormModel n)266 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n) :267 maxSatelliteConfiguration M J weight coeff ∈268 satelliteConfigurationSet M J :=269 (Classical.choose_spec270 (exists_maxSatelliteConfiguration M J weight coeff)).1271272private theorem abs_configurationPolynomial_le_max {n : ℕ} (M : NormModel n)273 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n)274 {C : SatelliteConfiguration n J}275 (hC : C ∈ satelliteConfigurationSet M J) :276 |configurationPolynomial weight coeff C| ≤277 |configurationPolynomial weight coeff278 (maxSatelliteConfiguration M J weight coeff)| :=279 (Classical.choose_spec280 (exists_maxSatelliteConfiguration M J weight coeff)).2 C hC281282private theorem maxNetSatelliteConfiguration_satellites_one_sub_epsilon283 {n : ℕ} (M : NormModel n) {η ε weight : ℝ}284 (hη0 : 0 ≤ η) (hηD : η < detMax M) (hε : 0 < ε)285 (H : NearMaxInverseBound M η)286 (C : FiniteCoefficientNet (n := n) H.boundConstant287 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))288 (hweight : 0 < weight)289 (hgap : satelliteBudget M (centerValue C) < weight * η)290 {x : Coord n} (hx : M.p x = 1) :291 ∃ a : C.centers,292 1 - ε <293 |(maxSatelliteConfiguration M C.centers weight (centerValue C)).2 a x| := by294 let Q := maxSatelliteConfiguration M C.centers weight (centerValue C)295 have hQ : Q ∈ satelliteConfigurationSet M C.centers := by296 exact maxSatelliteConfiguration_mem M C.centers weight (centerValue C)297 have hmax : ∀ D ∈ satelliteConfigurationSet M C.centers,298 |configurationPolynomial weight (centerValue C) D| ≤299 |configurationPolynomial weight (centerValue C) Q| := by300 intro D hD301 simpa [Q] using abs_configurationPolynomial_le_max302 M C.centers weight (centerValue C) hD303 simpa [Q] using finiteNet_absoluteMaximizer_satellites_one_sub_epsilon304 M hη0 hηD hε H C hweight hgap hQ hmax hx305306open FiniteSup FiniteSup.Bridge PluckerSupport307namespace Internal308end Internal309open Internal310311private abbrev PluckerCoord (n N : ℕ) := MathlibAnnex.Matrix.MaximalMinorIndex n (Fin N) → ℝ312private abbrev positiveSatelliteAmbientDim (m : ℕ) (J : Type u) [Fintype J] := (m + 1) + Fintype.card J313private abbrev CompactRawSet := TopologicalSpace.NonemptyCompacts314private def supportOrientation (t : ℝ) : ℝ := if 0 ≤ t then 1 else -1315private theorem supportOrientation_mem (t : ℝ) : supportOrientation t = 1 ∨ supportOrientation t = -1 := by316 by_cases ht : 0 ≤ t317 · exact Or.inl (by simp [supportOrientation, ht])318 · exact Or.inr (by simp [supportOrientation, ht])319320private noncomputable def Internal.rawPluckerCompact {n N : ℕ} (M : NormModel n) :321 CompactRawSet (PluckerCoord n N) where322 carrier := MathlibAnnex.PluckerBody.generators M N323 isCompact' := MathlibAnnex.PluckerBody.isCompact_generators M324 nonempty' := MathlibAnnex.PluckerBody.generators_nonempty M325326def PluckerGeneratorGood {n N : ℕ} (M : NormModel n) (ε : ℝ)327 (z : PluckerCoord n N) : Prop :=328 ∃ A : Coord n →L[ℝ] SupCoord N,329 M.IsContraction A ∧330 FinMapAlmostIsometric M ε A ∧331 (z = MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A ∨ z = - MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A)332333private theorem sign_mul_le_abs {s t : ℝ} (hs : s = 1 ∨ s = -1) :334 s * t ≤ |t| := by335 rcases hs with rfl | rfl336 · simpa using le_abs_self t337 · simpa using neg_le_abs t338339private theorem Internal.abs_eq_of_oriented_signed_scaled_eq340 {v s τ p q : ℝ} (hv : 0 < v)341 (hs : s = 1 ∨ s = -1) (hτ : τ = 1 ∨ τ = -1)342 (h : v * (τ * (s * p)) = v * |q|) :343 |p| = |q| := by344 have hscalar : τ * (s * p) = |q| := by345 nlinarith346 have habs := congrArg abs hscalar347 rcases hs with rfl | rfl <;> rcases hτ with rfl | rfl <;>348 simpa using habs349350private theorem Internal.selectedNormalizedPlucker_mem_raw351 {m : ℕ} {J : Type u} [Fintype J]352 (M : NormModel (m + 1)) (weight : ℝ)353 (coeff : J → Coord (m + 1)) :354 MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M355 (configurationFinMap356 (maxSatelliteConfiguration M J weight coeff)) ∈357 MathlibAnnex.PluckerBody.generators M (positiveSatelliteAmbientDim m J) := by358 have hC := maxSatelliteConfiguration_mem M J weight coeff359 exact ⟨configurationFinMap (maxSatelliteConfiguration M J weight coeff),360 (configuration_contraction_iff M _).2 hC, Or.inl rfl⟩361362theorem exists_contraction_maximizing_abs_configurationPolynomial_of_mem_maxSlice363 {m : ℕ} {J : Type u} [Fintype J]364 (M : NormModel (m + 1)) (weight : ℝ)365 (coeff : J → Coord (m + 1))366 {z : PluckerCoord (m + 1) (positiveSatelliteAmbientDim m J)}367 (hz : z ∈ MathlibAnnex.NonemptyCompacts.maxSlice (rawPluckerCompact368 (N := positiveSatelliteAmbientDim m J) M)369 (orientedSatelliteSupport weight coeff370 (maxSatelliteConfiguration M J weight coeff))) :371 ∃ A : Coord (m + 1) →L[ℝ]372 SupCoord (positiveSatelliteAmbientDim m J),373 M.IsContraction A ∧374 (z = MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A ∨ z = - MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A) ∧375 let C := finMapConfiguration A376 C ∈ satelliteConfigurationSet M J ∧377 ∀ D ∈ satelliteConfigurationSet M J,378 |configurationPolynomial weight coeff D| ≤379 |configurationPolynomial weight coeff C| := by380 classical381 let Cstar : SatelliteConfiguration (m + 1) J :=382 maxSatelliteConfiguration M J weight coeff383 let R := rawPluckerCompact (N := positiveSatelliteAmbientDim m J) M384 let ℓ := orientedSatelliteSupport weight coeff Cstar385 have hCstar : Cstar ∈ satelliteConfigurationSet M J := by386 simpa [Cstar] using maxSatelliteConfiguration_mem M J weight coeff387 have hstarMax : ∀ D ∈ satelliteConfigurationSet M J,388 |configurationPolynomial weight coeff D| ≤389 |configurationPolynomial weight coeff Cstar| := by390 intro D hD391 simpa [Cstar] using abs_configurationPolynomial_le_max M J weight coeff hD392 have hstarRaw : MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M (configurationFinMap Cstar) ∈ (R : Set _) := by393 change MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M (configurationFinMap Cstar) ∈394 MathlibAnnex.PluckerBody.generators M (positiveSatelliteAmbientDim m J)395 simpa [Cstar] using selectedNormalizedPlucker_mem_raw M weight coeff396 have hstarLeZ :397 ℓ (MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M (configurationFinMap Cstar)) ≤ ℓ z := by398 calc399 ℓ (MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M (configurationFinMap Cstar))400 ≤ MathlibAnnex.NonemptyCompacts.maxValue R ℓ := MathlibAnnex.NonemptyCompacts.le_maximizer R ℓ hstarRaw401 _ = ℓ z := hz.2.symm402 rcases hz.1 with ⟨A, hA, hzPos | hzNeg⟩403 · let C : SatelliteConfiguration (m + 1) J := finMapConfiguration A404 have hC : C ∈ satelliteConfigurationSet M J :=405 finMapConfiguration_mem M hA406 have hAC : configurationFinMap C = A := by407 dsimp [C]408 exact configurationFinMap_finMapConfiguration A409 have hs := supportOrientation_mem410 (configurationPolynomial weight coeff Cstar)411 have hupper : ℓ z ≤412 M.closedUnitBallVolume * |configurationPolynomial weight coeff Cstar| := by413 rw [hzPos, ← hAC]414 rw [orientedSatelliteSupport_configuration]415 apply mul_le_mul_of_nonneg_left _ (le_of_lt M.closedUnitBallVolume_pos)416 exact (sign_mul_le_abs hs).trans (hstarMax C hC)417 have heq : ℓ z =418 M.closedUnitBallVolume * |configurationPolynomial weight coeff Cstar| := by419 apply le_antisymm hupper420 simpa [ℓ, Cstar, orientedSatelliteSupport_self] using hstarLeZ421 have hsupport :422 M.closedUnitBallVolume *423 (1 * (supportOrientation424 (configurationPolynomial weight coeff Cstar) *425 configurationPolynomial weight coeff C)) =426 M.closedUnitBallVolume * |configurationPolynomial weight coeff Cstar| := by427 calc428 M.closedUnitBallVolume *429 (1 * (supportOrientation430 (configurationPolynomial weight coeff Cstar) *431 configurationPolynomial weight coeff C)) =432 M.closedUnitBallVolume *433 (supportOrientation434 (configurationPolynomial weight coeff Cstar) *435 configurationPolynomial weight coeff C) := by ring436 _ = ℓ (MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M (configurationFinMap C)) :=437 (orientedSatelliteSupport_configuration438 M weight coeff Cstar C).symm439 _ = ℓ (MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A) := by rw [hAC]440 _ = ℓ z := by rw [hzPos]441 _ = M.closedUnitBallVolume *442 |configurationPolynomial weight coeff Cstar| := heq443 have habs : |configurationPolynomial weight coeff C| =444 |configurationPolynomial weight coeff Cstar| :=445 abs_eq_of_oriented_signed_scaled_eq M.closedUnitBallVolume_pos hs (Or.inl rfl)446 hsupport447 refine ⟨A, hA, Or.inl hzPos, hC, ?_⟩448 intro D hD449 exact (hstarMax D hD).trans_eq habs.symm450 · let C : SatelliteConfiguration (m + 1) J := finMapConfiguration A451 have hC : C ∈ satelliteConfigurationSet M J :=452 finMapConfiguration_mem M hA453 have hAC : configurationFinMap C = A := by454 dsimp [C]455 exact configurationFinMap_finMapConfiguration A456 have hs := supportOrientation_mem457 (configurationPolynomial weight coeff Cstar)458 have hminusSign :459 - supportOrientation (configurationPolynomial weight coeff Cstar) = 1 ∨460 - supportOrientation (configurationPolynomial weight coeff Cstar) = -1 := by461 rcases hs with h | h <;> simp [h]462 have hupper : ℓ z ≤463 M.closedUnitBallVolume * |configurationPolynomial weight coeff Cstar| := by464 calc465 ℓ z = ℓ (- MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A) := by rw [hzNeg]466 _ = -ℓ (MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A) := by simp467 _ = -ℓ (MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M (configurationFinMap C)) := by rw [hAC]468 _ = -(M.closedUnitBallVolume *469 (supportOrientation470 (configurationPolynomial weight coeff Cstar) *471 configurationPolynomial weight coeff C)) := by472 rw [orientedSatelliteSupport_configuration]473 rfl474 _ = M.closedUnitBallVolume *475 ((-supportOrientation476 (configurationPolynomial weight coeff Cstar)) *477 configurationPolynomial weight coeff C) := by ring478 _ ≤ M.closedUnitBallVolume *479 |configurationPolynomial weight coeff Cstar| := by480 apply mul_le_mul_of_nonneg_left _ (le_of_lt M.closedUnitBallVolume_pos)481 exact (sign_mul_le_abs hminusSign).trans (hstarMax C hC)482 have heq : ℓ z =483 M.closedUnitBallVolume * |configurationPolynomial weight coeff Cstar| := by484 apply le_antisymm hupper485 simpa [ℓ, Cstar, orientedSatelliteSupport_self] using hstarLeZ486 have hsupport :487 M.closedUnitBallVolume *488 ((-1) * (supportOrientation489 (configurationPolynomial weight coeff Cstar) *490 configurationPolynomial weight coeff C)) =491 M.closedUnitBallVolume * |configurationPolynomial weight coeff Cstar| := by492 calc493 M.closedUnitBallVolume *494 ((-1) * (supportOrientation495 (configurationPolynomial weight coeff Cstar) *496 configurationPolynomial weight coeff C)) =497 -(M.closedUnitBallVolume *498 (supportOrientation499 (configurationPolynomial weight coeff Cstar) *500 configurationPolynomial weight coeff C)) := by ring501 _ = -ℓ (MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M (configurationFinMap C)) := by502 rw [orientedSatelliteSupport_configuration]503 rfl504 _ = -ℓ (MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A) := by rw [hAC]505 _ = ℓ (- MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A) := by simp506 _ = ℓ z := by rw [hzNeg]507 _ = M.closedUnitBallVolume *508 |configurationPolynomial weight coeff Cstar| := heq509 have habs : |configurationPolynomial weight coeff C| =510 |configurationPolynomial weight coeff Cstar| :=511 abs_eq_of_oriented_signed_scaled_eq M.closedUnitBallVolume_pos hs (Or.inr rfl)512 hsupport513 refine ⟨A, hA, Or.inr hzNeg, hC, ?_⟩514 intro D hD515 exact (hstarMax D hD).trans_eq habs.symm516517theorem targetRawSupportMaximizer_good518 {m : ℕ} (M : NormModel (m + 1)) {η ε weight : ℝ}519 (hη0 : 0 ≤ η) (hηD : η < detMax M) (hε : 0 < ε)520 (H : NearMaxInverseBound M η)521 (Cnet : FiniteCoefficientNet (n := m + 1) H.boundConstant522 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))523 (hweight : 0 < weight)524 (hgap : satelliteBudget M (centerValue Cnet) < weight * η)525 {z : PluckerCoord (m + 1)526 (positiveSatelliteAmbientDim m Cnet.centers)}527 (hz : z ∈ MathlibAnnex.NonemptyCompacts.maxSlice (rawPluckerCompact528 (N := positiveSatelliteAmbientDim m Cnet.centers) M)529 (orientedSatelliteSupport weight (centerValue Cnet)530 (maxSatelliteConfiguration M Cnet.centers531 weight (centerValue Cnet)))) :532 PluckerGeneratorGood M ε z := by533 classical534 rcases exists_contraction_maximizing_abs_configurationPolynomial_of_mem_maxSlice535 M weight (centerValue Cnet) hz with536 ⟨A, hA, hzA, hC, hmax⟩537 let C : SatelliteConfiguration (m + 1) Cnet.centers :=538 finMapConfiguration A539 have hAC : configurationFinMap C = A := by540 dsimp [C]541 exact configurationFinMap_finMapConfiguration A542 refine ⟨A, hA, ?_, hzA⟩543 intro x hx544 rcases finiteNet_absoluteMaximizer_satellites_one_sub_epsilon545 M hη0 hηD hε H Cnet hweight hgap hC hmax hx with ⟨a, ha⟩546 have hcoord : |C.2 a x| ≤ ‖configurationFinMap C x‖ := by547 have := norm_le_pi_norm (configurationFinMap C x)548 (Fin.natAdd (m + 1) (Fintype.equivFin Cnet.centers a))549 simpa [configurationFinMap_apply_satellite, Real.norm_eq_abs] using this550 rw [hAC] at hcoord551 exact ha.trans_le hcoord552553private theorem exists_commonGoodRaw554 {m : ℕ} (MX MY : NormModel (m + 1)) {η ε weight : ℝ}555 (hη0 : 0 ≤ η) (hηD : η < detMax MY) (hε : 0 < ε)556 (H : NearMaxInverseBound MY η)557 (Cnet : FiniteCoefficientNet (n := m + 1) H.boundConstant558 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))559 (hweight : 0 < weight)560 (hgap : satelliteBudget MY (centerValue Cnet) < weight * η)561 (hHull :562 MathlibAnnex.PluckerBody.body MX (positiveSatelliteAmbientDim m Cnet.centers) =563 MathlibAnnex.PluckerBody.body MY (positiveSatelliteAmbientDim m Cnet.centers)) :564 ∃ z : PluckerCoord (m + 1)565 (positiveSatelliteAmbientDim m Cnet.centers),566 z ∈ MathlibAnnex.PluckerBody.generators MX567 (positiveSatelliteAmbientDim m Cnet.centers) ∧568 z ∈ MathlibAnnex.PluckerBody.generators MY569 (positiveSatelliteAmbientDim m Cnet.centers) ∧570 PluckerGeneratorGood MY ε z := by571 classical572 let RX := rawPluckerCompact573 (N := positiveSatelliteAmbientDim m Cnet.centers) MX574 let RY := rawPluckerCompact575 (N := positiveSatelliteAmbientDim m Cnet.centers) MY576 let Cstar : SatelliteConfiguration (m + 1) Cnet.centers :=577 maxSatelliteConfiguration MY Cnet.centers weight (centerValue Cnet)578 let ℓ := orientedSatelliteSupport weight (centerValue Cnet) Cstar579 have hHull' : convexHull ℝ (RX : Set (PluckerCoord (m + 1) (positiveSatelliteAmbientDim m Cnet.centers))) = convexHull ℝ (RY : Set (PluckerCoord (m + 1) (positiveSatelliteAmbientDim m Cnet.centers))) := by580 simpa [RX, RY, rawPluckerCompact, MathlibAnnex.PluckerBody.body] using hHull581 exact MathlibAnnex.exists_common_pi582 RX RY hHull' ℓ (PluckerGeneratorGood MY ε)583 (fun z hz => targetRawSupportMaximizer_good584 MY hη0 hηD hε H Cnet hweight hgap (by simpa [RY, ℓ, Cstar] using hz))585586structure AlmostIsometryMatch {m : ℕ}587 (MX MY : NormModel (m + 1)) (ε : ℝ) where588 ambientDim : ℕ589 z : PluckerCoord (m + 1) ambientDim590 sourceMap : Coord (m + 1) →L[ℝ] SupCoord ambientDim591 targetMap : Coord (m + 1) →L[ℝ] SupCoord ambientDim592 isContraction_sourceMap : MX.IsContraction sourceMap593 isContraction_targetMap : MY.IsContraction targetMap594 finMapAlmostIsometric_targetMap : FinMapAlmostIsometric MY ε targetMap595 eq_ballVolumeScaledMaximalMinors_sourceMap_or_neg :596 z = MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MX sourceMap ∨597 z = - MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MX sourceMap598 eq_ballVolumeScaledMaximalMinors_targetMap_or_neg :599 z = MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MY targetMap ∨600 z = - MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MY targetMap601602theorem nonempty_almostIsometryMatch_at_satelliteDimension603 {m : ℕ} (MX MY : NormModel (m + 1)) {η ε weight : ℝ}604 (hη0 : 0 ≤ η) (hηD : η < detMax MY) (hε : 0 < ε)605 (H : NearMaxInverseBound MY η)606 (Cnet : FiniteCoefficientNet (n := m + 1) H.boundConstant607 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))608 (hweight : 0 < weight)609 (hgap : satelliteBudget MY (centerValue Cnet) < weight * η)610 (hHull :611 MathlibAnnex.PluckerBody.body MX (positiveSatelliteAmbientDim m Cnet.centers) =612 MathlibAnnex.PluckerBody.body MY (positiveSatelliteAmbientDim m Cnet.centers)) :613 Nonempty (AlmostIsometryMatch MX MY ε) := by614 classical615 rcases exists_commonGoodRaw MX MY hη0 hηD hε H Cnet616 hweight hgap hHull with ⟨z, hzX, _hzY, hgood⟩617 rcases hzX with ⟨T, hT, hTsign⟩618 rcases hgood with ⟨A, hA, hAlmost, hAsign⟩619 exact ⟨{620 ambientDim := positiveSatelliteAmbientDim m Cnet.centers621 z := z622 sourceMap := T623 targetMap := A624 isContraction_sourceMap := hT625 isContraction_targetMap := hA626 finMapAlmostIsometric_targetMap := hAlmost627 eq_ballVolumeScaledMaximalMinors_sourceMap_or_neg := hTsign628 eq_ballVolumeScaledMaximalMinors_targetMap_or_neg := hAsign629 }⟩630631theorem nonempty_almostIsometryMatch_of_all_body_eq632 {m : ℕ} (MX MY : NormModel (m + 1)) {ε : ℝ} (hε : 0 < ε)633 (hBodies : ∀ N : ℕ, MathlibAnnex.PluckerBody.body MX N = MathlibAnnex.PluckerBody.body MY N) :634 Nonempty (AlmostIsometryMatch MX MY ε) := by635 let η : ℝ := detMax MY / 2636 have hD : 0 < detMax MY := detMax_pos MY637 have hη : 0 < η := by638 dsimp [η]639 linarith640 have hηD : η < detMax MY := by641 dsimp [η]642 linarith643 rcases exists_goodSatellitePackage MY hη hηD hε with644 ⟨H, Cnet, weight, hweight, hgap, _hselectedGood⟩645 exact nonempty_almostIsometryMatch_at_satelliteDimension646 MX MY hη.le hηD hε H Cnet hweight hgap647 (hBodies (positiveSatelliteAmbientDim m Cnet.centers))648649end MathlibAnnex.FiniteRecovery