Exact source: MathlibAnnex/Analysis/Normed/Dual/Satellite.lean
Pinned GitHub source · Raw UTF-8 source
Back to A nearby norming point gives an almost-norming evaluation
1import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Transport2import MathlibAnnex.Analysis.Normed.Dual.DeterminantFrame3import Mathlib.Analysis.LocallyConvex.HahnBanach4import Mathlib.Analysis.Normed.Module.Span5import Mathlib.Topology.MetricSpace.Cover67noncomputable section8set_option autoImplicit false9open Set Module10open scoped BigOperators NNReal11namespace MathlibAnnex.Satellite12universe u13private abbrev Coord (n : ℕ) := Fin n → ℝ14private abbrev NormModel (n : ℕ) := EquivalentSeminorm (Coord n)15private abbrev DualFrame (n : ℕ) := DeterminantFrame.Frame n (Coord n)16private abbrev dualFrameMatrix {n : ℕ} := DeterminantFrame.frameMatrix (Pi.basisFun ℝ (Fin n))17private abbrev frameDet {n : ℕ} := DeterminantFrame.frameDeterminant (Pi.basisFun ℝ (Fin n))18private abbrev replacementDet {n : ℕ} := DeterminantFrame.replacementDeterminant (Pi.basisFun ℝ (Fin n))19private abbrev frameCoordinates {n : ℕ} := @DeterminantFrame.frameCoordinates n (Coord n) _ _20private abbrev framePreimage {n : ℕ} (B : DualFrame n) (c : Coord n) := (dualFrameMatrix B)⁻¹.mulVec c21private abbrev IsDualContraction {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) := ∀ x, |r x| ≤ M.p x22private abbrev dualRowSet {n : ℕ} (M : NormModel n) := {r : Coord n →L[ℝ] ℝ | IsDualContraction M r}23private abbrev dualFrameSet {n : ℕ} (M : NormModel n) := {B : DualFrame n | ∀ i, IsDualContraction M (B i)}2425private instance modelFiniteDimensional {n : ℕ} (M : NormModel n) : FiniteDimensional ℝ (EquivalentSeminorm.Space M) :=26 inferInstanceAs (FiniteDimensional ℝ (Coord n))2728private def modelBasis {n : ℕ} (M : NormModel n) : Basis (Fin n) ℝ (EquivalentSeminorm.Space M) :=29 Pi.basisFun ℝ (Fin n)3031private def toModelRow {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :32 EquivalentSeminorm.Space M →L[ℝ] ℝ :=33 LinearMap.toContinuousLinearMap (show EquivalentSeminorm.Space M →ₗ[ℝ] ℝ from r.toLinearMap)3435private def fromModelRow {n : ℕ} (M : NormModel n) (r : EquivalentSeminorm.Space M →L[ℝ] ℝ) :36 Coord n →L[ℝ] ℝ :=37 LinearMap.toContinuousLinearMap (show Coord n →ₗ[ℝ] ℝ from r.toLinearMap)3839private theorem toModelRow_mem_iff {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :40 toModelRow M r ∈ DeterminantFrame.unitRowSet (EquivalentSeminorm.Space M) ↔ IsDualContraction M r := by41 rw [DeterminantFrame.mem_unitRowSet]42 constructor43 · intro h x44 have := (toModelRow M r).le_opNorm (show EquivalentSeminorm.Space M from x)45 change |r x| ≤ ‖toModelRow M r‖ * M.p x at this46 exact this.trans (by nlinarith [apply_nonneg M.p x])47 · intro h48 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one49 intro x50 change |r (show Coord n from x)| ≤ 1 * M.p (show Coord n from x)51 simpa only [one_mul] using h (show Coord n from x)5253private abbrev detMax {n : ℕ} (M : NormModel n) := DeterminantFrame.determinantMaximum (modelBasis M)54private abbrev NearMaxInverseBound {n : ℕ} (M : NormModel n) := DeterminantFrame.NearMaxInverseBound (modelBasis M)55private abbrev nearMaxFrames {n : ℕ} (M : NormModel n) (η : ℝ) := {B : DualFrame n | B ∈ dualFrameSet M ∧ detMax M - η ≤ |frameDet B|}5657private theorem toModelFrame_mem {n : ℕ} (M : NormModel n) {B : DualFrame n} (h : B ∈ dualFrameSet M) :58 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.unitFrameSet n (EquivalentSeminorm.Space M) := by59 intro i60 exact (toModelRow_mem_iff M (B i)).mpr (h i)6162private theorem toModelFrame_near {n : ℕ} (M : NormModel n) {η : ℝ} {B : DualFrame n} (h : B ∈ nearMaxFrames M η) :63 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.nearMaxFrames (modelBasis M) η :=64 ⟨toModelFrame_mem M h.1, h.2⟩6566private theorem seminorm_framePreimage_le {n : ℕ} (M : NormModel n) {η : ℝ} (H : NearMaxInverseBound M η) {B : DualFrame n}67 (h : B ∈ nearMaxFrames M η) (c : Coord n) : M.p (framePreimage B c) ≤ H.boundConstant * ‖c‖ := by68 exact H.bound (toModelFrame_near M h) c6970private theorem detMax_pos {n : ℕ} (M : NormModel n) : 0 < detMax M :=71 DeterminantFrame.determinantMaximum_pos (modelBasis M)7273private theorem nearMaxFrame_det_ne_zero {n : ℕ} (M : NormModel n) {η : ℝ}74 (hη : η < detMax M) {B : DualFrame n} (hB : B ∈ nearMaxFrames M η) : frameDet B ≠ 0 :=75 DeterminantFrame.nearMaxFrame_det_ne_zero (modelBasis M) hη (toModelFrame_near M hB)7677private theorem inverse_mulVec_frameCoordinates {n : ℕ} (M : NormModel n) {η : ℝ}78 (hη : η < detMax M) {B : DualFrame n} (hB : B ∈ nearMaxFrames M η) (x : Coord n) :79 framePreimage B (frameCoordinates B x) = x := by80 exact DeterminantFrame.inverse_mulVec_frameCoordinates (modelBasis M) hη (toModelFrame_near M hB) (show EquivalentSeminorm.Space M from x)8182private theorem abs_replacementDet_le_detMax {n : ℕ} (M : NormModel n) {B : DualFrame n} (hB : B ∈ dualFrameSet M)83 (i : Fin n) {r : Coord n →L[ℝ] ℝ} (hr : IsDualContraction M r) : |replacementDet B i r| ≤ detMax M := by84 have h := DeterminantFrame.abs_replacementDeterminant_le_maximum (modelBasis M) (toModelFrame_mem M hB) i ((toModelRow_mem_iff M r).mpr hr)85 have heq : (fun j => toModelRow M ((DeterminantFrame.replaceRow B i r) j)) =86 DeterminantFrame.replaceRow (fun j => toModelRow M (B j)) i (toModelRow M r) := by87 funext j88 by_cases hj : j = i <;> simp [DeterminantFrame.replaceRow, hj]89 change |DeterminantFrame.frameDeterminant (modelBasis M)90 (fun j => toModelRow M ((DeterminantFrame.replaceRow B i r) j))| ≤ detMax M91 rw [heq]92 exact h9394private def maxFrame {n : ℕ} (M : NormModel n) : DualFrame n :=95 fun i => fromModelRow M (DeterminantFrame.maximizingFrame (modelBasis M) i)9697private theorem maxFrame_det {n : ℕ} (M : NormModel n) : |frameDet (maxFrame M)| = detMax M := rfl9899private theorem maxFrame_mem {n : ℕ} (M : NormModel n) : maxFrame M ∈ dualFrameSet M := by100 intro i101 apply (toModelRow_mem_iff M _).mp102 have h := DeterminantFrame.maximizingFrame_mem (modelBasis M) i103 convert h using 1104 ext x105 rfl106107108private abbrev replaceFrameRow {n : ℕ} := @DeterminantFrame.replaceRow n (Coord n) _ _109private abbrev functionalRow {n : ℕ} := DeterminantFrame.functionalCoordinates (Pi.basisFun ℝ (Fin n))110private theorem continuous_frameDet {n : ℕ} : Continuous (frameDet : DualFrame n → ℝ) :=111 DeterminantFrame.continuous_frameDeterminant (Pi.basisFun ℝ (Fin n))112private theorem dualFrameMatrix_replaceFrameRow {n : ℕ} (B : DualFrame n) (i : Fin n) (r : Coord n →L[ℝ] ℝ) :113 dualFrameMatrix (replaceFrameRow B i r) = (dualFrameMatrix B).updateRow i (functionalRow r) :=114 DeterminantFrame.frameMatrix_replaceRow (Pi.basisFun ℝ (Fin n)) B i r115private theorem sum_mul_replacementDet {n : ℕ} (B : DualFrame n) (hB : frameDet B ≠ 0) (r : Coord n →L[ℝ] ℝ) (c : Coord n) :116 (∑ i : Fin n, c i * replacementDet B i r) = frameDet B * r (framePreimage B c) :=117 DeterminantFrame.sum_mul_replacementDeterminant (Pi.basisFun ℝ (Fin n)) B hB r c118119private theorem isCompact_dualRowSet {n : ℕ} (M : NormModel n) : IsCompact (dualRowSet M) := by120 have hc : IsClosed (dualRowSet M) := by121 have heq : dualRowSet M = (⋂ x : Coord n, {r : Coord n →L[ℝ] ℝ | |r x| ≤ M.p x}) := by ext r; simp [dualRowSet, IsDualContraction]122 rw [heq]123 exact isClosed_iInter fun x => isClosed_le (by fun_prop) continuous_const124 have hb : Bornology.IsBounded (dualRowSet M) := by125 apply (Metric.isBounded_iff_subset_closedBall (0 : Coord n →L[ℝ] ℝ)).2126 refine ⟨M.upper, ?_⟩127 intro r hr128 rw [Metric.mem_closedBall, dist_zero_right]129 apply ContinuousLinearMap.opNorm_le_bound _ M.upper_pos.le130 intro x131 exact (hr x).trans (M.le_upper x)132 exact Metric.isCompact_of_isClosed_isBounded hc hb133134private theorem isCompact_dualFrameSet {n : ℕ} (M : NormModel n) : IsCompact (dualFrameSet M) := by135 have heq : dualFrameSet M = Set.univ.pi (fun _ : Fin n => dualRowSet M) := by ext B; simp [dualFrameSet, dualRowSet]136 rw [heq]137 exact isCompact_univ_pi fun _ => isCompact_dualRowSet M138139namespace Internal140end Internal141142open Internal143private theorem Internal.dualRowSet_eq_modelContractionSet {n : ℕ} (M : NormModel n) :144 dualRowSet M = EquivalentSeminorm.contractionSet M ℝ := by145 ext b146 simp [dualRowSet, IsDualContraction, EquivalentSeminorm.contractionSet, EquivalentSeminorm.IsContraction, Real.norm_eq_abs]147148149def satellitePolynomial {n : ℕ} {J : Type*} [Fintype J]150 (weight : ℝ) (coeff : J → Coord n)151 (B : DualFrame n) (sat : J → (Coord n →L[ℝ] ℝ)) : ℝ :=152 weight * frameDet B +153 ∑ a : J, ∑ i : Fin n, coeff a i * replacementDet B i (sat a)154155156private noncomputable def Internal.lineModelFunctional {n : ℕ} (M : NormModel n)157 (x : Coord n) (hx : x ≠ 0) :158 Module.Dual ℝ (ℝ ∙ x) :=159 (((M.p x) • ContinuousLinearEquiv.coord ℝ x hx) :160 (ℝ ∙ x) →L[ℝ] ℝ).toLinearMap161162163private theorem span_vector_eq_coord_smul {n : ℕ} (x : Coord n) (hx : x ≠ 0)164 (y : ℝ ∙ x) :165 (y : Coord n) = (ContinuousLinearEquiv.coord ℝ x hx y) • x := by166 have h := ContinuousLinearEquiv.toSpanNonzeroSingleton_coord ℝ hx y167 exact (congrArg Subtype.val h).symm168169170private theorem Internal.lineModelFunctional_le {n : ℕ} (M : NormModel n)171 (x : Coord n) (hx : x ≠ 0) (y : ℝ ∙ x) :172 lineModelFunctional M x hx y ≤ M.p (y : Coord n) := by173 let a : ℝ := ContinuousLinearEquiv.coord ℝ x hx y174 have hy : (y : Coord n) = a • x := by175 simpa [a] using span_vector_eq_coord_smul x hx y176 have hnonneg : 0 ≤ M.p x := apply_nonneg M.p x177 calc178 lineModelFunctional M x hx y = M.p x * a := by179 simp [lineModelFunctional, a]180 _ ≤ M.p x * |a| :=181 mul_le_mul_of_nonneg_left (le_abs_self a) hnonneg182 _ = |a| * M.p x := by ring183 _ = M.p (a • x) := by184 simpa [Real.norm_eq_abs] using (map_smul_eq_mul M.p a x).symm185 _ = M.p (y : Coord n) := by rw [hy]186187188private theorem exists_modelNormingFunctional {n : ℕ} (M : NormModel n)189 (x : Coord n) :190 ∃ r : Coord n →L[ℝ] ℝ,191 IsDualContraction M r ∧ r x = M.p x := by192 by_cases hx : x = 0193 · subst x194 refine ⟨0, ?_, by simp⟩195 intro y196 simp197 · let S : Subspace ℝ (Coord n) := ℝ ∙ x198 let f : Module.Dual ℝ S := lineModelFunctional M x hx199 obtain ⟨r, hrS, hrdom⟩ :=200 Module.Dual.exists_continuous_extension_of_le_seminorm_real201 S f M.continuous_p (fun y => lineModelFunctional_le M x hx y)202 refine ⟨r, ?_, ?_⟩203 · intro y204 exact hrdom y205 · have hself := hrS206 (⟨x, Submodule.mem_span_singleton_self x⟩ : S)207 simpa [S, f, lineModelFunctional] using hself208209210private theorem IsDualContraction.neg {n : ℕ} {M : NormModel n}211 {r : Coord n →L[ℝ] ℝ} (hr : IsDualContraction M r) :212 IsDualContraction M (-r) := by213 intro x214 simpa using hr x215216217private theorem Internal.exists_modelNormingEndpoints {n : ℕ} (M : NormModel n)218 (x : Coord n) :219 ∃ rPlus rMinus : Coord n →L[ℝ] ℝ,220 IsDualContraction M rPlus ∧221 IsDualContraction M rMinus ∧222 rPlus x = M.p x ∧223 rMinus x = -M.p x := by224 rcases exists_modelNormingFunctional M x with ⟨r, hr, hrx⟩225 refine ⟨r, -r, hr, hr.neg, hrx, ?_⟩226 simp [hrx]227228229def coefficientAnnulus {n : ℕ} (K : ℝ) : Set (Coord n) :=230 {c | K⁻¹ ≤ ‖c‖ ∧ ‖c‖ ≤ 1}231232233private theorem isClosed_coefficientAnnulus {n : ℕ} (K : ℝ) :234 IsClosed (coefficientAnnulus (n := n) K) := by235 change IsClosed ({c : Coord n | K⁻¹ ≤ ‖c‖} ∩ {c : Coord n | ‖c‖ ≤ 1})236 exact (isClosed_le continuous_const continuous_norm).inter237 (isClosed_le continuous_norm continuous_const)238239240private theorem isBounded_coefficientAnnulus {n : ℕ} (K : ℝ) :241 Bornology.IsBounded (coefficientAnnulus (n := n) K) := by242 rw [Metric.isBounded_iff_subset_closedBall (0 : Coord n)]243 refine ⟨1, ?_⟩244 intro c hc245 simpa [coefficientAnnulus, Metric.mem_closedBall, dist_eq_norm] using hc.2246247248private theorem isCompact_coefficientAnnulus {n : ℕ} (K : ℝ) :249 IsCompact (coefficientAnnulus (n := n) K) := by250 exact Metric.isCompact_of_isClosed_isBounded251 (isClosed_coefficientAnnulus K)252 (isBounded_coefficientAnnulus K)253254255structure FiniteCoefficientNet {n : ℕ} (K : ℝ) (ρ : ℝ≥0) where256 centers : Set (Coord n)257 centers_subset : centers ⊆ coefficientAnnulus K258 finite_centers : centers.Finite259 isCover : Metric.IsCover ρ (coefficientAnnulus K) centers260261262private theorem nonempty_finiteCoefficientNet {n : ℕ} (K : ℝ) {ρ : ℝ≥0}263 (hρ : ρ ≠ 0) : Nonempty (FiniteCoefficientNet (n := n) K ρ) := by264 rcases Metric.exists_finite_isCover_of_isCompact hρ265 (isCompact_coefficientAnnulus (n := n) K) with266 ⟨C, hCsub, hCfinite, hcover⟩267 exact ⟨⟨C, hCsub, hCfinite, hcover⟩⟩268269270variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}271272private theorem FiniteCoefficientNet.exists_center (C : FiniteCoefficientNet (n := n) K ρ)273 {z : Coord n} (hz : z ∈ coefficientAnnulus K) :274 ∃ c ∈ C.centers, edist z c ≤ ρ :=275 C.isCover hz276277278variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}279280private theorem FiniteCoefficientNet.center_mem_annulus (C : FiniteCoefficientNet (n := n) K ρ)281 {c : Coord n} (hc : c ∈ C.centers) : c ∈ coefficientAnnulus K :=282 C.centers_subset hc283284285variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}286287private noncomputable instance Internal.centerFintype (C : FiniteCoefficientNet (n := n) K ρ) :288 Fintype C.centers :=289 C.finite_centers.fintype290291292variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}293294private def Internal.centerValue (C : FiniteCoefficientNet (n := n) K ρ) (c : C.centers) :295 Coord n := c.1296297298private def Internal.satelliteRadius (ε K : ℝ) : ℝ := min ε 1 / (8 * K)299300301private theorem Internal.satelliteRadius_pos {ε K : ℝ} (hε : 0 < ε) (hK : 0 < K) :302 0 < satelliteRadius ε K := by303 exact div_pos (lt_min hε zero_lt_one) (mul_pos (by norm_num) hK)304305306private theorem Internal.two_mul_bound_mul_satelliteRadius_lt_half {ε K : ℝ}307 (hε : 0 < ε) (hK : 0 < K) :308 2 * K * satelliteRadius ε K < ε / 2 := by309 have hden : 0 < 8 * K := mul_pos (by norm_num) hK310 have hmin : min ε 1 ≤ ε := min_le_left _ _311 unfold satelliteRadius312 calc313 2 * K * (min ε 1 / (8 * K)) = min ε 1 / 4 := by field_simp; ring314 _ ≤ ε / 4 := by linarith315 _ < ε / 2 := by linarith316317318private theorem Internal.satelliteRadius_lt_half_inv {ε K : ℝ}319 (_hε : 0 < ε) (hK : 0 < K) :320 satelliteRadius ε K < 1 / (2 * K) := by321 have hmin : min ε 1 ≤ 1 := min_le_right _ _322 unfold satelliteRadius323 have hK2 : 0 < 2 * K := mul_pos (by norm_num) hK324 have hK8 : 0 < 8 * K := mul_pos (by norm_num) hK325 calc326 min ε 1 / (8 * K) ≤ 1 / (8 * K) :=327 div_le_div_of_nonneg_right hmin hK8.le328 _ < 1 / (2 * K) := by329 apply one_div_lt_one_div_of_lt hK2330 nlinarith331332333private noncomputable def Internal.satelliteRadiusNNReal (ε K : ℝ) (hε : 0 < ε) (hK : 0 < K) :334 ℝ≥0 :=335 ⟨satelliteRadius ε K, (satelliteRadius_pos hε hK).le⟩336337338@[simp] private theorem Internal.coe_satelliteRadiusNNReal (ε K : ℝ) (hε : 0 < ε) (hK : 0 < K) :339 (satelliteRadiusNNReal ε K hε hK : ℝ) = satelliteRadius ε K := rfl340341342private theorem Internal.satelliteRadiusNNReal_ne_zero {ε K : ℝ} (hε : 0 < ε) (hK : 0 < K) :343 satelliteRadiusNNReal ε K hε hK ≠ 0 := by344 exact ne_of_gt (by345 change 0 < satelliteRadius ε K346 exact satelliteRadius_pos hε hK)347348349theorem frameCoordinates_norm_le_model {n : ℕ} (M : NormModel n)350 {B : DualFrame n} (hB : B ∈ dualFrameSet M) (x : Coord n) :351 ‖frameCoordinates B x‖ ≤ M.p x := by352 apply (pi_norm_le_iff_of_nonneg (by positivity : 0 ≤ M.p x)).2353 intro i354 simpa [frameCoordinates, DeterminantFrame.frameCoordinates, Real.norm_eq_abs] using hB i x355356357theorem frameCoordinates_mem_coefficientAnnulus {n : ℕ}358 (M : NormModel n) {η : ℝ} (hη : η < detMax M)359 (H : NearMaxInverseBound M η) {B : DualFrame n}360 (hB : B ∈ nearMaxFrames M η) {x : Coord n}361 (hx : M.p x = 1) :362 frameCoordinates B x ∈ coefficientAnnulus H.boundConstant := by363 have hupper : ‖frameCoordinates B x‖ ≤ 1 := by364 simpa [hx] using frameCoordinates_norm_le_model M hB.1 x365 have hrec := inverse_mulVec_frameCoordinates M hη hB x366 have hinv : M.p x =367 M.p ((dualFrameMatrix B)⁻¹.mulVec (frameCoordinates B x)) := by368 exact congrArg M.p hrec.symm369 have hprod : 1 ≤ H.boundConstant * ‖frameCoordinates B x‖ := by370 calc371 1 = M.p x := hx.symm372 _ = M.p ((dualFrameMatrix B)⁻¹.mulVec (frameCoordinates B x)) := hinv373 _ ≤ H.boundConstant * ‖frameCoordinates B x‖ := seminorm_framePreimage_le M H hB _374 have hlower : H.boundConstant⁻¹ ≤ ‖frameCoordinates B x‖ := by375 have hdiv : 1 / H.boundConstant ≤ ‖frameCoordinates B x‖ :=376 (div_le_iff₀ H.boundConstant_pos).2 (by simpa [mul_comm] using hprod)377 simpa [one_div] using hdiv378 exact ⟨hlower, hupper⟩379380381theorem modelDist_framePreimage_le {n : ℕ} (M : NormModel n)382 {η : ℝ} (hη : η < detMax M) (H : NearMaxInverseBound M η) {B : DualFrame n}383 (hB : B ∈ nearMaxFrames M η) (x c : Coord n) :384 M.p (x - framePreimage B c) ≤385 H.boundConstant * ‖frameCoordinates B x - c‖ := by386 calc387 M.p (x - framePreimage B c) =388 M.p (framePreimage B (frameCoordinates B x) - framePreimage B c) := by389 rw [inverse_mulVec_frameCoordinates M hη hB x]390 _ = M.p (framePreimage B (frameCoordinates B x - c)) := by391 apply congrArg (fun y : Coord n => M.p y)392 simp [framePreimage, Matrix.mulVec_sub]393 _ ≤ H.boundConstant * ‖frameCoordinates B x - c‖ := by394 simpa [framePreimage] using seminorm_framePreimage_le M H hB (frameCoordinates B x - c)395396397private theorem Internal.FiniteCoefficientNet.exists_center_dist {n : ℕ} {K : ℝ} {ρ : ℝ≥0}398 (C : FiniteCoefficientNet (n := n) K ρ)399 {z : Coord n} (hz : z ∈ coefficientAnnulus K) :400 ∃ c ∈ C.centers, dist z c ≤ (ρ : ℝ) := by401 rcases C.isCover hz with ⟨c, hc, hdist⟩402 refine ⟨c, hc, ?_⟩403 exact_mod_cast hdist404405406theorem exists_net_preimage_close {n : ℕ} (M : NormModel n)407 {η : ℝ} (hη : η < detMax M) (H : NearMaxInverseBound M η)408 {ρ : ℝ≥0} (C : FiniteCoefficientNet (n := n) H.boundConstant ρ)409 {B : DualFrame n} (hB : B ∈ nearMaxFrames M η)410 {x : Coord n} (hx : M.p x = 1) :411 ∃ c ∈ C.centers,412 M.p (x - framePreimage B c) ≤ H.boundConstant * (ρ : ℝ) := by413 have hz : frameCoordinates B x ∈ coefficientAnnulus H.boundConstant :=414 frameCoordinates_mem_coefficientAnnulus M hη H hB hx415 rcases Internal.FiniteCoefficientNet.exists_center_dist C hz with ⟨c, hc, hdist⟩416 refine ⟨c, hc, ?_⟩417 calc418 M.p (x - framePreimage B c)419 ≤ H.boundConstant * ‖frameCoordinates B x - c‖ :=420 modelDist_framePreimage_le M hη H hB x c421 _ = H.boundConstant * dist (frameCoordinates B x) c := by422 rw [dist_eq_norm]423 _ ≤ H.boundConstant * (ρ : ℝ) :=424 mul_le_mul_of_nonneg_left hdist H.boundConstant_nonneg425426427def satelliteBudget {n : ℕ} {J : Type u} [Fintype J]428 (M : NormModel n) (coeff : J → Coord n) : ℝ :=429 detMax M * ∑ a : J, ∑ i : Fin n, |coeff a i|430431432private theorem Internal.satelliteBudget_nonneg {n : ℕ} {J : Type u} [Fintype J]433 (M : NormModel n) (coeff : J → Coord n) :434 0 ≤ satelliteBudget M coeff := by435 unfold satelliteBudget436 exact mul_nonneg (detMax_pos M).le437 (Finset.sum_nonneg fun a _ =>438 Finset.sum_nonneg fun i _ => abs_nonneg (coeff a i))439440441theorem abs_satelliteTerms_le_budget {n : ℕ} {J : Type u} [Fintype J]442 (M : NormModel n) (coeff : J → Coord n) {B : DualFrame n}443 (hB : B ∈ dualFrameSet M)444 (sat : J → (Coord n →L[ℝ] ℝ))445 (hsat : ∀ a, IsDualContraction M (sat a)) :446 |∑ a : J, ∑ i : Fin n,447 coeff a i * replacementDet B i (sat a)| ≤448 satelliteBudget M coeff := by449 calc450 |∑ a : J, ∑ i : Fin n,451 coeff a i * replacementDet B i (sat a)|452 ≤ ∑ a : J, |∑ i : Fin n,453 coeff a i * replacementDet B i (sat a)| :=454 Finset.abs_sum_le_sum_abs _ _455 _ ≤ ∑ a : J, ∑ i : Fin n,456 |coeff a i * replacementDet B i (sat a)| := by457 apply Finset.sum_le_sum458 intro a ha459 exact Finset.abs_sum_le_sum_abs _ _460 _ ≤ ∑ a : J, ∑ i : Fin n,461 |coeff a i| * detMax M := by462 apply Finset.sum_le_sum463 intro a ha464 apply Finset.sum_le_sum465 intro i hi466 rw [abs_mul]467 exact mul_le_mul_of_nonneg_left468 (abs_replacementDet_le_detMax M hB i (hsat a)) (abs_nonneg _)469 _ = satelliteBudget M coeff := by470 unfold satelliteBudget471 rw [Finset.mul_sum]472 apply Finset.sum_congr rfl473 intro a ha474 rw [Finset.mul_sum]475 apply Finset.sum_congr rfl476 intro i hi477 ring478479480theorem abs_satellitePolynomial_le {n : ℕ} {J : Type u} [Fintype J]481 (M : NormModel n) {weight : ℝ} (hweight : 0 ≤ weight)482 (coeff : J → Coord n) {B : DualFrame n}483 (hB : B ∈ dualFrameSet M)484 (sat : J → (Coord n →L[ℝ] ℝ))485 (hsat : ∀ a, IsDualContraction M (sat a)) :486 |satellitePolynomial weight coeff B sat| ≤487 weight * |frameDet B| + satelliteBudget M coeff := by488 unfold satellitePolynomial489 calc490 |weight * frameDet B +491 ∑ a : J, ∑ i : Fin n,492 coeff a i * replacementDet B i (sat a)|493 ≤ |weight * frameDet B| +494 |∑ a : J, ∑ i : Fin n,495 coeff a i * replacementDet B i (sat a)| := abs_add_le _ _496 _ ≤ weight * |frameDet B| + satelliteBudget M coeff := by497 rw [abs_mul, abs_of_nonneg hweight]498 exact add_le_add le_rfl499 (abs_satelliteTerms_le_budget M coeff hB sat hsat)500501502theorem base_mem_nearMax_of_benchmark_le {n : ℕ} {J : Type u} [Fintype J]503 (M : NormModel n) {η weight : ℝ} (_hη0 : 0 ≤ η) (hweight : 0 < weight)504 (coeff : J → Coord n) {B : DualFrame n}505 (hB : B ∈ dualFrameSet M)506 (sat : J → (Coord n →L[ℝ] ℝ))507 (hsat : ∀ a, IsDualContraction M (sat a))508 (hgap : satelliteBudget M coeff < weight * η)509 (hbenchmark : weight * detMax M ≤510 |satellitePolynomial weight coeff B sat|) :511 B ∈ nearMaxFrames M η := by512 refine ⟨hB, ?_⟩513 by_contra hnear514 have hdet : |frameDet B| < detMax M - η := lt_of_not_ge hnear515 have hupper := abs_satellitePolynomial_le M hweight.le coeff hB sat hsat516 have hstrict :517 weight * |frameDet B| + satelliteBudget M coeff <518 weight * detMax M := by519 have hbase : weight * |frameDet B| < weight * (detMax M - η) :=520 mul_lt_mul_of_pos_left hdet hweight521 nlinarith522 exact (not_lt_of_ge hbenchmark) (hupper.trans_lt hstrict)523524525theorem exists_weight_dominating_budget {n : ℕ} {J : Type u} [Fintype J]526 (M : NormModel n) (coeff : J → Coord n) {η : ℝ} (hη : 0 < η) :527 ∃ weight : ℝ, 0 < weight ∧ satelliteBudget M coeff < weight * η := by528 refine ⟨satelliteBudget M coeff / η + 1, ?_, ?_⟩529 · have hbudget := satelliteBudget_nonneg M coeff530 have hdiv : 0 ≤ satelliteBudget M coeff / η := div_nonneg hbudget hη.le531 linarith532 · field_simp [hη.ne']533 nlinarith [satelliteBudget_nonneg M coeff]534535536abbrev SatelliteRows (n : ℕ) (J : Type u) := J → (Coord n →L[ℝ] ℝ)537538539abbrev SatelliteConfiguration (n : ℕ) (J : Type u) :=540 DualFrame n × SatelliteRows n J541542543def satelliteRowsSet {n : ℕ} (M : NormModel n) (J : Type u) :544 Set (SatelliteRows n J) :=545 {sat | ∀ a, IsDualContraction M (sat a)}546547548def satelliteConfigurationSet {n : ℕ} (M : NormModel n) (J : Type u) :549 Set (SatelliteConfiguration n J) :=550 dualFrameSet M ×ˢ satelliteRowsSet M J551552553@[simp] private theorem Internal.mem_satelliteRowsSet {n : ℕ} (M : NormModel n)554 (J : Type u) {sat : SatelliteRows n J} :555 sat ∈ satelliteRowsSet M J ↔ ∀ a, IsDualContraction M (sat a) := Iff.rfl556557558@[simp] private theorem Internal.mem_satelliteConfigurationSet {n : ℕ} (M : NormModel n)559 (J : Type u) {C : SatelliteConfiguration n J} :560 C ∈ satelliteConfigurationSet M J ↔561 C.1 ∈ dualFrameSet M ∧ ∀ a, IsDualContraction M (C.2 a) := Iff.rfl562563564private theorem isCompact_satelliteRowsSet {n : ℕ} (M : NormModel n)565 (J : Type u) [Fintype J] :566 IsCompact (satelliteRowsSet M J) := by567 have heq : satelliteRowsSet M J =568 Set.univ.pi (fun _ : J => dualRowSet M) := by569 ext sat570 simp [satelliteRowsSet, dualRowSet]571 rw [heq]572 exact isCompact_univ_pi fun _ => isCompact_dualRowSet M573574575private theorem isCompact_satelliteConfigurationSet {n : ℕ} (M : NormModel n)576 (J : Type u) [Fintype J] :577 IsCompact (satelliteConfigurationSet M J) := by578 exact (isCompact_dualFrameSet M).prod (isCompact_satelliteRowsSet M J)579580581private theorem satelliteConfigurationSet_nonempty {n : ℕ} (M : NormModel n)582 (J : Type u) :583 (satelliteConfigurationSet M J).Nonempty := by584 refine ⟨((fun _ => 0), fun _ => 0), ?_⟩585 constructor586 · intro i x587 simpa only [zero_apply, abs_zero] using (apply_nonneg M.p x)588 · intro a x589 simpa only [zero_apply, abs_zero] using (apply_nonneg M.p x)590591592def configurationPolynomial {n : ℕ} {J : Type u} [Fintype J]593 (weight : ℝ) (coeff : J → Coord n) :594 SatelliteConfiguration n J → ℝ :=595 fun C => satellitePolynomial weight coeff C.1 C.2596597598private theorem continuous_configurationPolynomial {n : ℕ} {J : Type u} [Fintype J]599 (weight : ℝ) (coeff : J → Coord n) :600 Continuous (configurationPolynomial weight coeff) := by601 change Continuous fun C : SatelliteConfiguration n J =>602 weight * frameDet C.1 +603 ∑ a : J, ∑ i : Fin n,604 coeff a i * replacementDet C.1 i (C.2 a)605 have hreplacement : ∀ (a : J) (i : Fin n),606 Continuous fun C : SatelliteConfiguration n J =>607 replacementDet C.1 i (C.2 a) := by608 intro a i609 unfold replacementDet DeterminantFrame.replacementDeterminant DeterminantFrame.frameDeterminant610 apply Continuous.matrix_det611 apply continuous_matrix612 intro k j613 simp only [DeterminantFrame.frameMatrix, Pi.basisFun_apply]614 change Continuous fun C : SatelliteConfiguration n J =>615 (replaceFrameRow C.1 i (C.2 a)) k (Pi.single j 1)616 by_cases hki : k = i617 · subst k618 simpa [replaceFrameRow, DeterminantFrame.replaceRow] using619 (show Continuous fun C : SatelliteConfiguration n J =>620 C.2 a (Pi.single j 1) by fun_prop)621 · simpa [replaceFrameRow, DeterminantFrame.replaceRow, hki] using622 (show Continuous fun C : SatelliteConfiguration n J =>623 C.1 k (Pi.single j 1) by fun_prop)624 apply Continuous.add625 · exact continuous_const.mul (continuous_frameDet.comp continuous_fst)626 · exact continuous_finsetSum Finset.univ fun a _ =>627 continuous_finsetSum Finset.univ fun i _ =>628 continuous_const.mul (hreplacement a i)629630631private theorem exists_maxSatelliteConfiguration {n : ℕ} (M : NormModel n)632 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n) :633 ∃ C ∈ satelliteConfigurationSet M J,634 ∀ D ∈ satelliteConfigurationSet M J,635 |configurationPolynomial weight coeff D| ≤636 |configurationPolynomial weight coeff C| := by637 rcases (isCompact_satelliteConfigurationSet M J).exists_isMaxOn638 (satelliteConfigurationSet_nonempty M J)639 (continuous_configurationPolynomial weight coeff).abs.continuousOn with640 ⟨C, hC, hmax⟩641 exact ⟨C, hC, hmax⟩642643644noncomputable def maxSatelliteConfiguration {n : ℕ} (M : NormModel n)645 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n) :646 SatelliteConfiguration n J :=647 Classical.choose (exists_maxSatelliteConfiguration M J weight coeff)648649650private theorem Internal.maxSatelliteConfiguration_mem {n : ℕ} (M : NormModel n)651 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n) :652 maxSatelliteConfiguration M J weight coeff ∈653 satelliteConfigurationSet M J :=654 (Classical.choose_spec655 (exists_maxSatelliteConfiguration M J weight coeff)).1656657658private theorem Internal.abs_configurationPolynomial_le_max {n : ℕ} (M : NormModel n)659 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n)660 {C : SatelliteConfiguration n J}661 (hC : C ∈ satelliteConfigurationSet M J) :662 |configurationPolynomial weight coeff C| ≤663 |configurationPolynomial weight coeff664 (maxSatelliteConfiguration M J weight coeff)| :=665 (Classical.choose_spec666 (exists_maxSatelliteConfiguration M J weight coeff)).2 C hC667668669@[simp] private theorem replacementDet_zero {n : ℕ} (B : DualFrame n) (i : Fin n) :670 replacementDet B i (0 : Coord n →L[ℝ] ℝ) = 0 := by671 change Matrix.det (dualFrameMatrix (replaceFrameRow B i 0)) = 0672 rw [dualFrameMatrix_replaceFrameRow]673 apply Matrix.det_eq_zero_of_row_eq_zero i674 intro j675 simp [functionalRow, DeterminantFrame.functionalCoordinates]676677678private noncomputable def Internal.benchmarkConfiguration {n : ℕ} (M : NormModel n)679 (J : Type u) : SatelliteConfiguration n J :=680 (maxFrame M, fun _ => 0)681682683private theorem Internal.benchmarkConfiguration_mem {n : ℕ} (M : NormModel n)684 (J : Type u) :685 benchmarkConfiguration M J ∈ satelliteConfigurationSet M J := by686 constructor687 · exact maxFrame_mem M688 · intro a x689 simpa only [benchmarkConfiguration, zero_apply, abs_zero] using690 (apply_nonneg M.p x)691692693private theorem Internal.abs_configurationPolynomial_benchmark {n : ℕ} (M : NormModel n)694 (J : Type u) [Fintype J] {weight : ℝ} (hweight : 0 ≤ weight)695 (coeff : J → Coord n) :696 |configurationPolynomial weight coeff (benchmarkConfiguration M J)| =697 weight * detMax M := by698 simp [configurationPolynomial, benchmarkConfiguration, satellitePolynomial,699 abs_mul, abs_of_nonneg hweight, maxFrame_det]700701702private theorem Internal.benchmark_le_maxSatelliteConfiguration {n : ℕ} (M : NormModel n)703 (J : Type u) [Fintype J] {weight : ℝ} (hweight : 0 ≤ weight)704 (coeff : J → Coord n) :705 weight * detMax M ≤706 |configurationPolynomial weight coeff707 (maxSatelliteConfiguration M J weight coeff)| := by708 rw [← abs_configurationPolynomial_benchmark M J hweight coeff]709 exact abs_configurationPolynomial_le_max M J weight coeff710 (benchmarkConfiguration_mem M J)711712713theorem absoluteMaximizer_base_nearMax {n : ℕ} {J : Type u}714 [Fintype J] (M : NormModel n) {η weight : ℝ}715 (hη0 : 0 ≤ η) (hweight : 0 < weight)716 (coeff : J → Coord n)717 (hgap : satelliteBudget M coeff < weight * η)718 {C : SatelliteConfiguration n J}719 (hC : C ∈ satelliteConfigurationSet M J)720 (hmax : ∀ D ∈ satelliteConfigurationSet M J,721 |configurationPolynomial weight coeff D| ≤722 |configurationPolynomial weight coeff C|) :723 C.1 ∈ nearMaxFrames M η := by724 apply base_mem_nearMax_of_benchmark_le M hη0 hweight coeff hC.1 C.2 hC.2 hgap725 calc726 weight * detMax M =727 |configurationPolynomial weight coeff (benchmarkConfiguration M J)| := by728 symm729 exact abs_configurationPolynomial_benchmark M J hweight.le coeff730 _ ≤ |configurationPolynomial weight coeff C| :=731 hmax (benchmarkConfiguration M J) (benchmarkConfiguration_mem M J)732 _ = |satellitePolynomial weight coeff C.1 C.2| := rfl733734735private theorem maxSatelliteConfiguration_base_nearMax {n : ℕ} {J : Type u}736 [Fintype J] (M : NormModel n) {η weight : ℝ}737 (hη0 : 0 ≤ η) (hweight : 0 < weight)738 (coeff : J → Coord n)739 (hgap : satelliteBudget M coeff < weight * η) :740 (maxSatelliteConfiguration M J weight coeff).1 ∈741 nearMaxFrames M η := by742 let C := maxSatelliteConfiguration M J weight coeff743 have hC : C ∈ satelliteConfigurationSet M J := by744 exact maxSatelliteConfiguration_mem M J weight coeff745 apply base_mem_nearMax_of_benchmark_le M hη0 hweight coeff hC.1 C.2 hC.2 hgap746 simpa [configurationPolynomial, C] using747 benchmark_le_maxSatelliteConfiguration M J hweight.le coeff748749750private theorem Internal.abs_add_eq_add_abs_of_mul_nonneg {a b : ℝ} (h : 0 ≤ a * b) :751 |a + b| = |a| + |b| := by752 rcases mul_nonneg_iff.mp h with hab | hab753 · rw [abs_of_nonneg hab.1, abs_of_nonneg hab.2,754 abs_of_nonneg (add_nonneg hab.1 hab.2)]755 · rw [abs_of_nonpos hab.1, abs_of_nonpos hab.2,756 abs_of_nonpos (add_nonpos hab.1 hab.2)]757 ring758759760private theorem Internal.abs_add_or_abs_sub_eq_add_abs (a b : ℝ) :761 |a + b| = |a| + |b| ∨ |a - b| = |a| + |b| := by762 by_cases h : 0 ≤ a * b763 · exact Or.inl (abs_add_eq_add_abs_of_mul_nonneg h)764 · right765 have hneg : 0 ≤ a * (-b) := by nlinarith766 simpa [sub_eq_add_neg, abs_neg] using767 (abs_add_eq_add_abs_of_mul_nonneg hneg)768769770theorem abs_affine_endpoint_rigidity771 {R d u p : ℝ} (hp : 0 ≤ p) (hu : |u| ≤ p) (hd : d ≠ 0)772 (hplus : |R + d * p| ≤ |R + d * u|)773 (hminus : |R - d * p| ≤ |R + d * u|) :774 |u| = p := by775 have hend : |R| + |d| * p ≤ |R + d * u| := by776 rcases abs_add_or_abs_sub_eq_add_abs R (d * p) with h | h777 · calc778 |R| + |d| * p = |R| + |d * p| := by779 rw [abs_mul, abs_of_nonneg hp]780 _ = |R + d * p| := h.symm781 _ ≤ |R + d * u| := hplus782 · calc783 |R| + |d| * p = |R| + |d * p| := by784 rw [abs_mul, abs_of_nonneg hp]785 _ = |R - d * p| := h.symm786 _ ≤ |R + d * u| := hminus787 have htri : |R + d * u| ≤ |R| + |d| * |u| := by788 calc789 |R + d * u| ≤ |R| + |d * u| := abs_add_le _ _790 _ = |R| + |d| * |u| := by rw [abs_mul]791 have hmul : |d| * p ≤ |d| * |u| := by792 linarith793 have hp_le : p ≤ |u| := by794 nlinarith [abs_pos.mpr hd]795 exact le_antisymm hu hp_le796797798private def Internal.satelliteRowContribution {n : ℕ} {J : Type u} [Fintype J]799 (coeff : J → Coord n) (B : DualFrame n)800 (sat : J → (Coord n →L[ℝ] ℝ)) (a : J) : ℝ :=801 ∑ i : Fin n, coeff a i * replacementDet B i (sat a)802803804private def Internal.satelliteRemainder {n : ℕ} {J : Type u} [Fintype J] [DecidableEq J]805 (weight : ℝ) (coeff : J → Coord n)806 (C : SatelliteConfiguration n J) (a : J) : ℝ :=807 weight * frameDet C.1 +808 Finset.sum (Finset.univ.erase a) (fun b =>809 satelliteRowContribution coeff C.1 C.2 b)810811812private theorem Internal.configurationPolynomial_eq_remainder_add {n : ℕ}813 {J : Type u} [Fintype J] [DecidableEq J]814 (weight : ℝ) (coeff : J → Coord n)815 (C : SatelliteConfiguration n J) (a : J) :816 configurationPolynomial weight coeff C =817 satelliteRemainder weight coeff C a +818 satelliteRowContribution coeff C.1 C.2 a := by819 have hsum := Finset.add_sum_erase (Finset.univ : Finset J)820 (fun b : J => satelliteRowContribution coeff C.1 C.2 b)821 (Finset.mem_univ a)822 change weight * frameDet C.1 +823 ∑ b : J, satelliteRowContribution coeff C.1 C.2 b =824 (weight * frameDet C.1 +825 Finset.sum (Finset.univ.erase a) (fun b =>826 satelliteRowContribution coeff C.1 C.2 b)) +827 satelliteRowContribution coeff C.1 C.2 a828 rw [← hsum]829 ring830831832private theorem satelliteRowContribution_eq_det_mul_eval {n : ℕ}833 {J : Type u} [Fintype J] (coeff : J → Coord n)834 {B : DualFrame n} (hB : frameDet B ≠ 0)835 (sat : J → (Coord n →L[ℝ] ℝ)) (a : J) :836 satelliteRowContribution coeff B sat a =837 frameDet B * sat a (framePreimage B (coeff a)) := by838 exact sum_mul_replacementDet B hB (sat a) (coeff a)839840841private def Internal.updateSatelliteConfiguration {n : ℕ} {J : Type u}842 [DecidableEq J] (C : SatelliteConfiguration n J) (a : J)843 (r : Coord n →L[ℝ] ℝ) : SatelliteConfiguration n J :=844 (C.1, Function.update C.2 a r)845846847private theorem Internal.updateSatelliteConfiguration_mem {n : ℕ} {J : Type u}848 [DecidableEq J] (M : NormModel n)849 {C : SatelliteConfiguration n J}850 (hC : C ∈ satelliteConfigurationSet M J) (a : J)851 {r : Coord n →L[ℝ] ℝ} (hr : IsDualContraction M r) :852 updateSatelliteConfiguration C a r ∈ satelliteConfigurationSet M J := by853 constructor854 · exact hC.1855 · intro b856 by_cases hba : b = a857 · subst b858 simpa [updateSatelliteConfiguration] using hr859 · simpa [updateSatelliteConfiguration, hba] using hC.2 b860861862private theorem Internal.satelliteRemainder_update {n : ℕ} {J : Type u}863 [Fintype J] [DecidableEq J]864 (weight : ℝ) (coeff : J → Coord n)865 (C : SatelliteConfiguration n J) (a : J)866 (r : Coord n →L[ℝ] ℝ) :867 satelliteRemainder weight coeff868 (updateSatelliteConfiguration C a r) a =869 satelliteRemainder weight coeff C a := by870 unfold satelliteRemainder updateSatelliteConfiguration871 apply congrArg (fun t : ℝ => weight * frameDet C.1 + t)872 apply Finset.sum_congr rfl873 intro b hb874 have hba : b ≠ a := Finset.ne_of_mem_erase hb875 simp [satelliteRowContribution, hba]876877878private theorem Internal.configurationPolynomial_update_eq {n : ℕ} {J : Type u}879 [Fintype J] [DecidableEq J]880 (weight : ℝ) (coeff : J → Coord n)881 (C : SatelliteConfiguration n J) (a : J)882 (r : Coord n →L[ℝ] ℝ) (hdet : frameDet C.1 ≠ 0) :883 configurationPolynomial weight coeff884 (updateSatelliteConfiguration C a r) =885 satelliteRemainder weight coeff C a +886 frameDet C.1 * r (framePreimage C.1 (coeff a)) := by887 rw [configurationPolynomial_eq_remainder_add,888 satelliteRemainder_update]889 change satelliteRemainder weight coeff C a +890 satelliteRowContribution coeff C.1 (Function.update C.2 a r) a =891 satelliteRemainder weight coeff C a +892 frameDet C.1 * r (framePreimage C.1 (coeff a))893 rw [satelliteRowContribution_eq_det_mul_eval coeff hdet]894 simp895896897theorem absoluteMaximizer_satellite_norms_preimage {n : ℕ}898 (M : NormModel n) {J : Type u} [Fintype J] [DecidableEq J]899 {η weight : ℝ} (hηD : η < detMax M)900 (coeff : J → Coord n)901 {C : SatelliteConfiguration n J}902 (hC : C ∈ satelliteConfigurationSet M J)903 (hnear : C.1 ∈ nearMaxFrames M η)904 (hmax : ∀ D ∈ satelliteConfigurationSet M J,905 |configurationPolynomial weight coeff D| ≤906 |configurationPolynomial weight coeff C|)907 (a : J) :908 |C.2 a (framePreimage C.1 (coeff a))| =909 M.p (framePreimage C.1 (coeff a)) := by910 let z : Coord n := framePreimage C.1 (coeff a)911 let R : ℝ := satelliteRemainder weight coeff C a912 let d : ℝ := frameDet C.1913 let u : ℝ := C.2 a z914 let p : ℝ := M.p z915 have hd : d ≠ 0 := by916 simpa [d] using nearMaxFrame_det_ne_zero M hηD hnear917 have hu : |u| ≤ p := by918 simpa [u, p] using hC.2 a z919 have hp : 0 ≤ p := by920 exact apply_nonneg M.p z921 rcases exists_modelNormingEndpoints M z with922 ⟨rPlus, rMinus, hrPlus, hrMinus, hrPlusZ, hrMinusZ⟩923 have hself : updateSatelliteConfiguration C a (C.2 a) = C := by924 have hsat : Function.update C.2 a (C.2 a) = C.2 := by925 funext b926 by_cases hba : b = a927 · subst b928 simp929 · simp [hba]930 exact Prod.ext rfl hsat931 have hcurrent :932 configurationPolynomial weight coeff C = R + d * u := by933 have hformula :=934 configurationPolynomial_update_eq weight coeff C a (C.2 a) hd935 rw [hself] at hformula936 simpa [R, d, u, z] using hformula937 have hplus : |R + d * p| ≤ |R + d * u| := by938 have hm := hmax (updateSatelliteConfiguration C a rPlus)939 (updateSatelliteConfiguration_mem M hC a hrPlus)940 rw [configurationPolynomial_update_eq weight coeff C a rPlus hd,941 hcurrent] at hm942 simpa [R, d, p, z, hrPlusZ] using hm943 have hminus : |R - d * p| ≤ |R + d * u| := by944 have hm := hmax (updateSatelliteConfiguration C a rMinus)945 (updateSatelliteConfiguration_mem M hC a hrMinus)946 rw [configurationPolynomial_update_eq weight coeff C a rMinus hd,947 hcurrent] at hm948 simpa [R, d, p, z, hrMinusZ, sub_eq_add_neg] using hm949 simpa [u, p, z] using950 abs_affine_endpoint_rigidity hp hu hd hplus hminus951952953def CoefficientDetectsUnit {n : ℕ} (M : NormModel n) {J : Type u}954 (η : ℝ) (H : NearMaxInverseBound M η) (ρ : ℝ)955 (coeff : J → Coord n) : Prop :=956 ∀ ⦃B : DualFrame n⦄, B ∈ nearMaxFrames M η →957 ∀ ⦃x : Coord n⦄, M.p x = 1 →958 ∃ a : J, M.p (x - framePreimage B (coeff a)) ≤ H.boundConstant * ρ959960961private theorem Internal.model_sub_error_le_model {n : ℕ} (M : NormModel n)962 (x z : Coord n) :963 M.p x - M.p (x - z) ≤ M.p z := by964 have h := map_add_le_add M.p (x - z) z965 have hx : (x - z) + z = x := sub_add_cancel x z966 rw [hx] at h967 linarith968969970theorem abs_eval_lower_of_norms_nearby {n : ℕ} (M : NormModel n)971 {r : Coord n →L[ℝ] ℝ} (hr : IsDualContraction M r)972 {x z : Coord n} (hx : M.p x = 1)973 {δ : ℝ} (hδ : M.p (x - z) ≤ δ)974 (hnorm : |r z| = M.p z) :975 1 - 2 * δ ≤ |r x| := by976 have hpz : 1 - δ ≤ M.p z := by977 have := model_sub_error_le_model M x z978 rw [hx] at this979 linarith980 have hdiff : |r (x - z)| ≤ δ := (hr (x - z)).trans hδ981 have hlin : r z = r x - r (x - z) := by982 have hmap := r.map_sub x z983 linarith984 have hz_le : |r z| ≤ |r x| + δ := by985 calc986 |r z| = |r x - r (x - z)| := by rw [hlin]987 _ ≤ |r x| + |r (x - z)| := abs_sub _ _988 _ ≤ |r x| + δ := add_le_add le_rfl hdiff989 rw [hnorm] at hz_le990 linarith991992993theorem absoluteMaximizer_satellites_almost_norm {n : ℕ}994 (M : NormModel n) {J : Type u} [Fintype J] [DecidableEq J]995 {η weight ρ : ℝ} (hηD : η < detMax M)996 (H : NearMaxInverseBound M η) (coeff : J → Coord n)997 (hdetect : CoefficientDetectsUnit M η H ρ coeff)998 {C : SatelliteConfiguration n J}999 (hC : C ∈ satelliteConfigurationSet M J)1000 (hnear : C.1 ∈ nearMaxFrames M η)1001 (hmax : ∀ D ∈ satelliteConfigurationSet M J,1002 |configurationPolynomial weight coeff D| ≤1003 |configurationPolynomial weight coeff C|)1004 {x : Coord n} (hx : M.p x = 1) :1005 ∃ a : J, 1 - 2 * (H.boundConstant * ρ) ≤ |C.2 a x| := by1006 rcases hdetect hnear hx with ⟨a, ha⟩1007 refine ⟨a, ?_⟩1008 let z : Coord n := framePreimage C.1 (coeff a)1009 have hnorm : |C.2 a z| = M.p z := by1010 simpa [z] using absoluteMaximizer_satellite_norms_preimage1011 M hηD coeff hC hnear hmax a1012 exact abs_eval_lower_of_norms_nearby M (hC.2 a) hx ha hnorm101310141015theorem absoluteMaximizer_satellites_one_sub_epsilon {n : ℕ}1016 (M : NormModel n) {J : Type u} [Fintype J] [DecidableEq J]1017 {η weight ε : ℝ} (hηD : η < detMax M) (hε : 0 < ε)1018 (H : NearMaxInverseBound M η) (coeff : J → Coord n)1019 (hdetect : CoefficientDetectsUnit M η H (satelliteRadius ε H.boundConstant) coeff)1020 {C : SatelliteConfiguration n J}1021 (hC : C ∈ satelliteConfigurationSet M J)1022 (hnear : C.1 ∈ nearMaxFrames M η)1023 (hmax : ∀ D ∈ satelliteConfigurationSet M J,1024 |configurationPolynomial weight coeff D| ≤1025 |configurationPolynomial weight coeff C|)1026 {x : Coord n} (hx : M.p x = 1) :1027 ∃ a : J, 1 - ε < |C.2 a x| := by1028 rcases absoluteMaximizer_satellites_almost_norm M hηD H coeff hdetect1029 hC hnear hmax hx with ⟨a, ha⟩1030 refine ⟨a, lt_of_lt_of_le ?_ ha⟩1031 have hr := two_mul_bound_mul_satelliteRadius_lt_half hε H.boundConstant_pos1032 nlinarith103310341035theorem finiteCoefficientNet_detectsUnit {n : ℕ} (M : NormModel n)1036 {η : ℝ} (hηD : η < detMax M) (H : NearMaxInverseBound M η)1037 {ρ : ℝ≥0} (C : FiniteCoefficientNet (n := n) H.boundConstant ρ) :1038 CoefficientDetectsUnit M η H (ρ : ℝ) (Internal.centerValue C) := by1039 intro B hB x hx1040 rcases exists_net_preimage_close M hηD H C hB hx with1041 ⟨c, hc, hclose⟩1042 exact ⟨⟨c, hc⟩, by simpa [Internal.centerValue] using hclose⟩104310441045theorem finiteNet_absoluteMaximizer_satellites_one_sub_epsilon1046 {n : ℕ} (M : NormModel n) {η ε weight : ℝ}1047 (hη0 : 0 ≤ η) (hηD : η < detMax M) (hε : 0 < ε)1048 (H : NearMaxInverseBound M η)1049 (Cnet : FiniteCoefficientNet (n := n) H.boundConstant1050 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))1051 (hweight : 0 < weight)1052 (hgap : satelliteBudget M (Internal.centerValue Cnet) < weight * η)1053 {Q : SatelliteConfiguration n Cnet.centers}1054 (hQ : Q ∈ satelliteConfigurationSet M Cnet.centers)1055 (hmax : ∀ D ∈ satelliteConfigurationSet M Cnet.centers,1056 |configurationPolynomial weight (Internal.centerValue Cnet) D| ≤1057 |configurationPolynomial weight (Internal.centerValue Cnet) Q|)1058 {x : Coord n} (hx : M.p x = 1) :1059 ∃ a : Cnet.centers, 1 - ε < |Q.2 a x| := by1060 have hnear : Q.1 ∈ nearMaxFrames M η :=1061 absoluteMaximizer_base_nearMax M hη0 hweight (Internal.centerValue Cnet) hgap hQ hmax1062 have hdetect : CoefficientDetectsUnit M η H1063 (satelliteRadius ε H.boundConstant) (Internal.centerValue Cnet) := by1064 simpa using finiteCoefficientNet_detectsUnit M hηD H Cnet1065 exact absoluteMaximizer_satellites_one_sub_epsilon1066 M hηD hε H (Internal.centerValue Cnet) hdetect hQ hnear hmax hx106710681069private theorem maxNetSatelliteConfiguration_satellites_one_sub_epsilon1070 {n : ℕ} (M : NormModel n) {η ε weight : ℝ}1071 (hη0 : 0 ≤ η) (hηD : η < detMax M) (hε : 0 < ε)1072 (H : NearMaxInverseBound M η)1073 (C : FiniteCoefficientNet (n := n) H.boundConstant1074 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))1075 (hweight : 0 < weight)1076 (hgap : satelliteBudget M (Internal.centerValue C) < weight * η)1077 {x : Coord n} (hx : M.p x = 1) :1078 ∃ a : C.centers,1079 1 - ε <1080 |(maxSatelliteConfiguration M C.centers weight (Internal.centerValue C)).2 a x| := by1081 let Q := maxSatelliteConfiguration M C.centers weight (Internal.centerValue C)1082 have hQ : Q ∈ satelliteConfigurationSet M C.centers := by1083 exact maxSatelliteConfiguration_mem M C.centers weight (Internal.centerValue C)1084 have hmax : ∀ D ∈ satelliteConfigurationSet M C.centers,1085 |configurationPolynomial weight (Internal.centerValue C) D| ≤1086 |configurationPolynomial weight (Internal.centerValue C) Q| := by1087 intro D hD1088 simpa [Q] using abs_configurationPolynomial_le_max1089 M C.centers weight (Internal.centerValue C) hD1090 simpa [Q] using finiteNet_absoluteMaximizer_satellites_one_sub_epsilon1091 M hη0 hηD hε H C hweight hgap hQ hmax hx109210931094theorem exists_goodNetSatelliteMaximizer1095 {n : ℕ} (M : NormModel n) {η ε : ℝ}1096 (hη : 0 < η) (hηD : η < detMax M) (hε : 0 < ε)1097 (H : NearMaxInverseBound M η)1098 (C : FiniteCoefficientNet (n := n) H.boundConstant1099 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos)) :1100 ∃ weight : ℝ,1101 0 < weight ∧1102 satelliteBudget M (Internal.centerValue C) < weight * η ∧1103 ∀ x : Coord n, M.p x = 1 →1104 ∃ a : C.centers,1105 1 - ε <1106 |(maxSatelliteConfiguration M C.centers weight (Internal.centerValue C)).2 a x| := by1107 rcases exists_weight_dominating_budget M (Internal.centerValue C) hη with1108 ⟨weight, hweight, hgap⟩1109 refine ⟨weight, hweight, hgap, ?_⟩1110 intro x hx1111 exact maxNetSatelliteConfiguration_satellites_one_sub_epsilon1112 M hη.le hηD hε H C hweight hgap hx111311141115theorem exists_goodSatellitePackage1116 {n : ℕ} (M : NormModel n) {η ε : ℝ}1117 (hη : 0 < η) (hηD : η < detMax M) (hε : 0 < ε) :1118 ∃ H : NearMaxInverseBound M η,1119 ∃ C : FiniteCoefficientNet (n := n) H.boundConstant1120 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos),1121 ∃ weight : ℝ,1122 0 < weight ∧1123 satelliteBudget M (Internal.centerValue C) < weight * η ∧1124 ∀ x : Coord n, M.p x = 1 →1125 ∃ a : C.centers,1126 1 - ε <1127 |(maxSatelliteConfiguration M C.centers1128 weight (Internal.centerValue C)).2 a x| := by1129 rcases DeterminantFrame.nonempty_nearMaxInverseBound (modelBasis M) hη.le hηD with ⟨H⟩1130 rcases nonempty_finiteCoefficientNet H.boundConstant1131 (satelliteRadiusNNReal_ne_zero hε H.boundConstant_pos) with ⟨C⟩1132 rcases exists_goodNetSatelliteMaximizer M hη hηD hε H C with1133 ⟨weight, hweight, hgap, hgood⟩1134 exact ⟨H, C, weight, hweight, hgap, hgood⟩11351136end MathlibAnnex.Satellite