Exact source: MathlibAnnex/Analysis/Normed/Plucker/LimitRecovery.lean
Pinned GitHub source · Raw UTF-8 source
Back to The recovered contraction maps one unit ball onto the other
1import MathlibAnnex.Analysis.Normed.Plucker.RecoveryCertificate2import MathlibAnnex.Analysis.Normed.Ball.VolumeRigidity3import Mathlib.Analysis.Normed.Module.FiniteDimension45/-! Compact recovery limit, exact top volume, and rigidity of the ball image. -/6noncomputable section7set_option autoImplicit false8set_option maxHeartbeats 20000009open Set Filter MeasureTheory10open scoped ENNReal11namespace MathlibAnnex.PluckerRecovery12namespace Internal13private abbrev clmMatrix {n N : ℕ} (A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) := LinearMap.toMatrix' A.toLinearMap14private def recoveryEpsilon (k : ℕ) : ℝ := 1 / ((k + 2 : ℕ) : ℝ)1516@[simp] private theorem recoveryEpsilon_pos (k : ℕ) : 0 < recoveryEpsilon k := by17 -- [R11-API-CHECK:LIM-001]18 apply one_div_pos.mpr19 exact_mod_cast (by omega : 0 < k + 2)2021@[simp] private theorem recoveryEpsilon_le_half (k : ℕ) :22 recoveryEpsilon k ≤ (1 / 2 : ℝ) := by23 -- [R11-API-CHECK:LIM-002]24 have hden : (2 : ℝ) ≤ ((k + 2 : ℕ) : ℝ) := by25 exact_mod_cast (by omega : 2 ≤ k + 2)26 exact one_div_le_one_div_of_le (by norm_num) hden2728/-- The chosen distortions converge to zero. -/29private theorem tendsto_recoveryEpsilon_zero :30 Filter.Tendsto recoveryEpsilon Filter.atTop (nhds 0) := by31 -- [R11-API-CHECK:LIM-003]32 change Filter.Tendsto (fun k : ℕ => 1 / (((k + 2 : ℕ) : ℝ)))33 Filter.atTop (nhds 0)34 have hden : Filter.Tendsto (fun k : ℕ => (k : ℝ) + 2)35 Filter.atTop Filter.atTop :=36 Filter.tendsto_atTop_add_const_right Filter.atTop 237 tendsto_natCast_atTop_atTop38 simpa only [one_div, Function.comp_def, Nat.cast_add, Nat.cast_ofNat] using39 (tendsto_inv_atTop_zero.comp hden)4041/-- Choice of one recovery certificate at each canonical distortion. -/42private noncomputable def recoveryCertificateSequence {m : ℕ}43 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))44 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N)45 (k : ℕ) : LinearCertificate MX MY (recoveryEpsilon k) :=46 Classical.choice47 (nonempty_linearCertificate_of_pluckerBodies_eq MX MY48 (recoveryEpsilon_pos k) hBodies)4950/-- The square map in the `k`-th recovery certificate. -/51private noncomputable def recoveryMapSequence {m : ℕ}52 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))53 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N)54 (k : ℕ) : (Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ) :=55 (recoveryCertificateSequence MX MY hBodies k).linearMap5657/-- Uniform reference-norm bound for the whole recovery sequence. -/58private theorem recoveryMapSequence_referenceNorm_le {m : ℕ}59 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))60 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N)61 (k : ℕ) (x : (Fin (m + 1) → ℝ)) :62 ‖recoveryMapSequence MX MY hBodies k x‖ ≤63 (2 * MX.upper / MY.lower) * ‖x‖ := by64 -- [R11-API-CHECK:LIM-004]65 exact (recoveryCertificateSequence MX MY hBodies k).referenceNorm_le66 (recoveryEpsilon_le_half k) x6768/-- Exact top-volume identity for every map in the sequence. -/69private theorem closedUnitBallVolume_mul_abs_det_recoveryMapSequence {m : ℕ}70 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))71 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N)72 (k : ℕ) :73 MX.closedUnitBallVolume *74 |Matrix.det (clmMatrix (recoveryMapSequence MX MY hBodies k))| =75 MY.closedUnitBallVolume := by76 -- [R11-API-CHECK:LIM-005]77 let C := recoveryCertificateSequence MX MY hBodies k78 have h := C.closedUnitBallVolume_mul_abs_det79 rw [C.det_eq] at h80 simpa [recoveryMapSequence, C] using h8182/-- Vanishing-distortion model estimate for every sequence term. -/83private theorem one_sub_mul_seminorm_recoveryMapSequence_le {m : ℕ}84 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))85 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N)86 (k : ℕ) (x : (Fin (m + 1) → ℝ)) :87 (1 - recoveryEpsilon k) *88 MY.p (recoveryMapSequence MX MY hBodies k x) ≤ MX.p x := by89 exact (recoveryCertificateSequence MX MY hBodies k).one_sub_mul_seminorm_linearMap_le x90private def recoveryOperatorRadius {m : ℕ}91 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) : ℝ :=92 2 * MX.upper / MY.lower9394@[simp] private theorem recoveryOperatorRadius_pos {m : ℕ}95 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) :96 0 < recoveryOperatorRadius MX MY := by97 unfold recoveryOperatorRadius98 exact div_pos (mul_pos (by norm_num) MX.upper_pos) MY.lower_pos99100@[simp] private theorem recoveryOperatorRadius_nonneg {m : ℕ}101 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) :102 0 ≤ recoveryOperatorRadius MX MY :=103 (recoveryOperatorRadius_pos MX MY).le104105/-- One closed operator ball containing every recovery map. -/106private def recoveryOperatorCarrier {m : ℕ}107 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) :108 Set ((Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ)) :=109 Metric.closedBall 0 (recoveryOperatorRadius MX MY)110111/-- Each canonical recovery map lies in the common carrier. -/112private theorem recoveryMapSequence_mem_carrier {m : ℕ}113 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))114 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N)115 (k : ℕ) :116 recoveryMapSequence MX MY hBodies k ∈117 recoveryOperatorCarrier MX MY := by118 -- [R11-API-CHECK:LIM-101]119 have hop : ‖recoveryMapSequence MX MY hBodies k‖ ≤120 recoveryOperatorRadius MX MY := by121 exact (recoveryMapSequence MX MY hBodies k).opNorm_le_bound122 (recoveryOperatorRadius_nonneg MX MY)123 (recoveryMapSequence_referenceNorm_le MX MY hBodies k)124 simpa [recoveryOperatorCarrier, Metric.mem_closedBall, dist_eq_norm,125 recoveryOperatorRadius] using hop126127/-- The common operator carrier is compact. -/128private theorem isCompact_recoveryOperatorCarrier {m : ℕ}129 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) :130 IsCompact (recoveryOperatorCarrier MX MY) := by131 -- [R11-API-CHECK:LIM-102]132 exact Metric.isCompact_of_isClosed_isBounded133 Metric.isClosed_closedBall Metric.isBounded_closedBall134135/-- A chosen convergent subsequence of the recovery maps. -/136private structure RecoverySubsequence {m : ℕ}137 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))138 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N) where139 limit : (Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ)140 index : ℕ → ℕ141 strictMono : StrictMono index142 tendsto : Tendsto143 (fun j => recoveryMapSequence MX MY hBodies (index j))144 atTop (nhds limit)145 limit_mem : limit ∈ recoveryOperatorCarrier MX MY146147/-- Compactness supplies a convergent subsequence. -/148private theorem nonempty_recoverySubsequence {m : ℕ}149 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))150 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N) :151 Nonempty (RecoverySubsequence MX MY hBodies) := by152 -- [R11-API-CHECK:LIM-103]153 rcases (isCompact_recoveryOperatorCarrier MX MY).tendsto_subseq154 (fun k => recoveryMapSequence_mem_carrier MX MY hBodies k) with155 ⟨L, hL, φ, hφ, hconv⟩156 exact ⟨{157 limit := L158 index := φ159 strictMono := hφ160 tendsto := by simpa [Function.comp_def] using hconv161 limit_mem := hL162 }⟩163private theorem tendsto_clm_apply {n : ℕ}164 {A : ℕ → (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)}165 {L : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)}166 (hA : Tendsto A atTop (nhds L)) (x : (Fin n → ℝ)) :167 Tendsto (fun k => A k x) atTop (nhds (L x)) := by168 -- [R11-API-CHECK:LIM-201]169 exact (((ContinuousLinearMap.apply ℝ ((Fin n → ℝ))) x).continuous.continuousAt.tendsto.comp hA)170171namespace RecoverySubsequence172173variable {m : ℕ} {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}174 {hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N}175 (S : RecoverySubsequence MX MY hBodies)176177/-- The distortions along the strict subsequence still tend to zero. -/178private theorem tendsto_epsilon_zero :179 Tendsto (fun j => recoveryEpsilon (S.index j)) atTop (nhds 0) := by180 -- [R11-API-CHECK:LIM-202]181 exact tendsto_recoveryEpsilon_zero.comp S.strictMono.tendsto_atTop182183/-- The selected maps converge pointwise. -/184private theorem tendsto_apply (x : (Fin (m + 1) → ℝ)) :185 Tendsto186 (fun j => recoveryMapSequence MX MY hBodies (S.index j) x)187 atTop (nhds (S.limit x)) :=188 tendsto_clm_apply S.tendsto x189190/-- Exact model contraction inequality for the limit map. -/191private theorem seminorm_limit_le (x : (Fin (m + 1) → ℝ)) :192 MY.p (S.limit x) ≤ MX.p x := by193 -- [R11-API-CHECK:LIM-203]194 have hε := S.tendsto_epsilon_zero195 have hpx : Tendsto196 (fun j => MY.p197 (recoveryMapSequence MX MY hBodies (S.index j) x))198 atTop (nhds (MY.p (S.limit x))) :=199 MY.continuous_p.continuousAt.tendsto.comp (S.tendsto_apply x)200 have hleft : Tendsto201 (fun j => (1 - recoveryEpsilon (S.index j)) *202 MY.p (recoveryMapSequence MX MY hBodies (S.index j) x))203 atTop (nhds (MY.p (S.limit x))) := by204 convert ((tendsto_const_nhds.sub hε).mul hpx) using 1; ring205 have hev : ∀ᶠ j in atTop,206 (1 - recoveryEpsilon (S.index j)) *207 MY.p (recoveryMapSequence MX MY hBodies (S.index j) x) ≤208 MX.p x :=209 Filter.Eventually.of_forall fun j =>210 one_sub_mul_seminorm_recoveryMapSequence_le MX MY hBodies (S.index j) x211 exact le_of_tendsto hleft hev212213/-- The limit sends the source model unit ball into the target model unit ball. -/214private theorem limit_image_unitBall_subset :215 S.limit '' MX.closedUnitBall ⊆ MY.closedUnitBall := by216 intro y hy217 rcases hy with ⟨x, hx, rfl⟩218 exact MY.mem_closedUnitBall.mpr219 ((S.seminorm_limit_le x).trans (MX.mem_closedUnitBall.mp hx))220221end RecoverySubsequence222namespace RecoverySubsequence223224variable {m : ℕ} {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}225 {hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N}226 (S : RecoverySubsequence MX MY hBodies)227228/-- Determinants of the selected maps converge to the determinant of the limit. -/229private theorem tendsto_coordDet :230 Tendsto231 (fun j => ContinuousLinearMap.det232 (recoveryMapSequence MX MY hBodies (S.index j)))233 atTop (nhds (ContinuousLinearMap.det S.limit)) := by234 exact ContinuousLinearMap.continuous_det.continuousAt.tendsto.comp S.tendsto235236/-- The exact top-volume identity passes to the limit. -/237private theorem closedUnitBallVolume_mul_abs_det_limit :238 MX.closedUnitBallVolume * |ContinuousLinearMap.det S.limit| = MY.closedUnitBallVolume := by239 -- [R11-API-CHECK:LIM-301]240 have hcont : Continuous241 (fun A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ) =>242 MX.closedUnitBallVolume * |ContinuousLinearMap.det A|) :=243 continuous_const.mul ContinuousLinearMap.continuous_det.abs244 have h₁ : Tendsto245 (fun j => MX.closedUnitBallVolume *246 |ContinuousLinearMap.det (recoveryMapSequence MX MY hBodies (S.index j))|)247 atTop (nhds (MX.closedUnitBallVolume * |ContinuousLinearMap.det S.limit|)) :=248 hcont.continuousAt.tendsto.comp S.tendsto249 have hterm : ∀ j,250 MX.closedUnitBallVolume *251 |ContinuousLinearMap.det (recoveryMapSequence MX MY hBodies (S.index j))| =252 MY.closedUnitBallVolume := by253 intro j254 simpa [ContinuousLinearMap.det] using255 closedUnitBallVolume_mul_abs_det_recoveryMapSequence MX MY hBodies (S.index j)256 have hfun :257 (fun j => MX.closedUnitBallVolume *258 |ContinuousLinearMap.det (recoveryMapSequence MX MY hBodies (S.index j))|) =259 (fun _ : ℕ => MY.closedUnitBallVolume) := funext hterm260 have h₂ : Tendsto261 (fun j => MX.closedUnitBallVolume *262 |ContinuousLinearMap.det (recoveryMapSequence MX MY hBodies (S.index j))|)263 atTop (nhds MY.closedUnitBallVolume) := by264 rw [hfun]265 exact tendsto_const_nhds266 exact tendsto_nhds_unique h₁ h₂267268/-- The limit determinant cannot vanish. -/269private theorem limit_coordDet_ne_zero : ContinuousLinearMap.det S.limit ≠ 0 := by270 intro hzero271 have hvol := S.closedUnitBallVolume_mul_abs_det_limit272 rw [hzero, abs_zero, mul_zero] at hvol273 exact MY.closedUnitBallVolume_pos.ne' hvol.symm274275/-- The compact limit is injective. -/276private theorem limit_injective : Function.Injective S.limit :=277 by278 apply LinearMap.ker_eq_bot.mp279 exact not_not.mp ((LinearMap.det_eq_zero_iff_ker_ne_bot).not.mp S.limit_coordDet_ne_zero)280281/-- The compact limit is surjective. -/282private theorem limit_surjective : Function.Surjective S.limit :=283 (LinearMap.injective_iff_surjective).mp S.limit_injective284285end RecoverySubsequence286287end Internal288open Internal289structure LimitCertificate {m : ℕ}290 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) where291 linearMap : (Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ)292 seminorm_linearMap_le : ∀ x, MY.p (linearMap x) ≤ MX.p x293 image_closedUnitBall_subset : linearMap '' MX.closedUnitBall ⊆ MY.closedUnitBall294 closedUnitBallVolume_mul_abs_det : MX.closedUnitBallVolume * |ContinuousLinearMap.det linearMap| = MY.closedUnitBallVolume295 det_ne_zero : ContinuousLinearMap.det linearMap ≠ 0296 injective : Function.Injective linearMap297 surjective : Function.Surjective linearMap298299/-- Equality of all finite Plücker bodies yields a limit recovery certificate. -/300theorem nonempty_limitCertificate_of_pluckerBodies_eq {m : ℕ}301 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))302 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N) :303 Nonempty (LimitCertificate MX MY) := by304 let S := Classical.choice (nonempty_recoverySubsequence MX MY hBodies)305 exact ⟨{306 linearMap := S.limit307 seminorm_linearMap_le := S.seminorm_limit_le308 image_closedUnitBall_subset := S.limit_image_unitBall_subset309 closedUnitBallVolume_mul_abs_det := S.closedUnitBallVolume_mul_abs_det_limit310 det_ne_zero := S.limit_coordDet_ne_zero311 injective := S.limit_injective312 surjective := S.limit_surjective313 }⟩314315namespace Internal316private noncomputable def linearImageBallVolume {n : ℕ}317 (M : EquivalentSeminorm (Fin n → ℝ)) (A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) : ℝ :=318 (volume (A '' M.closedUnitBall)).toReal319320/-- The real-valued image volume is `|det A|` times the source ball volume. -/321private theorem linearImageBallVolume_eq {n : ℕ}322 (M : EquivalentSeminorm (Fin n → ℝ)) (A : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) :323 linearImageBallVolume M A = |ContinuousLinearMap.det A| * M.closedUnitBallVolume := by324 -- [R11-API-CHECK:LIMVOL-002]325 rw [linearImageBallVolume, MeasureTheory.Measure.addHaar_image_continuousLinearMap,326 ENNReal.toReal_mul]327 simp [EquivalentSeminorm.closedUnitBallVolume, abs_nonneg]328329/-- Equality of finite ENNReal values follows from equality of their real parts. -/330private theorem ennreal_eq_of_toReal_eq {a b : ℝ≥0∞}331 (ha : a ≠ ⊤) (hb : b ≠ ⊤) (h : a.toReal = b.toReal) :332 a = b := by333 -- [R11-API-CHECK:LIMVOL-003]334 apply le_antisymm335 · exact (ENNReal.toReal_le_toReal ha hb).mp h.le336 · exact (ENNReal.toReal_le_toReal hb ha).mp h.ge337338namespace LimitRecoveryCertificate339variable {m : ℕ} {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)} (C : LimitCertificate MX MY)340private theorem linearImageBallVolume_eq_target :341 linearImageBallVolume MX C.linearMap = MY.closedUnitBallVolume := by342 rw [linearImageBallVolume_eq]343 simpa [mul_comm] using C.closedUnitBallVolume_mul_abs_det344345end LimitRecoveryCertificate346end Internal347348namespace LimitCertificate349variable {m : ℕ} {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)} (C : LimitCertificate MX MY)350theorem measure_image_unitBall_eq :351 volume (C.linearMap '' MX.closedUnitBall) = volume MY.closedUnitBall := by352 -- [R11-API-CHECK:LIMVOL-004]353 apply ennreal_eq_of_toReal_eq354 · exact (MX.isCompact_closedUnitBall.image C.linearMap.continuous).measure_ne_top355 · exact MY.isCompact_closedUnitBall.measure_ne_top356 · simpa [linearImageBallVolume, EquivalentSeminorm.closedUnitBallVolume] using357 Internal.LimitRecoveryCertificate.linearImageBallVolume_eq_target C358359/-- Inclusion and exact measure force equality: strict containment loses measure. -/360theorem image_unitBall_eq : C.linearMap '' MX.closedUnitBall = MY.closedUnitBall := by361 by_contra hne362 have hlt : volume (C.linearMap '' MX.closedUnitBall) < volume MY.closedUnitBall :=363 SeminormBall.measure_lt volume MY.p MY.continuous_p364 (MX.isCompact_closedUnitBall.image C.linearMap.continuous) C.image_closedUnitBall_subset hne365 exact hlt.ne C.measure_image_unitBall_eq366end LimitCertificate367end MathlibAnnex.PluckerRecovery