Exact source: MathlibAnnex/Analysis/Normed/Plucker/RecoveryCertificate.lean
Pinned GitHub source · Raw UTF-8 source
Back to A volume-normalized linear contraction obtained by a limit · Back to Almost-contractive linear recovery with exact volume scaling
1import MathlibAnnex.Analysis.Normed.Operator.FiniteRecovery2import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Transport3import MathlibAnnex.LinearAlgebra.Matrix.MaximalMinor4import MathlibAnnex.LinearAlgebra.Matrix.MaximalMinorFactorization5import Mathlib.Analysis.Normed.Module.FiniteDimension67/-! Linear recovery with the selected leading chart, exact signed volume,8and the source-to-target factorization. Private witnesses stay in this module. -/9noncomputable section10set_option autoImplicit false11set_option maxHeartbeats 200000012open Set Module13open scoped BigOperators NNReal Matrix14namespace MathlibAnnex.PluckerRecovery15namespace Internal16universe u17open Satellite FiniteSup FiniteSup.Bridge PluckerSupport FiniteRecovery18private abbrev Coord (n : ℕ) := Fin n → ℝ19private abbrev NormModel (n : ℕ) := EquivalentSeminorm (Coord n)20private abbrev DualFrame (n : ℕ) := DeterminantFrame.Frame n (Coord n)21private abbrev dualFrameMatrix {n : ℕ} := DeterminantFrame.frameMatrix (Pi.basisFun ℝ (Fin n))22private abbrev frameDet {n : ℕ} := DeterminantFrame.frameDeterminant (Pi.basisFun ℝ (Fin n))23private abbrev replacementDet {n : ℕ} := DeterminantFrame.replacementDeterminant (Pi.basisFun ℝ (Fin n))24private abbrev frameCoordinates {n : ℕ} := @DeterminantFrame.frameCoordinates n (Coord n) _ _25private abbrev framePreimage {n : ℕ} (B : DualFrame n) (c : Coord n) := (dualFrameMatrix B)⁻¹.mulVec c26private abbrev IsDualContraction {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) := ∀ x, |r x| ≤ M.p x27private abbrev dualRowSet {n : ℕ} (M : NormModel n) := {r : Coord n →L[ℝ] ℝ | IsDualContraction M r}28private abbrev dualFrameSet {n : ℕ} (M : NormModel n) := {B : DualFrame n | ∀ i, IsDualContraction M (B i)}2930private instance modelFiniteDimensional {n : ℕ} (M : NormModel n) : FiniteDimensional ℝ (EquivalentSeminorm.Space M) :=31 inferInstanceAs (FiniteDimensional ℝ (Coord n))3233private def modelBasis {n : ℕ} (M : NormModel n) : Basis (Fin n) ℝ (EquivalentSeminorm.Space M) :=34 Pi.basisFun ℝ (Fin n)3536private def toModelRow {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :37 EquivalentSeminorm.Space M →L[ℝ] ℝ :=38 LinearMap.toContinuousLinearMap (show EquivalentSeminorm.Space M →ₗ[ℝ] ℝ from r.toLinearMap)3940private def fromModelRow {n : ℕ} (M : NormModel n) (r : EquivalentSeminorm.Space M →L[ℝ] ℝ) :41 Coord n →L[ℝ] ℝ :=42 LinearMap.toContinuousLinearMap (show Coord n →ₗ[ℝ] ℝ from r.toLinearMap)4344private theorem toModelRow_mem_iff {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :45 toModelRow M r ∈ DeterminantFrame.unitRowSet (EquivalentSeminorm.Space M) ↔ IsDualContraction M r := by46 rw [DeterminantFrame.mem_unitRowSet]47 constructor48 · intro h x49 have := (toModelRow M r).le_opNorm (show EquivalentSeminorm.Space M from x)50 change |r x| ≤ ‖toModelRow M r‖ * M.p x at this51 exact this.trans (by nlinarith [apply_nonneg M.p x])52 · intro h53 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one54 intro x55 change |r (show Coord n from x)| ≤ 1 * M.p (show Coord n from x)56 simpa only [one_mul] using h (show Coord n from x)5758private abbrev detMax {n : ℕ} (M : NormModel n) := DeterminantFrame.determinantMaximum (modelBasis M)59private abbrev NearMaxInverseBound {n : ℕ} (M : NormModel n) := DeterminantFrame.NearMaxInverseBound (modelBasis M)60private abbrev nearMaxFrames {n : ℕ} (M : NormModel n) (η : ℝ) := {B : DualFrame n | B ∈ dualFrameSet M ∧ detMax M - η ≤ |frameDet B|}6162private theorem toModelFrame_mem {n : ℕ} (M : NormModel n) {B : DualFrame n} (h : B ∈ dualFrameSet M) :63 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.unitFrameSet n (EquivalentSeminorm.Space M) := by64 intro i65 exact (toModelRow_mem_iff M (B i)).mpr (h i)6667private theorem toModelFrame_near {n : ℕ} (M : NormModel n) {η : ℝ} {B : DualFrame n} (h : B ∈ nearMaxFrames M η) :68 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.nearMaxFrames (modelBasis M) η :=69 ⟨toModelFrame_mem M h.1, h.2⟩7071private theorem seminorm_framePreimage_le {n : ℕ} (M : NormModel n) {η : ℝ} (H : NearMaxInverseBound M η) {B : DualFrame n}72 (h : B ∈ nearMaxFrames M η) (c : Coord n) : M.p (framePreimage B c) ≤ H.boundConstant * ‖c‖ := by73 exact H.bound (toModelFrame_near M h) c7475private theorem detMax_pos {n : ℕ} (M : NormModel n) : 0 < detMax M :=76 DeterminantFrame.determinantMaximum_pos (modelBasis M)7778private theorem nearMaxFrame_det_ne_zero {n : ℕ} (M : NormModel n) {η : ℝ}79 (hη : η < detMax M) {B : DualFrame n} (hB : B ∈ nearMaxFrames M η) : frameDet B ≠ 0 :=80 DeterminantFrame.nearMaxFrame_det_ne_zero (modelBasis M) hη (toModelFrame_near M hB)8182private abbrev SupCoord (n : ℕ) := Fin n → ℝ8384variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}85private noncomputable instance centerFintype (C : FiniteCoefficientNet (n := n) K ρ) :86 Fintype C.centers :=87 C.finite_centers.fintype88899091variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}92private def centerValue (C : FiniteCoefficientNet (n := n) K ρ) (c : C.centers) :93 Coord n := c.19495private def satelliteRadius (ε K : ℝ) : ℝ := min ε 1 / (8 * K)9697private theorem satelliteRadius_pos {ε K : ℝ} (hε : 0 < ε) (hK : 0 < K) :98 0 < satelliteRadius ε K := by99 exact div_pos (lt_min hε zero_lt_one) (mul_pos (by norm_num) hK)100101private theorem two_mul_bound_mul_satelliteRadius_lt_half {ε K : ℝ}102 (hε : 0 < ε) (hK : 0 < K) :103 2 * K * satelliteRadius ε K < ε / 2 := by104 have hden : 0 < 8 * K := mul_pos (by norm_num) hK105 have hmin : min ε 1 ≤ ε := min_le_left _ _106 unfold satelliteRadius107 calc108 2 * K * (min ε 1 / (8 * K)) = min ε 1 / 4 := by field_simp; ring109 _ ≤ ε / 4 := by linarith110 _ < ε / 2 := by linarith111112private theorem satelliteRadius_lt_half_inv {ε K : ℝ}113 (_hε : 0 < ε) (hK : 0 < K) :114 satelliteRadius ε K < 1 / (2 * K) := by115 have hmin : min ε 1 ≤ 1 := min_le_right _ _116 unfold satelliteRadius117 have hK2 : 0 < 2 * K := mul_pos (by norm_num) hK118 have hK8 : 0 < 8 * K := mul_pos (by norm_num) hK119 calc120 min ε 1 / (8 * K) ≤ 1 / (8 * K) :=121 div_le_div_of_nonneg_right hmin hK8.le122 _ < 1 / (2 * K) := by123 apply one_div_lt_one_div_of_lt hK2124 nlinarith125126private noncomputable def satelliteRadiusNNReal (ε K : ℝ) (hε : 0 < ε) (hK : 0 < K) :127 ℝ≥0 :=128 ⟨satelliteRadius ε K, (satelliteRadius_pos hε hK).le⟩129130@[simp] private theorem coe_satelliteRadiusNNReal (ε K : ℝ) (hε : 0 < ε) (hK : 0 < K) :131 (satelliteRadiusNNReal ε K hε hK : ℝ) = satelliteRadius ε K := rfl132133private abbrev MinorIndex (n N : ℕ) := MathlibAnnex.Matrix.MaximalMinorIndex n (Fin N)134private abbrev PluckerCoord (n N : ℕ) := MinorIndex n N → ℝ135private abbrev clmMatrix {n N : ℕ} (A : Coord n →L[ℝ] SupCoord N) := LinearMap.toMatrix' A.toLinearMap136private abbrev maximalMinor := @MathlibAnnex.Matrix.maximalMinor137private abbrev maximalMinors := @MathlibAnnex.Matrix.maximalMinors138private abbrev selectedSubmatrix := @MathlibAnnex.Matrix.maximalSubmatrix139private abbrev minorIndexOfOrderEmbedding := @MathlibAnnex.Matrix.MaximalMinorIndex.ofOrderEmbedding140private abbrev selectedSubmatrix_minorIndexOfOrderEmbedding := @MathlibAnnex.Matrix.maximalSubmatrix_ofOrderEmbedding141private abbrev maximalMinor_minorIndexOfOrderEmbedding := @MathlibAnnex.Matrix.maximalMinor_ofOrderEmbedding142variable {m : ℕ} {J : Type u} [Fintype J]143144private abbrev positiveSatelliteAmbientDim (m : ℕ) (J : Type u) [Fintype J] : ℕ :=145 (m + 1) + Fintype.card J146147private def baseRowIndex (J : Type u) [Fintype J] (i : Fin (m + 1)) :148 Fin (positiveSatelliteAmbientDim m J) :=149 Fin.castAdd (Fintype.card J) i150151private noncomputable def baseRowOrderEmb (m : ℕ) (J : Type u) [Fintype J] :152 Fin (m + 1) ↪o Fin (positiveSatelliteAmbientDim m J) :=153 Fin.castAddOrderEmb (Fintype.card J)154155@[simp] private theorem baseRowOrderEmb_apply (i : Fin (m + 1)) :156 baseRowOrderEmb m J i = baseRowIndex J i := by157 rfl158private noncomputable def baseMinorIndex :159 MinorIndex (m + 1) (positiveSatelliteAmbientDim m J) :=160 minorIndexOfOrderEmbedding (baseRowOrderEmb m J)161private theorem maximalMinor_configurationFinMap_base162 (C : SatelliteConfiguration (m + 1) J) :163 maximalMinor (clmMatrix (configurationFinMap C))164 (baseMinorIndex (m := m) (J := J)) = frameDet C.1 := by165 unfold baseMinorIndex166 unfold maximalMinor minorIndexOfOrderEmbedding167 rw [MathlibAnnex.Matrix.maximalMinor_ofOrderEmbedding]168 congr 1169 ext i j170 simp [baseRowOrderEmb, clmMatrix, DeterminantFrame.frameMatrix, Pi.basisFun_apply]171172private noncomputable def rawPluckerCompact {n N : ℕ} (M : NormModel n) :173 TopologicalSpace.NonemptyCompacts (PluckerCoord n N) where174 carrier := MathlibAnnex.PluckerBody.generators M N175 isCompact' := MathlibAnnex.PluckerBody.isCompact_generators M176 nonempty' := MathlibAnnex.PluckerBody.generators_nonempty M177178private theorem clm_injective_of_maximalMinor_ne_zero {n N : ℕ}179 (A : Coord n →L[ℝ] SupCoord N) (s : MinorIndex n N)180 (hs : maximalMinor (clmMatrix A) s ≠ 0) : Function.Injective A := by181 have h := MathlibAnnex.Matrix.mulVec_injective_of_maximalMinor_ne_zero (clmMatrix A) s hs182 intro x y hxy183 apply h184 simpa [clmMatrix, LinearMap.toMatrix'_mulVec] using hxy185private noncomputable abbrev leadingMinorIndex (m q : ℕ) :186 MinorIndex (m + 1) ((m + 1) + q) :=187 minorIndexOfOrderEmbedding (Fin.castAddOrderEmb q)188189/-- A sign used to record whether a raw point is the positive or negative190normalized Plücker generator. -/191private structure PluckerSign where192 value : ℝ193 value_eq : value = 1 ∨ value = -1194195namespace PluckerSign196197/-- Positive raw orientation. -/198private def positive : PluckerSign := ⟨1, Or.inl rfl⟩199200/-- Negative raw orientation. -/201private def negative : PluckerSign := ⟨-1, Or.inr rfl⟩202203@[simp] private theorem positive_value : positive.value = 1 := rfl204@[simp] private theorem negative_value : negative.value = -1 := rfl205206private theorem value_ne_zero (s : PluckerSign) : s.value ≠ 0 := by207 rcases s.value_eq with h | h <;> norm_num [h]208209private theorem value_sq (s : PluckerSign) : s.value * s.value = 1 := by210 rcases s.value_eq with h | h <;> norm_num [h]211212private theorem abs_value (s : PluckerSign) : |s.value| = 1 := by213 rcases s.value_eq with h | h <;> norm_num [h]214215end PluckerSign216217/-- The target support property strengthened by a nonzero leading Plücker218coordinate. -/219private def AnchoredPluckerGeneratorGood {m q : ℕ}220 (M : NormModel (m + 1)) (ε : ℝ)221 (z : PluckerCoord (m + 1) ((m + 1) + q)) : Prop :=222 PluckerGeneratorGood M ε z ∧ z (leadingMinorIndex m q) ≠ 0223224/-- Every oriented satellite-support maximizer has nonzero canonical base225coordinate. The proof uses the strict determinant gap before any226lexicographic refinement is performed. -/227private theorem targetRawSupportMaximizer_leading_ne_zero228 {m : ℕ} (M : NormModel (m + 1)) {η ε weight : ℝ}229 (hη0 : 0 ≤ η) (hηD : η < detMax M) (_hε : 0 < ε)230 (H : NearMaxInverseBound M η)231 (Cnet : FiniteCoefficientNet (n := m + 1) H.boundConstant232 (satelliteRadiusNNReal ε H.boundConstant _hε H.boundConstant_pos))233 (hweight : 0 < weight)234 (hgap : satelliteBudget M (centerValue Cnet) < weight * η)235 {z : PluckerCoord (m + 1)236 (positiveSatelliteAmbientDim m Cnet.centers)}237 (hz : z ∈ MathlibAnnex.NonemptyCompacts.maxSlice (rawPluckerCompact238 (N := positiveSatelliteAmbientDim m Cnet.centers) M)239 (orientedSatelliteSupport weight (centerValue Cnet)240 (maxSatelliteConfiguration M Cnet.centers241 weight (centerValue Cnet)))) :242 z (baseMinorIndex (m := m) (J := Cnet.centers)) ≠ 0 := by243 -- [R11-API-CHECK:ANC-001]244 classical245 rcases exists_contraction_maximizing_abs_configurationPolynomial_of_mem_maxSlice246 M weight (centerValue Cnet) hz with247 ⟨A, hA, hzA, hC, hmax⟩248 let C : SatelliteConfiguration (m + 1) Cnet.centers :=249 finMapConfiguration A250 have hAC : configurationFinMap C = A := by251 simp [C]252 have hnear : C.1 ∈ nearMaxFrames M η :=253 absoluteMaximizer_base_nearMax M hη0 hweight (centerValue Cnet)254 hgap hC hmax255 have hdet : frameDet C.1 ≠ 0 :=256 nearMaxFrame_det_ne_zero M hηD hnear257 have hminor :258 maximalMinor (clmMatrix A)259 (baseMinorIndex (m := m) (J := Cnet.centers)) ≠ 0 := by260 rw [← hAC, maximalMinor_configurationFinMap_base]261 exact hdet262 have hnormalized :263 MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors M A264 (baseMinorIndex (m := m) (J := Cnet.centers)) ≠ 0 := by265 -- `closedUnitBallVolume` and the selected base determinant are both nonzero.266 simp [MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors, MathlibAnnex.Matrix.maximalMinors,267 M.closedUnitBallVolume_pos.ne', hminor]268 rcases hzA with hzA | hzA269 · simpa [hzA] using hnormalized270 · rw [hzA]271 simpa using neg_ne_zero.mpr hnormalized272273/-- Every target support maximizer is both almost isometric and anchored at the274canonical leading minor. -/275private theorem targetRawSupportMaximizer_anchoredGood276 {m : ℕ} (M : NormModel (m + 1)) {η ε weight : ℝ}277 (hη0 : 0 ≤ η) (hηD : η < detMax M) (hε : 0 < ε)278 (H : NearMaxInverseBound M η)279 (Cnet : FiniteCoefficientNet (n := m + 1) H.boundConstant280 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))281 (hweight : 0 < weight)282 (hgap : satelliteBudget M (centerValue Cnet) < weight * η)283 {z : PluckerCoord (m + 1)284 (positiveSatelliteAmbientDim m Cnet.centers)}285 (hz : z ∈ MathlibAnnex.NonemptyCompacts.maxSlice (rawPluckerCompact286 (N := positiveSatelliteAmbientDim m Cnet.centers) M)287 (orientedSatelliteSupport weight (centerValue Cnet)288 (maxSatelliteConfiguration M Cnet.centers289 weight (centerValue Cnet)))) :290 PluckerGeneratorGood M ε z ∧291 z (baseMinorIndex (m := m) (J := Cnet.centers)) ≠ 0 := by292 exact ⟨targetRawSupportMaximizer_good M hη0 hηD hε H Cnet293 hweight hgap hz,294 targetRawSupportMaximizer_leading_ne_zero M hη0 hηD hε H Cnet295 hweight hgap hz⟩296297/-- Equality of the source and target Plücker bodies yields a common raw point298which is target-almost-isometric and has a nonzero canonical leading299coordinate. -/300private theorem exists_commonAnchoredRaw301 {m : ℕ} (MX MY : NormModel (m + 1)) {η ε weight : ℝ}302 (hη0 : 0 ≤ η) (hηD : η < detMax MY) (hε : 0 < ε)303 (H : NearMaxInverseBound MY η)304 (Cnet : FiniteCoefficientNet (n := m + 1) H.boundConstant305 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))306 (hweight : 0 < weight)307 (hgap : satelliteBudget MY (centerValue Cnet) < weight * η)308 (hHull :309 MathlibAnnex.PluckerBody.body MX (positiveSatelliteAmbientDim m Cnet.centers) =310 MathlibAnnex.PluckerBody.body MY (positiveSatelliteAmbientDim m Cnet.centers)) :311 ∃ z : PluckerCoord (m + 1)312 (positiveSatelliteAmbientDim m Cnet.centers),313 z ∈ MathlibAnnex.PluckerBody.generators MX314 (positiveSatelliteAmbientDim m Cnet.centers) ∧315 z ∈ MathlibAnnex.PluckerBody.generators MY316 (positiveSatelliteAmbientDim m Cnet.centers) ∧317 PluckerGeneratorGood MY ε z ∧318 z (baseMinorIndex (m := m) (J := Cnet.centers)) ≠ 0 := by319 -- [R11-API-CHECK:ANC-002]320 classical321 let RX := rawPluckerCompact322 (N := positiveSatelliteAmbientDim m Cnet.centers) MX323 let RY := rawPluckerCompact324 (N := positiveSatelliteAmbientDim m Cnet.centers) MY325 let Cstar : SatelliteConfiguration (m + 1) Cnet.centers :=326 maxSatelliteConfiguration MY Cnet.centers weight (centerValue Cnet)327 let ℓ := orientedSatelliteSupport weight (centerValue Cnet) Cstar328 have hHull' : convexHull ℝ (RX : Set (PluckerCoord (m + 1) (positiveSatelliteAmbientDim m Cnet.centers))) = convexHull ℝ (RY : Set (PluckerCoord (m + 1) (positiveSatelliteAmbientDim m Cnet.centers))) := by329 simpa [RX, RY, rawPluckerCompact, MathlibAnnex.PluckerBody.body] using hHull330 exact MathlibAnnex.exists_common_pi331 RX RY hHull' ℓ332 (fun z => PluckerGeneratorGood MY ε z ∧333 z (baseMinorIndex (m := m) (J := Cnet.centers)) ≠ 0)334 (fun z hz => targetRawSupportMaximizer_anchoredGood335 MY hη0 hηD hε H Cnet hweight hgap336 (by simpa [RY, ℓ, Cstar] using hz))337338/-- Common source/target maps with a fixed nonzero leading Plücker coordinate.339The ambient dimension is stored as `(m+1)+q`, so all later chart calculations340use the first square block and the final `q` tail rows. -/341private structure AnchoredAlmostIsometryMatch {m : ℕ}342 (MX MY : NormModel (m + 1)) (ε : ℝ) where343 q : ℕ344 z : PluckerCoord (m + 1) ((m + 1) + q)345 sourceMap : Coord (m + 1) →L[ℝ] SupCoord ((m + 1) + q)346 targetMap : Coord (m + 1) →L[ℝ] SupCoord ((m + 1) + q)347 isContraction_sourceMap : MX.IsContraction sourceMap348 isContraction_targetMap : MY.IsContraction targetMap349 finMapAlmostIsometric_targetMap : FinMapAlmostIsometric MY ε targetMap350 sourceSign : PluckerSign351 targetSign : PluckerSign352 eq_sourceSign_smul_ballVolumeScaledMaximalMinors : z = sourceSign.value • MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MX sourceMap353 eq_targetSign_smul_ballVolumeScaledMaximalMinors : z = targetSign.value • MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors MY targetMap354 apply_leadingMinorIndex_ne_zero : z (leadingMinorIndex m q) ≠ 0355356/-- Convert the old `z = v ∨ z = -v` representation into an explicit sign. -/357private theorem exists_sign_representation {ι : Type*} [Fintype ι]358 {z v : ι → ℝ} (h : z = v ∨ z = -v) :359 ∃ s : PluckerSign, z = s.value • v := by360 rcases h with h | h361 · exact ⟨PluckerSign.positive, by simp [h]⟩362 · exact ⟨PluckerSign.negative, by simp [h]⟩363364/-- Fixed-satellite-dimension anchored extraction. -/365private theorem nonempty_anchoredAlmostIsometryMatch_at_satelliteDimension366 {m : ℕ} (MX MY : NormModel (m + 1)) {η ε weight : ℝ}367 (hη0 : 0 ≤ η) (hηD : η < detMax MY) (hε : 0 < ε)368 (H : NearMaxInverseBound MY η)369 (Cnet : FiniteCoefficientNet (n := m + 1) H.boundConstant370 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))371 (hweight : 0 < weight)372 (hgap : satelliteBudget MY (centerValue Cnet) < weight * η)373 (hHull :374 MathlibAnnex.PluckerBody.body MX (positiveSatelliteAmbientDim m Cnet.centers) =375 MathlibAnnex.PluckerBody.body MY (positiveSatelliteAmbientDim m Cnet.centers)) :376 Nonempty (AnchoredAlmostIsometryMatch MX MY ε) := by377 -- [R11-API-CHECK:ANC-003]378 classical379 rcases exists_commonAnchoredRaw MX MY hη0 hηD hε H Cnet380 hweight hgap hHull with ⟨z, hzX, _hzY, hgood, hzLead⟩381 rcases hzX with ⟨T, hT, hTsign⟩382 rcases hgood with ⟨A, hA, hAlmost, hAsign⟩383 rcases exists_sign_representation hTsign with ⟨sT, hsT⟩384 rcases exists_sign_representation hAsign with ⟨sA, hsA⟩385 let q := Fintype.card Cnet.centers386 refine ⟨{387 q := q388 z := z389 sourceMap := T390 targetMap := A391 isContraction_sourceMap := hT392 isContraction_targetMap := hA393 finMapAlmostIsometric_targetMap := hAlmost394 sourceSign := sT395 targetSign := sA396 eq_sourceSign_smul_ballVolumeScaledMaximalMinors := hsT397 eq_targetSign_smul_ballVolumeScaledMaximalMinors := hsA398 apply_leadingMinorIndex_ne_zero := ?_399 }⟩400 simpa [q, leadingMinorIndex, positiveSatelliteAmbientDim,401 baseMinorIndex, baseRowOrderEmb] using hzLead402403/-- Equality of all finite Plücker bodies produces an anchored match for every404positive distortion parameter. -/405private theorem nonempty_anchoredAlmostIsometryMatch_of_all_body_eq406 {m : ℕ} (MX MY : NormModel (m + 1)) {ε : ℝ} (hε : 0 < ε)407 (hBodies : ∀ N : ℕ, MathlibAnnex.PluckerBody.body MX N = MathlibAnnex.PluckerBody.body MY N) :408 Nonempty (AnchoredAlmostIsometryMatch MX MY ε) := by409 let η : ℝ := detMax MY / 2410 have hD : 0 < detMax MY := detMax_pos MY411 have hη : 0 < η := by412 dsimp [η]413 linarith414 have hηD : η < detMax MY := by415 dsimp [η]416 linarith417 rcases exists_goodSatellitePackage MY hη hηD hε with418 ⟨H, Cnet, weight, hweight, hgap, _hselectedGood⟩419 exact nonempty_anchoredAlmostIsometryMatch_at_satelliteDimension420 MX MY hη.le hηD hε H Cnet hweight hgap421 (hBodies (positiveSatelliteAmbientDim m Cnet.centers))422private def AnchoredAlmostIsometryMatch.orientationProduct423 {m : ℕ} {MX MY : NormModel (m + 1)} {ε : ℝ}424 (P : AnchoredAlmostIsometryMatch MX MY ε) : ℝ :=425 P.sourceSign.value * P.targetSign.value426427namespace AnchoredAlmostIsometryMatch428429variable {m : ℕ} {MX MY : NormModel (m + 1)} {ε : ℝ}430 (P : AnchoredAlmostIsometryMatch MX MY ε)431432/-- The orientation product is again a sign. -/433private theorem orientationProduct_eq :434 P.orientationProduct = 1 ∨ P.orientationProduct = -1 := by435 rcases P.sourceSign.value_eq with hs | hs <;>436 rcases P.targetSign.value_eq with ht | ht <;>437 simp [orientationProduct, hs, ht]438439/-- The orientation product is nonzero. -/440private theorem orientationProduct_ne_zero : P.orientationProduct ≠ 0 := by441 rcases P.orientationProduct_eq with h | h <;> simp [h]442443444/-- The orientation product has absolute value one. -/445private theorem orientationProduct_abs : |P.orientationProduct| = 1 := by446 rcases P.orientationProduct_eq with h | h <;> simp [h]447448/-- Equality of the common raw point gives the weighted maximal-minor relation449coordinate by coordinate. -/450private theorem volume_mul_maximalMinor_sourceMap_eq451 (s : MinorIndex (m + 1) ((m + 1) + P.q)) :452 MX.closedUnitBallVolume * maximalMinor (clmMatrix P.sourceMap) s =453 P.orientationProduct * MY.closedUnitBallVolume *454 maximalMinor (clmMatrix P.targetMap) s := by455 -- [R11-API-CHECK:WMI-001]456 have hs := congrFun P.eq_sourceSign_smul_ballVolumeScaledMaximalMinors s457 have ht := congrFun P.eq_targetSign_smul_ballVolumeScaledMaximalMinors s458 have hcommon :459 P.sourceSign.value *460 (MX.closedUnitBallVolume * maximalMinor (clmMatrix P.sourceMap) s) =461 P.targetSign.value *462 (MY.closedUnitBallVolume * maximalMinor (clmMatrix P.targetMap) s) := by463 calc464 P.sourceSign.value *465 (MX.closedUnitBallVolume * maximalMinor (clmMatrix P.sourceMap) s) = P.z s := by466 simpa [MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors, MathlibAnnex.Matrix.maximalMinors, smul_eq_mul,467 mul_assoc, mul_left_comm, mul_comm] using hs.symm468 _ = P.targetSign.value *469 (MY.closedUnitBallVolume * maximalMinor (clmMatrix P.targetMap) s) := by470 simpa [MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors, MathlibAnnex.Matrix.maximalMinors, smul_eq_mul,471 mul_assoc, mul_left_comm, mul_comm] using ht472 calc473 MX.closedUnitBallVolume * maximalMinor (clmMatrix P.sourceMap) s =474 (P.sourceSign.value * P.sourceSign.value) *475 (MX.closedUnitBallVolume * maximalMinor (clmMatrix P.sourceMap) s) := by476 rw [P.sourceSign.value_sq]477 ring478 _ = P.sourceSign.value *479 (P.targetSign.value *480 (MY.closedUnitBallVolume * maximalMinor (clmMatrix P.targetMap) s)) := by481 rw [mul_assoc, hcommon]482 _ = P.orientationProduct * MY.closedUnitBallVolume *483 maximalMinor (clmMatrix P.targetMap) s := by484 simp [orientationProduct, mul_assoc]485486/-- The leading source minor is nonzero. -/487private theorem sourceLeadingMinor_ne_zero :488 maximalMinor (clmMatrix P.sourceMap) (leadingMinorIndex m P.q) ≠ 0 := by489 -- [R11-API-CHECK:WMI-002]490 intro hzero491 have hs := congrFun P.eq_sourceSign_smul_ballVolumeScaledMaximalMinors (leadingMinorIndex m P.q)492 apply P.apply_leadingMinorIndex_ne_zero493 rw [hs]494 simp [MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors, MathlibAnnex.Matrix.maximalMinors, hzero]495496/-- The leading target minor is nonzero. -/497private theorem targetLeadingMinor_ne_zero :498 maximalMinor (clmMatrix P.targetMap) (leadingMinorIndex m P.q) ≠ 0 := by499 -- [R11-API-CHECK:WMI-003]500 intro hzero501 have ht := congrFun P.eq_targetSign_smul_ballVolumeScaledMaximalMinors (leadingMinorIndex m P.q)502 apply P.apply_leadingMinorIndex_ne_zero503 rw [ht]504 simp [MathlibAnnex.Matrix.ballVolumeScaledMaximalMinors, MathlibAnnex.Matrix.maximalMinors, hzero]505506/-- Both ambient maps are injective, using the fixed leading minor rather than507an existential rank criterion. -/508private theorem sourceMap_injective : Function.Injective P.sourceMap :=509 clm_injective_of_maximalMinor_ne_zero P.sourceMap510 (leadingMinorIndex m P.q) P.sourceLeadingMinor_ne_zero511512private theorem targetMap_injective : Function.Injective P.targetMap :=513 clm_injective_of_maximalMinor_ne_zero P.targetMap514 (leadingMinorIndex m P.q) P.targetLeadingMinor_ne_zero515516end AnchoredAlmostIsometryMatch517518private abbrev matrixCLM {n N : ℕ} (A : Matrix (Fin N) (Fin n) ℝ) :519 Coord n →L[ℝ] SupCoord N := LinearMap.toContinuousLinearMap (Matrix.toLin' A)520@[simp] private theorem matrixCLM_apply {n N : ℕ} (A : Matrix (Fin N) (Fin n) ℝ) (x : Coord n) :521 matrixCLM A x = A.mulVec x := rfl522@[simp] private theorem clmMatrix_matrixCLM {n N : ℕ} (A : Matrix (Fin N) (Fin n) ℝ) :523 clmMatrix (matrixCLM A) = A := LinearMap.toMatrix'_toLin' A524private theorem clmMatrix_comp {n k N : ℕ} (A : Coord n →L[ℝ] SupCoord N) (B : Coord k →L[ℝ] Coord n) :525 clmMatrix (A.comp B) = clmMatrix A * clmMatrix B := LinearMap.toMatrix'_comp A.toLinearMap B.toLinearMap526private theorem frameCoordinates_eq_mulVec {n : ℕ} (B : DualFrame n) (x : Coord n) :527 frameCoordinates B x = (dualFrameMatrix B).mulVec x := by528 simpa [frameCoordinates, dualFrameMatrix, DeterminantFrame.coordinateEquiv] using529 DeterminantFrame.frameCoordinates_eq_mulVec (Pi.basisFun ℝ (Fin n)) B x530private theorem positiveSatelliteAmbientDim_fin (m q : ℕ) :531 positiveSatelliteAmbientDim m (Fin q) = (m + 1) + q := by532 simp [positiveSatelliteAmbientDim]533534private noncomputable def castFinCLM {n N N' : ℕ} (h : N' = N)535 (A : Coord n →L[ℝ] SupCoord N) : Coord n →L[ℝ] SupCoord N' := by536 subst N'537 exact A538539private noncomputable def castMinorIndex {n N N' : ℕ} (h : N' = N)540 (s : MinorIndex n N) : MinorIndex n N' := by541 subst N'542 exact s543544private theorem castMinorIndex_symm {n N N' : ℕ} (h : N' = N)545 (s : MinorIndex n N') :546 castMinorIndex h (castMinorIndex h.symm s) = s := by547 subst N'548 rfl549550private theorem maximalMinor_castFinCLM {n N N' : ℕ} (h : N' = N)551 (A : Coord n →L[ℝ] SupCoord N) (s : MinorIndex n N) :552 maximalMinor (clmMatrix (castFinCLM h A)) (castMinorIndex h s) =553 maximalMinor (clmMatrix A) s := by554 subst N'555 rfl556557@[simp] private theorem castFinCLM_apply {n N N' : ℕ} (h : N' = N)558 (A : Coord n →L[ℝ] SupCoord N) (x : Coord n) (i : Fin N') :559 castFinCLM h A x i = A x (Fin.cast h i) := by560 subst N'561 rfl562563private theorem castFinCLM_injective {n N N' : ℕ} (h : N' = N) :564 Function.Injective (castFinCLM h :565 (Coord n →L[ℝ] SupCoord N) → (Coord n →L[ℝ] SupCoord N')) := by566 subst N'567 intro A B hAB568 exact hAB569570private theorem castFinCLM_comp {n k N N' : ℕ} (h : N' = N)571 (A : Coord n →L[ℝ] SupCoord N) (B : Coord k →L[ℝ] Coord n) :572 castFinCLM h (A.comp B) = (castFinCLM h A).comp B := by573 subst N'574 rfl575576private theorem castBaseMinorIndex_eq_leading (m q : ℕ) :577 castMinorIndex (positiveSatelliteAmbientDim_fin m q).symm578 (baseMinorIndex (m := m) (J := Fin q)) =579 leadingMinorIndex m q := by580 have aux (a b : ℕ) (h : a = b) :581 castMinorIndex (congrArg (fun k => (m + 1) + k) h).symm582 (MathlibAnnex.Matrix.MaximalMinorIndex.ofOrderEmbedding583 (Fin.castAddOrderEmb (n := m + 1) a)) =584 MathlibAnnex.Matrix.MaximalMinorIndex.ofOrderEmbedding585 (Fin.castAddOrderEmb (n := m + 1) b) := by586 subst b587 rfl588 exact aux (Fintype.card (Fin q)) q (Fintype.card_fin q)589590namespace AnchoredAlmostIsometryMatch591592variable {m : ℕ} {MX MY : NormModel (m + 1)} {ε : ℝ}593 (P : AnchoredAlmostIsometryMatch MX MY ε)594595private noncomputable def sourceMapForConfiguration :596 Coord (m + 1) →L[ℝ]597 SupCoord (positiveSatelliteAmbientDim m (Fin P.q)) :=598 castFinCLM (positiveSatelliteAmbientDim_fin m P.q) P.sourceMap599600private noncomputable def targetMapForConfiguration :601 Coord (m + 1) →L[ℝ]602 SupCoord (positiveSatelliteAmbientDim m (Fin P.q)) :=603 castFinCLM (positiveSatelliteAmbientDim_fin m P.q) P.targetMap604605/-- Source map read as a base-first satellite configuration. -/606private noncomputable def sourceConfiguration :607 SatelliteConfiguration (m + 1) (Fin P.q) :=608 finMapConfiguration P.sourceMapForConfiguration609610/-- Target map read as a base-first satellite configuration. -/611private noncomputable def targetConfiguration :612 SatelliteConfiguration (m + 1) (Fin P.q) :=613 finMapConfiguration P.targetMapForConfiguration614615@[simp] private theorem sourceConfiguration_finMap :616 configurationFinMap P.sourceConfiguration =617 P.sourceMapForConfiguration := by618 simp [sourceConfiguration]619620@[simp] private theorem targetConfiguration_finMap :621 configurationFinMap P.targetConfiguration =622 P.targetMapForConfiguration := by623 simp [targetConfiguration]624625/-- The leading raw source minor is the determinant of the recovered base626configuration. -/627private theorem sourceLeadingMinor_eq_baseDet :628 maximalMinor (clmMatrix P.sourceMap) (leadingMinorIndex m P.q) =629 frameDet P.sourceConfiguration.1 := by630 let hdim := positiveSatelliteAmbientDim_fin m P.q631 let sCard := baseMinorIndex (m := m) (J := Fin P.q)632 let sRaw : MinorIndex (m + 1) ((m + 1) + P.q) :=633 castMinorIndex hdim.symm sCard634 have hsRaw : sRaw = leadingMinorIndex m P.q := by635 exact castBaseMinorIndex_eq_leading m P.q636 have hcast :637 maximalMinor (clmMatrix P.sourceMapForConfiguration) sCard =638 maximalMinor (clmMatrix P.sourceMap) sRaw := by639 have h := maximalMinor_castFinCLM hdim P.sourceMap sRaw640 change maximalMinor (clmMatrix P.sourceMapForConfiguration)641 (castMinorIndex hdim sRaw) =642 maximalMinor (clmMatrix P.sourceMap) sRaw at h643 rw [show castMinorIndex hdim sRaw = sCard by644 exact castMinorIndex_symm hdim sCard] at h645 exact h646 calc647 maximalMinor (clmMatrix P.sourceMap) (leadingMinorIndex m P.q) =648 maximalMinor (clmMatrix P.sourceMap) sRaw := by rw [hsRaw]649 _ = maximalMinor (clmMatrix P.sourceMapForConfiguration) sCard := hcast.symm650 _ = maximalMinor (clmMatrix (configurationFinMap P.sourceConfiguration))651 sCard := by rw [P.sourceConfiguration_finMap]652 _ = frameDet P.sourceConfiguration.1 := by653 simpa [sCard] using654 (maximalMinor_configurationFinMap_base P.sourceConfiguration)655656/-- The leading raw target minor is the determinant of the recovered base657configuration. -/658private theorem targetLeadingMinor_eq_baseDet :659 maximalMinor (clmMatrix P.targetMap) (leadingMinorIndex m P.q) =660 frameDet P.targetConfiguration.1 := by661 let hdim := positiveSatelliteAmbientDim_fin m P.q662 let sCard := baseMinorIndex (m := m) (J := Fin P.q)663 let sRaw : MinorIndex (m + 1) ((m + 1) + P.q) :=664 castMinorIndex hdim.symm sCard665 have hsRaw : sRaw = leadingMinorIndex m P.q := by666 exact castBaseMinorIndex_eq_leading m P.q667 have hcast :668 maximalMinor (clmMatrix P.targetMapForConfiguration) sCard =669 maximalMinor (clmMatrix P.targetMap) sRaw := by670 have h := maximalMinor_castFinCLM hdim P.targetMap sRaw671 change maximalMinor (clmMatrix P.targetMapForConfiguration)672 (castMinorIndex hdim sRaw) =673 maximalMinor (clmMatrix P.targetMap) sRaw at h674 rw [show castMinorIndex hdim sRaw = sCard by675 exact castMinorIndex_symm hdim sCard] at h676 exact h677 calc678 maximalMinor (clmMatrix P.targetMap) (leadingMinorIndex m P.q) =679 maximalMinor (clmMatrix P.targetMap) sRaw := by rw [hsRaw]680 _ = maximalMinor (clmMatrix P.targetMapForConfiguration) sCard := hcast.symm681 _ = maximalMinor (clmMatrix (configurationFinMap P.targetConfiguration))682 sCard := by rw [P.targetConfiguration_finMap]683 _ = frameDet P.targetConfiguration.1 := by684 simpa [sCard] using685 (maximalMinor_configurationFinMap_base P.targetConfiguration)686687/-- The fixed leading source determinant. -/688private theorem sourceBase_det_ne_zero :689 frameDet P.sourceConfiguration.1 ≠ 0 := by690 -- [R11-API-CHECK:CHT-001]691 rw [← P.sourceLeadingMinor_eq_baseDet]692 exact P.sourceLeadingMinor_ne_zero693694/-- The fixed leading target determinant. -/695private theorem targetBase_det_ne_zero :696 frameDet P.targetConfiguration.1 ≠ 0 := by697 -- [R11-API-CHECK:CHT-002]698 rw [← P.targetLeadingMinor_eq_baseDet]699 exact P.targetLeadingMinor_ne_zero700701/-- Inverse reconstruction for an arbitrary nondegenerate dual frame. -/702private theorem inverse_mulVec_frameCoordinates_of_det_ne_zero703 {n : ℕ} (B : DualFrame n) (hB : frameDet B ≠ 0)704 (x : Coord n) :705 (dualFrameMatrix B)⁻¹.mulVec (frameCoordinates B x) = x := by706 -- [R11-API-CHECK:CHT-003]707 have hunit : IsUnit (dualFrameMatrix B).det :=708 isUnit_iff_ne_zero.mpr (by simpa [frameDet, dualFrameMatrix, DeterminantFrame.frameDeterminant] using hB)709 rw [frameCoordinates_eq_mulVec, Matrix.mulVec_mulVec]710 rw [Matrix.nonsing_inv_mul _ hunit]711 exact Matrix.one_mulVec x712713/-- Matrix of the recovered source-to-target map. -/714private noncomputable def inducedMatrix : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ :=715 (dualFrameMatrix P.targetConfiguration.1)⁻¹ *716 dualFrameMatrix P.sourceConfiguration.1717718/-- Recovered coordinate linear map. -/719private noncomputable def inducedLinearMap : Coord (m + 1) →L[ℝ] Coord (m + 1) :=720 matrixCLM P.inducedMatrix721722@[simp] private theorem inducedLinearMap_apply (x : Coord (m + 1)) :723 P.inducedLinearMap x =724 (dualFrameMatrix P.targetConfiguration.1)⁻¹.mulVec725 (frameCoordinates P.sourceConfiguration.1 x) := by726 -- [R11-API-CHECK:CHT-004]727 simp [inducedLinearMap, inducedMatrix, matrixCLM_apply,728 Matrix.mulVec_mulVec, frameCoordinates_eq_mulVec]729private theorem volume_mul_frameDet_sourceConfiguration_eq :730 MX.closedUnitBallVolume * frameDet P.sourceConfiguration.1 =731 P.orientationProduct * MY.closedUnitBallVolume *732 frameDet P.targetConfiguration.1 := by733 -- [R11-API-CHECK:CHT-006]734 rw [← P.sourceLeadingMinor_eq_baseDet, ← P.targetLeadingMinor_eq_baseDet]735 exact P.volume_mul_maximalMinor_sourceMap_eq (leadingMinorIndex m P.q)736737/-- The generic R09 factorization is applied in the same fixed leading chart. -/738private theorem factorization : P.targetMap.comp P.inducedLinearMap = P.sourceMap := by739 let c : ℝ := P.orientationProduct * MY.closedUnitBallVolume / MX.closedUnitBallVolume740 have hc : c ≠ 0 := div_ne_zero741 (mul_ne_zero P.orientationProduct_ne_zero MY.closedUnitBallVolume_pos.ne') MX.closedUnitBallVolume_pos.ne'742 have hprop : MathlibAnnex.Matrix.MaximalMinorsProportional743 (clmMatrix P.sourceMap) (clmMatrix P.targetMap) c := by744 intro t745 apply mul_left_cancel₀ MX.closedUnitBallVolume_pos.ne'746 calc747 MX.closedUnitBallVolume * maximalMinor (clmMatrix P.sourceMap) t =748 P.orientationProduct * MY.closedUnitBallVolume * maximalMinor (clmMatrix P.targetMap) t :=749 P.volume_mul_maximalMinor_sourceMap_eq t750 _ = MX.closedUnitBallVolume * (c * maximalMinor (clmMatrix P.targetMap) t) := by751 dsimp [c]752 field_simp [MX.closedUnitBallVolume_pos.ne']753 have ht : MathlibAnnex.Matrix.orientedMaximalMinor (clmMatrix P.targetMap) (Fin.castAdd P.q) ≠ 0 := by754 have hn := P.targetLeadingMinor_ne_zero755 change MathlibAnnex.Matrix.maximalMinor (clmMatrix P.targetMap)756 (MathlibAnnex.Matrix.MaximalMinorIndex.ofOrderEmbedding (Fin.castAddOrderEmb P.q)) ≠ 0 at hn757 rw [MathlibAnnex.Matrix.maximalMinor_ofOrderEmbedding] at hn758 exact hn759 have hf := MathlibAnnex.Matrix.mul_chartFactor_eq_of_maximalMinorsProportional760 (clmMatrix P.sourceMap) (clmMatrix P.targetMap) c hc hprop (Fin.castAdd P.q) ht761 have hsbase : (clmMatrix P.sourceMap).submatrix (Fin.castAdd P.q) id =762 dualFrameMatrix P.sourceConfiguration.1 := by763 ext i j764 simp [sourceConfiguration, sourceMapForConfiguration, clmMatrix, dualFrameMatrix,765 DeterminantFrame.frameMatrix, Pi.basisFun_apply, finMapConfiguration_base_apply,766 castFinCLM_apply, positiveSatelliteAmbientDim]767 have htbase : (clmMatrix P.targetMap).submatrix (Fin.castAdd P.q) id =768 dualFrameMatrix P.targetConfiguration.1 := by769 ext i j770 simp [targetConfiguration, targetMapForConfiguration, clmMatrix, dualFrameMatrix,771 DeterminantFrame.frameMatrix, Pi.basisFun_apply, finMapConfiguration_base_apply,772 castFinCLM_apply, positiveSatelliteAmbientDim]773 have hmat : clmMatrix (P.targetMap.comp P.inducedLinearMap) = clmMatrix P.sourceMap := by774 rw [clmMatrix_comp]775 simpa [inducedLinearMap, inducedMatrix, MathlibAnnex.Matrix.chartFactor, hsbase, htbase] using hf776 apply ContinuousLinearMap.ext777 intro x778 simpa [clmMatrix] using congrArg (fun Q : Matrix (Fin ((m + 1) + P.q)) (Fin (m + 1)) ℝ => Q.mulVec x) hmat779private theorem inducedLinearMap_injective : Function.Injective P.inducedLinearMap := by780 -- [R11-API-CHECK:CHT-011]781 intro x y hxy782 apply P.sourceMap_injective783 have hx := congrArg784 (fun F : Coord (m + 1) →L[ℝ] SupCoord ((m + 1) + P.q) => F x)785 P.factorization786 have hy := congrArg787 (fun F : Coord (m + 1) →L[ℝ] SupCoord ((m + 1) + P.q) => F y)788 P.factorization789 calc790 P.sourceMap x = P.targetMap (P.inducedLinearMap x) := hx.symm791 _ = P.targetMap (P.inducedLinearMap y) := congrArg P.targetMap hxy792 _ = P.sourceMap y := hy793794end AnchoredAlmostIsometryMatch795namespace AnchoredAlmostIsometryMatch796797variable {m : ℕ} {MX MY : NormModel (m + 1)} {ε : ℝ}798 (P : AnchoredAlmostIsometryMatch MX MY ε)799800/-- Strict recovered-map estimate away from the origin. -/801private theorem inducedLinearMap_strict_model_bound802 {x : Coord (m + 1)} (hx : x ≠ 0) :803 (1 - ε) * MY.p (P.inducedLinearMap x) < MX.p x := by804 have hLx : P.inducedLinearMap x ≠ 0 := by805 intro hzero806 exact hx (P.inducedLinearMap_injective (by rw [map_zero]; exact hzero))807 have hlower := P.finMapAlmostIsometric_targetMap.lower_of_ne_zero hLx808 have hfactor : P.targetMap (P.inducedLinearMap x) = P.sourceMap x := by809 simpa using congrArg (fun F : Coord (m + 1) →L[ℝ]810 SupCoord ((m + 1) + P.q) => F x) P.factorization811 rw [hfactor] at hlower812 exact hlower.trans_le (P.isContraction_sourceMap x)813814/-- Non-strict recovered-map estimate valid at every vector. -/815private theorem inducedLinearMap_model_bound (x : Coord (m + 1)) :816 (1 - ε) * MY.p (P.inducedLinearMap x) ≤ MX.p x := by817 by_cases hx : x = 0818 · subst x819 simp only [map_zero, mul_zero, le_refl]820 · exact (P.inducedLinearMap_strict_model_bound hx).le821822/-- When `ε < 1`, the recovered map is quantitatively bounded from the source823model norm to the target model norm. -/824private theorem inducedLinearMap_model_norm_le825 (hε1 : ε < 1) (x : Coord (m + 1)) :826 MY.p (P.inducedLinearMap x) ≤ (1 - ε)⁻¹ * MX.p x := by827 -- [R11-API-CHECK:LIN-002]828 have hpos : 0 < 1 - ε := sub_pos.mpr hε1829 have h := P.inducedLinearMap_model_bound x830 apply (le_inv_mul_iff₀ hpos).2831 simpa [mul_assoc, mul_left_comm, mul_comm] using h832833/-- The recovered map is algebraically bijective in equal finite dimension. -/834private theorem inducedLinearMap_surjective : Function.Surjective P.inducedLinearMap := by835 -- [R11-API-CHECK:LIN-003]836 exact LinearMap.surjective_of_injective P.inducedLinearMap_injective837838839/-- The ambient ranges of the common representatives agree. The forward840inclusion is the factorization `T = A ∘ L`; the reverse inclusion uses841surjectivity of the recovered square map. -/842private theorem ambientRange_eq :843 Set.range P.sourceMap = Set.range P.targetMap := by844 -- [R11-API-CHECK:LIN-004]845 ext y846 constructor847 · rintro ⟨x, rfl⟩848 refine ⟨P.inducedLinearMap x, ?_⟩849 simpa using congrArg850 (fun F : Coord (m + 1) →L[ℝ] SupCoord ((m + 1) + P.q) => F x)851 P.factorization852 · rintro ⟨x, rfl⟩853 rcases P.inducedLinearMap_surjective x with ⟨u, hu⟩854 refine ⟨u, ?_⟩855 have hfactor := congrArg856 (fun F : Coord (m + 1) →L[ℝ] SupCoord ((m + 1) + P.q) => F u)857 P.factorization858 simpa [hu] using hfactor.symm859860/-- For `ε ≤ 1/2`, the target model norm of the recovered map is bounded by861twice the source model norm. -/862private theorem inducedLinearMap_model_norm_le_two863 (hεhalf : ε ≤ (1 / 2 : ℝ)) (x : Coord (m + 1)) :864 MY.p (P.inducedLinearMap x) ≤ 2 * MX.p x := by865 -- [R11-API-CHECK:LIN-005]866 have hcoeff : (1 / 2 : ℝ) ≤ 1 - ε := by linarith867 have hnonneg : 0 ≤ MY.p (P.inducedLinearMap x) := apply_nonneg MY.p _868 have h := P.inducedLinearMap_model_bound x869 nlinarith870871/-- Uniform reference-sup-norm bound used by the compact-limit stage. -/872private theorem inducedLinearMap_reference_norm_le873 (hεhalf : ε ≤ (1 / 2 : ℝ)) (x : Coord (m + 1)) :874 ‖P.inducedLinearMap x‖ ≤875 (2 * MX.upper / MY.lower) * ‖x‖ := by876 -- [R11-API-CHECK:LIN-006]877 have hlow := MY.lower_le (P.inducedLinearMap x)878 have hmid := P.inducedLinearMap_model_norm_le_two hεhalf x879 have hupp := MX.le_upper x880 have hpos : 0 < MY.lower := MY.lower_pos881 rw [div_mul_eq_mul_div]882 apply (le_div_iff₀ hpos).2883 nlinarith884885end AnchoredAlmostIsometryMatch886namespace AnchoredAlmostIsometryMatch887888variable {m : ℕ} {MX MY : NormModel (m + 1)} {ε : ℝ}889 (P : AnchoredAlmostIsometryMatch MX MY ε)890891/-- Determinant of the recovered square coordinate map. -/892private noncomputable def inducedDet : ℝ := P.inducedMatrix.det893894/-- Matrix form of the ambient factorization. -/895private theorem matrix_factorization :896 clmMatrix P.sourceMap =897 clmMatrix P.targetMap * clmMatrix P.inducedLinearMap := by898 -- [R11-API-CHECK:VOL-004]899 rw [← clmMatrix_comp, P.factorization]900901/-- Every source maximal minor is the corresponding target maximal minor times902`det L`. -/903private theorem sourceMinor_eq_targetMinor_mul_inducedDet904 (s : MinorIndex (m + 1) ((m + 1) + P.q)) :905 maximalMinor (clmMatrix P.sourceMap) s =906 maximalMinor (clmMatrix P.targetMap) s * P.inducedDet := by907 -- [R11-API-CHECK:VOL-005]908 rw [P.matrix_factorization]909 simpa only [maximalMinor, inducedDet, inducedLinearMap, clmMatrix_matrixCLM] using910 MathlibAnnex.Matrix.maximalMinor_mul (clmMatrix P.targetMap) (clmMatrix P.inducedLinearMap) s911912/-- Signed determinant-volume normalization. -/913private theorem inducedDet_signed_volume :914 MX.closedUnitBallVolume * P.inducedDet =915 P.orientationProduct * MY.closedUnitBallVolume := by916 -- [R11-API-CHECK:VOL-006]917 have hweighted := P.volume_mul_maximalMinor_sourceMap_eq918 (leadingMinorIndex m P.q)919 rw [P.sourceMinor_eq_targetMinor_mul_inducedDet] at hweighted920 have hA := P.targetLeadingMinor_ne_zero921 have hcancel :922 (MX.closedUnitBallVolume * P.inducedDet) *923 maximalMinor (clmMatrix P.targetMap)924 (leadingMinorIndex m P.q) =925 (P.orientationProduct * MY.closedUnitBallVolume) *926 maximalMinor (clmMatrix P.targetMap)927 (leadingMinorIndex m P.q) := by928 simpa [mul_assoc, mul_left_comm, mul_comm] using hweighted929 exact mul_right_cancel₀ hA hcancel930931/-- Exact absolute determinant normalization. -/932private theorem inducedDet_abs_volume :933 MX.closedUnitBallVolume * |P.inducedDet| = MY.closedUnitBallVolume := by934 -- [R11-API-CHECK:VOL-007]935 have h := congrArg abs P.inducedDet_signed_volume936 rw [abs_mul, abs_of_pos MX.closedUnitBallVolume_pos,937 abs_mul, P.orientationProduct_abs, one_mul,938 abs_of_pos MY.closedUnitBallVolume_pos] at h939 exact h940941/-- In particular the recovered square map is nonsingular. -/942private theorem inducedDet_ne_zero : P.inducedDet ≠ 0 := by943 intro hzero944 have h := P.inducedDet_abs_volume945 rw [hzero, abs_zero, mul_zero] at h946 exact MY.closedUnitBallVolume_pos.ne' h.symm947948end AnchoredAlmostIsometryMatch949950end Internal951open Internal952structure LinearCertificate {m : ℕ}953 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) (ε : ℝ) where954 q : ℕ955 sourceMap : (Fin (m + 1) → ℝ) →L[ℝ] (Fin ((m + 1) + q) → ℝ)956 targetMap : (Fin (m + 1) → ℝ) →L[ℝ] (Fin ((m + 1) + q) → ℝ)957 linearMap : (Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ)958 factor : targetMap.comp linearMap = sourceMap959 range_sourceMap_eq_range_targetMap : Set.range sourceMap = Set.range targetMap960 injective : Function.Injective linearMap961 surjective : Function.Surjective linearMap962 one_sub_mul_seminorm_linearMap_le : ∀ x, (1 - ε) * MY.p (linearMap x) ≤ MX.p x963 det : ℝ964 det_eq : det = ContinuousLinearMap.det linearMap965 closedUnitBallVolume_mul_abs_det : MX.closedUnitBallVolume * |det| = MY.closedUnitBallVolume966967namespace Internal968private noncomputable def AnchoredAlmostIsometryMatch.toRecoveryCertificate969 {m : ℕ} {MX MY : NormModel (m + 1)} {ε : ℝ}970 (P : AnchoredAlmostIsometryMatch MX MY ε) :971 LinearCertificate MX MY ε where972 q := P.q973 sourceMap := P.sourceMap974 targetMap := P.targetMap975 linearMap := P.inducedLinearMap976 factor := P.factorization977 range_sourceMap_eq_range_targetMap := P.ambientRange_eq978 injective := P.inducedLinearMap_injective979 surjective := P.inducedLinearMap_surjective980 one_sub_mul_seminorm_linearMap_le := P.inducedLinearMap_model_bound981 det := P.inducedDet982 det_eq := by983 simp [AnchoredAlmostIsometryMatch.inducedDet,984 AnchoredAlmostIsometryMatch.inducedLinearMap,985 clmMatrix_matrixCLM, ← LinearMap.det_toMatrix', clmMatrix]986 closedUnitBallVolume_mul_abs_det := P.inducedDet_abs_volume987988end Internal989theorem nonempty_linearCertificate_of_pluckerBodies_eq990 {m : ℕ} (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) {ε : ℝ} (hε : 0 < ε)991 (hBodies : ∀ N : ℕ, MathlibAnnex.PluckerBody.body MX N = MathlibAnnex.PluckerBody.body MY N) :992 Nonempty (LinearCertificate MX MY ε) := by993 rcases nonempty_anchoredAlmostIsometryMatch_of_all_body_eq MX MY hε hBodies994 with ⟨P⟩995 exact ⟨P.toRecoveryCertificate⟩996997998namespace LinearCertificate9991000variable {m : ℕ} {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)} {ε : ℝ}1001 (C : LinearCertificate MX MY ε)10021003/-- Model-norm uniformity at distortions at most one half. -/1004theorem seminorm_linearMap_le_two_mul (hεhalf : ε ≤ (1 / 2 : ℝ))1005 (x : (Fin (m + 1) → ℝ)) :1006 MY.p (C.linearMap x) ≤ 2 * MX.p x := by1007 -- [R11-API-CHECK:REC-001]1008 have hcoeff : (1 / 2 : ℝ) ≤ 1 - ε := by linarith1009 have hnonneg : 0 ≤ MY.p (C.linearMap x) := apply_nonneg MY.p _1010 have h := C.one_sub_mul_seminorm_linearMap_le x1011 nlinarith10121013/-- A distortion-independent reference-norm bound for the future sequence. -/1014theorem referenceNorm_le (hεhalf : ε ≤ (1 / 2 : ℝ))1015 (x : (Fin (m + 1) → ℝ)) :1016 ‖C.linearMap x‖ ≤ (2 * MX.upper / MY.lower) * ‖x‖ := by1017 -- [R11-API-CHECK:REC-002]1018 have hlow := MY.lower_le (C.linearMap x)1019 have hmid := C.seminorm_linearMap_le_two_mul hεhalf x1020 have hupp := MX.le_upper x1021 rw [div_mul_eq_mul_div]1022 apply (le_div_iff₀ MY.lower_pos).21023 nlinarith10241025end LinearCertificate10261027end MathlibAnnex.PluckerRecovery