Exact source: MathlibAnnex/Analysis/Normed/Operator/FiniteSup.lean
Pinned GitHub source · Raw UTF-8 source
Back to A strict lower bound on a norm's unit sphere
1import MathlibAnnex.Analysis.Normed.Dual.Satellite2import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Transport3import MathlibAnnex.LinearAlgebra.Matrix.VolumeScaledMaximalMinor45noncomputable section6set_option autoImplicit false7open Set Module8open scoped BigOperators NNReal9namespace MathlibAnnex.FiniteSup10universe u11open Satellite12private abbrev Coord (n : ℕ) := Fin n → ℝ13private abbrev NormModel (n : ℕ) := EquivalentSeminorm (Coord n)14private abbrev DualFrame (n : ℕ) := DeterminantFrame.Frame n (Coord n)15private abbrev dualFrameMatrix {n : ℕ} := DeterminantFrame.frameMatrix (Pi.basisFun ℝ (Fin n))16private abbrev frameDet {n : ℕ} := DeterminantFrame.frameDeterminant (Pi.basisFun ℝ (Fin n))17private abbrev replacementDet {n : ℕ} := DeterminantFrame.replacementDeterminant (Pi.basisFun ℝ (Fin n))18private abbrev frameCoordinates {n : ℕ} := @DeterminantFrame.frameCoordinates n (Coord n) _ _19private abbrev framePreimage {n : ℕ} (B : DualFrame n) (c : Coord n) := (dualFrameMatrix B)⁻¹.mulVec c20private abbrev IsDualContraction {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) := ∀ x, |r x| ≤ M.p x21private abbrev dualRowSet {n : ℕ} (M : NormModel n) := {r : Coord n →L[ℝ] ℝ | IsDualContraction M r}22private abbrev dualFrameSet {n : ℕ} (M : NormModel n) := {B : DualFrame n | ∀ i, IsDualContraction M (B i)}2324private instance modelFiniteDimensional {n : ℕ} (M : NormModel n) : FiniteDimensional ℝ (EquivalentSeminorm.Space M) :=25 inferInstanceAs (FiniteDimensional ℝ (Coord n))2627private def modelBasis {n : ℕ} (M : NormModel n) : Basis (Fin n) ℝ (EquivalentSeminorm.Space M) :=28 Pi.basisFun ℝ (Fin n)2930private def toModelRow {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :31 EquivalentSeminorm.Space M →L[ℝ] ℝ :=32 LinearMap.toContinuousLinearMap (show EquivalentSeminorm.Space M →ₗ[ℝ] ℝ from r.toLinearMap)3334private def fromModelRow {n : ℕ} (M : NormModel n) (r : EquivalentSeminorm.Space M →L[ℝ] ℝ) :35 Coord n →L[ℝ] ℝ :=36 LinearMap.toContinuousLinearMap (show Coord n →ₗ[ℝ] ℝ from r.toLinearMap)3738private theorem toModelRow_mem_iff {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) :39 toModelRow M r ∈ DeterminantFrame.unitRowSet (EquivalentSeminorm.Space M) ↔ IsDualContraction M r := by40 rw [DeterminantFrame.mem_unitRowSet]41 constructor42 · intro h x43 have := (toModelRow M r).le_opNorm (show EquivalentSeminorm.Space M from x)44 change |r x| ≤ ‖toModelRow M r‖ * M.p x at this45 exact this.trans (by nlinarith [apply_nonneg M.p x])46 · intro h47 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one48 intro x49 change |r (show Coord n from x)| ≤ 1 * M.p (show Coord n from x)50 simpa only [one_mul] using h (show Coord n from x)5152private abbrev detMax {n : ℕ} (M : NormModel n) := DeterminantFrame.determinantMaximum (modelBasis M)53private abbrev NearMaxInverseBound {n : ℕ} (M : NormModel n) := DeterminantFrame.NearMaxInverseBound (modelBasis M)54private abbrev nearMaxFrames {n : ℕ} (M : NormModel n) (η : ℝ) := {B : DualFrame n | B ∈ dualFrameSet M ∧ detMax M - η ≤ |frameDet B|}5556private theorem toModelFrame_mem {n : ℕ} (M : NormModel n) {B : DualFrame n} (h : B ∈ dualFrameSet M) :57 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.unitFrameSet n (EquivalentSeminorm.Space M) := by58 intro i59 exact (toModelRow_mem_iff M (B i)).mpr (h i)6061private theorem toModelFrame_near {n : ℕ} (M : NormModel n) {η : ℝ} {B : DualFrame n} (h : B ∈ nearMaxFrames M η) :62 (fun i => toModelRow M (B i)) ∈ DeterminantFrame.nearMaxFrames (modelBasis M) η :=63 ⟨toModelFrame_mem M h.1, h.2⟩6465private theorem seminorm_framePreimage_le {n : ℕ} (M : NormModel n) {η : ℝ} (H : NearMaxInverseBound M η) {B : DualFrame n}66 (h : B ∈ nearMaxFrames M η) (c : Coord n) : M.p (framePreimage B c) ≤ H.boundConstant * ‖c‖ := by67 exact H.bound (toModelFrame_near M h) c6869private theorem detMax_pos {n : ℕ} (M : NormModel n) : 0 < detMax M :=70 DeterminantFrame.determinantMaximum_pos (modelBasis M)7172private theorem nearMaxFrame_det_ne_zero {n : ℕ} (M : NormModel n) {η : ℝ}73 (hη : η < detMax M) {B : DualFrame n} (hB : B ∈ nearMaxFrames M η) : frameDet B ≠ 0 :=74 DeterminantFrame.nearMaxFrame_det_ne_zero (modelBasis M) hη (toModelFrame_near M hB)7576private theorem inverse_mulVec_frameCoordinates {n : ℕ} (M : NormModel n) {η : ℝ}77 (hη : η < detMax M) {B : DualFrame n} (hB : B ∈ nearMaxFrames M η) (x : Coord n) :78 framePreimage B (frameCoordinates B x) = x := by79 exact DeterminantFrame.inverse_mulVec_frameCoordinates (modelBasis M) hη (toModelFrame_near M hB) (show EquivalentSeminorm.Space M from x)8081private theorem abs_replacementDet_le_detMax {n : ℕ} (M : NormModel n) {B : DualFrame n} (hB : B ∈ dualFrameSet M)82 (i : Fin n) {r : Coord n →L[ℝ] ℝ} (hr : IsDualContraction M r) : |replacementDet B i r| ≤ detMax M := by83 have h := DeterminantFrame.abs_replacementDeterminant_le_maximum (modelBasis M) (toModelFrame_mem M hB) i ((toModelRow_mem_iff M r).mpr hr)84 have heq : (fun j => toModelRow M ((DeterminantFrame.replaceRow B i r) j)) =85 DeterminantFrame.replaceRow (fun j => toModelRow M (B j)) i (toModelRow M r) := by86 funext j87 by_cases hj : j = i <;> simp [DeterminantFrame.replaceRow, hj]88 change |DeterminantFrame.frameDeterminant (modelBasis M)89 (fun j => toModelRow M ((DeterminantFrame.replaceRow B i r) j))| ≤ detMax M90 rw [heq]91 exact h9293private def maxFrame {n : ℕ} (M : NormModel n) : DualFrame n :=94 fun i => fromModelRow M (DeterminantFrame.maximizingFrame (modelBasis M) i)9596private theorem maxFrame_det {n : ℕ} (M : NormModel n) : |frameDet (maxFrame M)| = detMax M := rfl9798private theorem maxFrame_mem {n : ℕ} (M : NormModel n) : maxFrame M ∈ dualFrameSet M := by99 intro i100 apply (toModelRow_mem_iff M _).mp101 have h := DeterminantFrame.maximizingFrame_mem (modelBasis M) i102 convert h using 1103 ext x104 rfl105106107private abbrev replaceFrameRow {n : ℕ} := @DeterminantFrame.replaceRow n (Coord n) _ _108private abbrev functionalRow {n : ℕ} := DeterminantFrame.functionalCoordinates (Pi.basisFun ℝ (Fin n))109private theorem continuous_frameDet {n : ℕ} : Continuous (frameDet : DualFrame n → ℝ) :=110 DeterminantFrame.continuous_frameDeterminant (Pi.basisFun ℝ (Fin n))111private theorem dualFrameMatrix_replaceFrameRow {n : ℕ} (B : DualFrame n) (i : Fin n) (r : Coord n →L[ℝ] ℝ) :112 dualFrameMatrix (replaceFrameRow B i r) = (dualFrameMatrix B).updateRow i (functionalRow r) :=113 DeterminantFrame.frameMatrix_replaceRow (Pi.basisFun ℝ (Fin n)) B i r114private theorem sum_mul_replacementDet {n : ℕ} (B : DualFrame n) (hB : frameDet B ≠ 0) (r : Coord n →L[ℝ] ℝ) (c : Coord n) :115 (∑ i : Fin n, c i * replacementDet B i r) = frameDet B * r (framePreimage B c) :=116 DeterminantFrame.sum_mul_replacementDeterminant (Pi.basisFun ℝ (Fin n)) B hB r c117118private theorem isCompact_dualRowSet {n : ℕ} (M : NormModel n) : IsCompact (dualRowSet M) := by119 have hc : IsClosed (dualRowSet M) := by120 have heq : dualRowSet M = (⋂ x : Coord n, {r : Coord n →L[ℝ] ℝ | |r x| ≤ M.p x}) := by ext r; simp [dualRowSet, IsDualContraction]121 rw [heq]122 exact isClosed_iInter fun x => isClosed_le (by fun_prop) continuous_const123 have hb : Bornology.IsBounded (dualRowSet M) := by124 apply (Metric.isBounded_iff_subset_closedBall (0 : Coord n →L[ℝ] ℝ)).2125 refine ⟨M.upper, ?_⟩126 intro r hr127 rw [Metric.mem_closedBall, dist_zero_right]128 apply ContinuousLinearMap.opNorm_le_bound _ M.upper_pos.le129 intro x130 exact (hr x).trans (M.le_upper x)131 exact Metric.isCompact_of_isClosed_isBounded hc hb132133private theorem isCompact_dualFrameSet {n : ℕ} (M : NormModel n) : IsCompact (dualFrameSet M) := by134 have heq : dualFrameSet M = Set.univ.pi (fun _ : Fin n => dualRowSet M) := by ext B; simp [dualFrameSet, dualRowSet]135 rw [heq]136 exact isCompact_univ_pi fun _ => isCompact_dualRowSet M137138139private abbrev SupCoord (n : ℕ) := Fin n → ℝ140141variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}142private noncomputable instance centerFintype (C : FiniteCoefficientNet (n := n) K ρ) :143 Fintype C.centers :=144 C.finite_centers.fintype145146147148variable {n : ℕ} {K : ℝ} {ρ : ℝ≥0}149private def centerValue (C : FiniteCoefficientNet (n := n) K ρ) (c : C.centers) :150 Coord n := c.1151152private def satelliteRadius (ε K : ℝ) : ℝ := min ε 1 / (8 * K)153154private theorem satelliteRadius_pos {ε K : ℝ} (hε : 0 < ε) (hK : 0 < K) :155 0 < satelliteRadius ε K := by156 exact div_pos (lt_min hε zero_lt_one) (mul_pos (by norm_num) hK)157158private theorem two_mul_bound_mul_satelliteRadius_lt_half {ε K : ℝ}159 (hε : 0 < ε) (hK : 0 < K) :160 2 * K * satelliteRadius ε K < ε / 2 := by161 have hden : 0 < 8 * K := mul_pos (by norm_num) hK162 have hmin : min ε 1 ≤ ε := min_le_left _ _163 unfold satelliteRadius164 calc165 2 * K * (min ε 1 / (8 * K)) = min ε 1 / 4 := by field_simp; ring166 _ ≤ ε / 4 := by linarith167 _ < ε / 2 := by linarith168169private theorem satelliteRadius_lt_half_inv {ε K : ℝ}170 (_hε : 0 < ε) (hK : 0 < K) :171 satelliteRadius ε K < 1 / (2 * K) := by172 have hmin : min ε 1 ≤ 1 := min_le_right _ _173 unfold satelliteRadius174 have hK2 : 0 < 2 * K := mul_pos (by norm_num) hK175 have hK8 : 0 < 8 * K := mul_pos (by norm_num) hK176 calc177 min ε 1 / (8 * K) ≤ 1 / (8 * K) :=178 div_le_div_of_nonneg_right hmin hK8.le179 _ < 1 / (2 * K) := by180 apply one_div_lt_one_div_of_lt hK2181 nlinarith182183private noncomputable def satelliteRadiusNNReal (ε K : ℝ) (hε : 0 < ε) (hK : 0 < K) :184 ℝ≥0 :=185 ⟨satelliteRadius ε K, (satelliteRadius_pos hε hK).le⟩186187@[simp] private theorem coe_satelliteRadiusNNReal (ε K : ℝ) (hε : 0 < ε) (hK : 0 < K) :188 (satelliteRadiusNNReal ε K hε hK : ℝ) = satelliteRadius ε K := rfl189190private theorem satelliteRadiusNNReal_ne_zero {ε K : ℝ} (hε : 0 < ε) (hK : 0 < K) :191 satelliteRadiusNNReal ε K hε hK ≠ 0 := by192 exact ne_of_gt (by193 change 0 < satelliteRadius ε K194 exact satelliteRadius_pos hε hK)195196private theorem isCompact_satelliteRowsSet {n : ℕ} (M : NormModel n)197 (J : Type u) [Fintype J] :198 IsCompact (satelliteRowsSet M J) := by199 have heq : satelliteRowsSet M J =200 Set.univ.pi (fun _ : J => dualRowSet M) := by201 ext sat202 simp [satelliteRowsSet, dualRowSet]203 rw [heq]204 exact isCompact_univ_pi fun _ => isCompact_dualRowSet M205206private theorem isCompact_satelliteConfigurationSet {n : ℕ} (M : NormModel n)207 (J : Type u) [Fintype J] :208 IsCompact (satelliteConfigurationSet M J) := by209 exact (isCompact_dualFrameSet M).prod (isCompact_satelliteRowsSet M J)210211private theorem satelliteConfigurationSet_nonempty {n : ℕ} (M : NormModel n)212 (J : Type u) :213 (satelliteConfigurationSet M J).Nonempty := by214 refine ⟨((fun _ => 0), fun _ => 0), ?_⟩215 constructor216 · intro i x217 simpa only [zero_apply, abs_zero] using (apply_nonneg M.p x)218 · intro a x219 simpa only [zero_apply, abs_zero] using (apply_nonneg M.p x)220221private theorem continuous_configurationPolynomial {n : ℕ} {J : Type u} [Fintype J]222 (weight : ℝ) (coeff : J → Coord n) :223 Continuous (configurationPolynomial weight coeff) := by224 change Continuous fun C : SatelliteConfiguration n J =>225 weight * frameDet C.1 +226 ∑ a : J, ∑ i : Fin n,227 coeff a i * replacementDet C.1 i (C.2 a)228 have hreplacement : ∀ (a : J) (i : Fin n),229 Continuous fun C : SatelliteConfiguration n J =>230 replacementDet C.1 i (C.2 a) := by231 intro a i232 unfold replacementDet DeterminantFrame.replacementDeterminant DeterminantFrame.frameDeterminant233 apply Continuous.matrix_det234 apply continuous_matrix235 intro k j236 simp only [DeterminantFrame.frameMatrix, Pi.basisFun_apply]237 change Continuous fun C : SatelliteConfiguration n J =>238 (replaceFrameRow C.1 i (C.2 a)) k (Pi.single j 1)239 by_cases hki : k = i240 · subst k241 simpa [replaceFrameRow, DeterminantFrame.replaceRow] using242 (show Continuous fun C : SatelliteConfiguration n J =>243 C.2 a (Pi.single j 1) by fun_prop)244 · simpa [replaceFrameRow, DeterminantFrame.replaceRow, hki] using245 (show Continuous fun C : SatelliteConfiguration n J =>246 C.1 k (Pi.single j 1) by fun_prop)247 apply Continuous.add248 · exact continuous_const.mul (continuous_frameDet.comp continuous_fst)249 · exact continuous_finsetSum Finset.univ fun a _ =>250 continuous_finsetSum Finset.univ fun i _ =>251 continuous_const.mul (hreplacement a i)252253private theorem exists_maxSatelliteConfiguration {n : ℕ} (M : NormModel n)254 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n) :255 ∃ C ∈ satelliteConfigurationSet M J,256 ∀ D ∈ satelliteConfigurationSet M J,257 |configurationPolynomial weight coeff D| ≤258 |configurationPolynomial weight coeff C| := by259 rcases (isCompact_satelliteConfigurationSet M J).exists_isMaxOn260 (satelliteConfigurationSet_nonempty M J)261 (continuous_configurationPolynomial weight coeff).abs.continuousOn with262 ⟨C, hC, hmax⟩263 exact ⟨C, hC, hmax⟩264265private theorem maxSatelliteConfiguration_mem {n : ℕ} (M : NormModel n)266 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n) :267 maxSatelliteConfiguration M J weight coeff ∈268 satelliteConfigurationSet M J :=269 (Classical.choose_spec270 (exists_maxSatelliteConfiguration M J weight coeff)).1271272private theorem abs_configurationPolynomial_le_max {n : ℕ} (M : NormModel n)273 (J : Type u) [Fintype J] (weight : ℝ) (coeff : J → Coord n)274 {C : SatelliteConfiguration n J}275 (hC : C ∈ satelliteConfigurationSet M J) :276 |configurationPolynomial weight coeff C| ≤277 |configurationPolynomial weight coeff278 (maxSatelliteConfiguration M J weight coeff)| :=279 (Classical.choose_spec280 (exists_maxSatelliteConfiguration M J weight coeff)).2 C hC281282private theorem maxNetSatelliteConfiguration_satellites_one_sub_epsilon283 {n : ℕ} (M : NormModel n) {η ε weight : ℝ}284 (hη0 : 0 ≤ η) (hηD : η < detMax M) (hε : 0 < ε)285 (H : NearMaxInverseBound M η)286 (C : FiniteCoefficientNet (n := n) H.boundConstant287 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))288 (hweight : 0 < weight)289 (hgap : satelliteBudget M (centerValue C) < weight * η)290 {x : Coord n} (hx : M.p x = 1) :291 ∃ a : C.centers,292 1 - ε <293 |(maxSatelliteConfiguration M C.centers weight (centerValue C)).2 a x| := by294 let Q := maxSatelliteConfiguration M C.centers weight (centerValue C)295 have hQ : Q ∈ satelliteConfigurationSet M C.centers := by296 exact maxSatelliteConfiguration_mem M C.centers weight (centerValue C)297 have hmax : ∀ D ∈ satelliteConfigurationSet M C.centers,298 |configurationPolynomial weight (centerValue C) D| ≤299 |configurationPolynomial weight (centerValue C) Q| := by300 intro D hD301 simpa [Q] using abs_configurationPolynomial_le_max302 M C.centers weight (centerValue C) hD303 simpa [Q] using finiteNet_absoluteMaximizer_satellites_one_sub_epsilon304 M hη0 hηD hε H C hweight hgap hQ hmax hx305306universe v307namespace Internal308end Internal309namespace Bridge310end Bridge311open Internal Bridge312313private noncomputable def finiteRowEquiv (n : ℕ) (J : Type u) [Fintype J] :314 Sum (Fin n) J ≃ Fin (n + Fintype.card J) :=315 (Equiv.sumCongr (Equiv.refl (Fin n)) (Fintype.equivFin J)).trans316 finSumFinEquiv317318@[simp] private theorem finiteRowEquiv_inl (n : ℕ) (J : Type u) [Fintype J]319 (i : Fin n) :320 finiteRowEquiv n J (Sum.inl i) = Fin.castAdd (Fintype.card J) i := by321 simp [finiteRowEquiv]322323@[simp] private theorem finiteRowEquiv_inr (n : ℕ) (J : Type u) [Fintype J]324 (a : J) :325 finiteRowEquiv n J (Sum.inr a) =326 Fin.natAdd n (Fintype.equivFin J a) := by327 simp [finiteRowEquiv]328329@[simp] private theorem finiteRowEquiv_symm_castAdd (n : ℕ) (J : Type u)330 [Fintype J] (i : Fin n) :331 (finiteRowEquiv n J).symm (Fin.castAdd (Fintype.card J) i) =332 Sum.inl i := by333 apply (finiteRowEquiv n J).injective334 simp only [Equiv.apply_symm_apply, finiteRowEquiv_inl]335336@[simp] private theorem finiteRowEquiv_symm_natAdd (n : ℕ) (J : Type u)337 [Fintype J] (a : J) :338 (finiteRowEquiv n J).symm339 (Fin.natAdd n (Fintype.equivFin J a)) = Sum.inr a := by340 apply (finiteRowEquiv n J).injective341 simp only [Equiv.apply_symm_apply, finiteRowEquiv_inr]342343private noncomputable def reindexPiCLM {ι : Type u} {κ : Type v}344 [Fintype ι] [Fintype κ] (e : ι ≃ κ) :345 (ι → ℝ) →L[ℝ] (κ → ℝ) :=346 ContinuousLinearMap.pi fun k => ContinuousLinearMap.proj (e.symm k)347348@[simp] private theorem reindexPiCLM_apply {ι : Type u} {κ : Type v}349 [Fintype ι] [Fintype κ] (e : ι ≃ κ) (x : ι → ℝ) (k : κ) :350 reindexPiCLM e x k = x (e.symm k) := rfl351352private theorem norm_reindexPiCLM {ι : Type u} {κ : Type v}353 [Fintype ι] [Fintype κ] (e : ι ≃ κ) (x : ι → ℝ) :354 ‖reindexPiCLM e x‖ = ‖x‖ := by355 apply le_antisymm356 · apply (pi_norm_le_iff_of_nonneg (norm_nonneg x)).2357 intro k358 simpa only [reindexPiCLM_apply] using359 norm_le_pi_norm x (e.symm k)360 · apply (pi_norm_le_iff_of_nonneg361 (norm_nonneg (reindexPiCLM e x))).2362 intro i363 simpa only [reindexPiCLM_apply, Equiv.symm_apply_apply] using364 norm_le_pi_norm (reindexPiCLM e x) (e i)365366private def Internal.configurationRow {n : ℕ} {J : Type u}367 (C : SatelliteConfiguration n J) :368 Sum (Fin n) J → (Coord n →L[ℝ] ℝ)369 | Sum.inl i => C.1 i370 | Sum.inr a => C.2 a371372noncomputable def configurationMap {n : ℕ} {J : Type u} [Fintype J]373 (C : SatelliteConfiguration n J) :374 Coord n →L[ℝ] (Sum (Fin n) J → ℝ) :=375 ContinuousLinearMap.pi (configurationRow C)376377@[simp] private theorem Internal.configurationMap_apply {n : ℕ} {J : Type u} [Fintype J]378 (C : SatelliteConfiguration n J) (x : Coord n)379 (k : Sum (Fin n) J) :380 configurationMap C x k = configurationRow C k x := rfl381382theorem configurationMap_norm_le_model {n : ℕ} {J : Type u} [Fintype J]383 (M : NormModel n) {C : SatelliteConfiguration n J}384 (hC : C ∈ satelliteConfigurationSet M J) (x : Coord n) :385 ‖configurationMap C x‖ ≤ M.p x := by386 apply (pi_norm_le_iff_of_nonneg (apply_nonneg M.p x)).2387 intro k388 cases k with389 | inl i =>390 simpa [configurationMap, configurationRow, Real.norm_eq_abs] using hC.1 i x391 | inr a =>392 simpa [configurationMap, configurationRow, Real.norm_eq_abs] using hC.2 a x393394theorem configurationMap_norm_gt_of_satellite {n : ℕ} {J : Type u}395 [Fintype J] (C : SatelliteConfiguration n J) (x : Coord n)396 {a : J} {t : ℝ} (ha : t < |C.2 a x|) :397 t < ‖configurationMap C x‖ := by398 have hcoord : |configurationMap C x (Sum.inr a)| ≤399 ‖configurationMap C x‖ := by400 simpa [Real.norm_eq_abs] using401 norm_le_pi_norm (configurationMap C x) (Sum.inr a)402 simpa [configurationMap, configurationRow] using ha.trans_le hcoord403404private theorem Internal.maxNetConfigurationMap_unit_lower {n : ℕ}405 (M : NormModel n) {η ε weight : ℝ}406 (hη0 : 0 ≤ η) (hηD : η < detMax M) (hε : 0 < ε)407 (H : NearMaxInverseBound M η)408 (Cnet : FiniteCoefficientNet (n := n) H.boundConstant409 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))410 (hweight : 0 < weight)411 (hgap : satelliteBudget M (centerValue Cnet) < weight * η)412 {x : Coord n} (hx : M.p x = 1) :413 1 - ε <414 ‖configurationMap415 (maxSatelliteConfiguration M Cnet.centers weight (centerValue Cnet)) x‖ := by416 rcases maxNetSatelliteConfiguration_satellites_one_sub_epsilon417 M hη0 hηD hε H Cnet hweight hgap hx with ⟨a, ha⟩418 exact configurationMap_norm_gt_of_satellite _ _ ha419420theorem maxNetConfigurationMap_lower_of_ne_zero {n : ℕ}421 (M : NormModel n) {η ε weight : ℝ}422 (hη0 : 0 ≤ η) (hηD : η < detMax M) (hε : 0 < ε)423 (H : NearMaxInverseBound M η)424 (Cnet : FiniteCoefficientNet (n := n) H.boundConstant425 (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))426 (hweight : 0 < weight)427 (hgap : satelliteBudget M (centerValue Cnet) < weight * η)428 {x : Coord n} (hx0 : x ≠ 0) :429 (1 - ε) * M.p x <430 ‖configurationMap431 (maxSatelliteConfiguration M Cnet.centers weight (centerValue Cnet)) x‖ := by432 let t : ℝ := M.p x433 have ht : 0 < t := by434 have htnonneg : 0 ≤ t := apply_nonneg M.p x435 have htne : t ≠ 0 := by436 intro hzero437 exact hx0 (M.eq_zero_of_apply_eq_zero (by simpa [t] using hzero))438 exact lt_of_le_of_ne htnonneg (Ne.symm htne)439 let u : Coord n := t⁻¹ • x440 have hu : M.p u = 1 := by441 change M.p (t⁻¹ • x) = 1442 rw [map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.mpr ht)]443 change t⁻¹ * t = 1444 exact inv_mul_cancel₀ ht.ne' 445 have hunit := maxNetConfigurationMap_unit_lower446 M hη0 hηD hε H Cnet hweight hgap hu447 have hmap :448 configurationMap449 (maxSatelliteConfiguration M Cnet.centers weight (centerValue Cnet)) u =450 t⁻¹ • configurationMap451 (maxSatelliteConfiguration M Cnet.centers weight (centerValue Cnet)) x := by452 simp [u]453 rw [hmap, norm_smul, Real.norm_eq_abs, abs_of_pos (inv_pos.mpr ht)] at hunit454 have hunit' :455 1 - ε <456 ‖configurationMap457 (maxSatelliteConfiguration M Cnet.centers weight (centerValue Cnet)) x‖ / t := by458 simpa [div_eq_mul_inv, mul_comm] using hunit459 exact (lt_div_iff₀ ht).mp hunit' 460461abbrev Bridge.satelliteAmbientDim (n : ℕ) (J : Type u) [Fintype J] : ℕ :=462 n + Fintype.card J463464noncomputable def Bridge.configurationFinMap {n : ℕ} {J : Type u} [Fintype J]465 (C : SatelliteConfiguration n J) :466 Coord n →L[ℝ] SupCoord (satelliteAmbientDim n J) :=467 (reindexPiCLM (finiteRowEquiv n J)).comp (configurationMap C)468469@[simp] theorem Bridge.configurationFinMap_apply_base {n : ℕ} {J : Type u}470 [Fintype J] (C : SatelliteConfiguration n J) (x : Coord n) (i : Fin n) :471 configurationFinMap C x (Fin.castAdd (Fintype.card J) i) = C.1 i x := by472 simp [configurationFinMap, configurationMap, configurationRow]473474@[simp] theorem Bridge.configurationFinMap_apply_satellite {n : ℕ} {J : Type u}475 [Fintype J] (C : SatelliteConfiguration n J) (x : Coord n) (a : J) :476 configurationFinMap C x (Fin.natAdd n (Fintype.equivFin J a)) = C.2 a x := by477 simp [configurationFinMap, configurationMap, configurationRow]478479theorem Bridge.configurationFinMap_norm {n : ℕ} {J : Type u} [Fintype J]480 (C : SatelliteConfiguration n J) (x : Coord n) :481 ‖configurationFinMap C x‖ = ‖configurationMap C x‖ := by482 exact norm_reindexPiCLM (finiteRowEquiv n J) (configurationMap C x)483484theorem Bridge.configurationFinMap_norm_le_model {n : ℕ} {J : Type u}485 [Fintype J] (M : NormModel n) {C : SatelliteConfiguration n J}486 (hC : C ∈ satelliteConfigurationSet M J) (x : Coord n) :487 ‖configurationFinMap C x‖ ≤ M.p x := by488 rw [configurationFinMap_norm]489 exact configurationMap_norm_le_model M hC x490491noncomputable def Bridge.finMapBaseRow {n : ℕ} {J : Type u} [Fintype J]492 (A : Coord n →L[ℝ] SupCoord (satelliteAmbientDim n J)) (i : Fin n) :493 Coord n →L[ℝ] ℝ :=494 (ContinuousLinearMap.proj (Fin.castAdd (Fintype.card J) i)).comp A495496noncomputable def Bridge.finMapSatelliteRow {n : ℕ} {J : Type u} [Fintype J]497 (A : Coord n →L[ℝ] SupCoord (satelliteAmbientDim n J)) (a : J) :498 Coord n →L[ℝ] ℝ :=499 (ContinuousLinearMap.proj (Fin.natAdd n (Fintype.equivFin J a))).comp A500501noncomputable def Bridge.finMapConfiguration {n : ℕ} {J : Type u} [Fintype J]502 (A : Coord n →L[ℝ] SupCoord (satelliteAmbientDim n J)) :503 SatelliteConfiguration n J :=504 (finMapBaseRow A, finMapSatelliteRow A)505506@[simp] theorem Bridge.finMapConfiguration_base_apply {n : ℕ} {J : Type u}507 [Fintype J] (A : Coord n →L[ℝ] SupCoord (satelliteAmbientDim n J))508 (i : Fin n) (x : Coord n) :509 (finMapConfiguration A).1 i x =510 A x (Fin.castAdd (Fintype.card J) i) := rfl511512@[simp] theorem Bridge.finMapConfiguration_satellite_apply {n : ℕ} {J : Type u}513 [Fintype J] (A : Coord n →L[ℝ] SupCoord (satelliteAmbientDim n J))514 (a : J) (x : Coord n) :515 (finMapConfiguration A).2 a x =516 A x (Fin.natAdd n (Fintype.equivFin J a)) := rfl517518@[simp] theorem Bridge.finMapConfiguration_configurationFinMap {n : ℕ} {J : Type u}519 [Fintype J] (C : SatelliteConfiguration n J) :520 finMapConfiguration (configurationFinMap C) = C := by521 apply Prod.ext522 · funext i523 ext x524 simp [finMapConfiguration, finMapBaseRow]525 · funext a526 ext x527 simp [finMapConfiguration, finMapSatelliteRow]528529@[simp] theorem Bridge.configurationFinMap_finMapConfiguration {n : ℕ} {J : Type u}530 [Fintype J]531 (A : Coord n →L[ℝ] SupCoord (satelliteAmbientDim n J)) :532 configurationFinMap (finMapConfiguration A) = A := by533 ext x k534 obtain ⟨i | a, rfl⟩ := (finiteRowEquiv n J).surjective k535 · simp [configurationFinMap, finMapConfiguration, configurationRow]536 change A x (Fin.castAdd (Fintype.card J) i) =537 A x (Fin.castAdd (Fintype.card J) i)538 rfl539 · simp [configurationFinMap, finMapConfiguration, configurationRow]540 change A x (Fin.natAdd n (Fintype.equivFin J a)) =541 A x (Fin.natAdd n (Fintype.equivFin J a))542 rfl543544theorem Bridge.finMapConfiguration_mem {n : ℕ} {J : Type u} [Fintype J]545 (M : NormModel n)546 {A : Coord n →L[ℝ] SupCoord (satelliteAmbientDim n J)}547 (hA : M.IsContraction A) :548 finMapConfiguration A ∈ satelliteConfigurationSet M J := by549 constructor550 · intro i x551 have hcoord : |A x (Fin.castAdd (Fintype.card J) i)| ≤ ‖A x‖ := by552 simpa [Real.norm_eq_abs] using553 norm_le_pi_norm (A x) (Fin.castAdd (Fintype.card J) i)554 exact hcoord.trans (hA x)555 · intro a x556 have hcoord : |A x (Fin.natAdd n (Fintype.equivFin J a))| ≤ ‖A x‖ := by557 simpa [Real.norm_eq_abs] using558 norm_le_pi_norm (A x) (Fin.natAdd n (Fintype.equivFin J a))559 exact hcoord.trans (hA x)560561theorem Bridge.configuration_contraction_iff {n : ℕ} {J : Type u} [Fintype J]562 (M : NormModel n) (C : SatelliteConfiguration n J) :563 M.IsContraction (configurationFinMap C) ↔564 C ∈ satelliteConfigurationSet M J := by565 constructor566 · intro h567 simpa using finMapConfiguration_mem M h568 · intro h569 exact configurationFinMap_norm_le_model M h570571def FinMapAlmostIsometric {n N : ℕ} (M : NormModel n) (ε : ℝ)572 (A : Coord n →L[ℝ] SupCoord N) : Prop :=573 ∀ x : Coord n, M.p x = 1 → 1 - ε < ‖A x‖574575theorem FinMapAlmostIsometric.lower_of_ne_zero {n N : ℕ} {M : NormModel n} {ε : ℝ}576 {A : Coord n →L[ℝ] SupCoord N}577 (hA : FinMapAlmostIsometric M ε A)578 {x : Coord n} (hx : x ≠ 0) :579 (1 - ε) * M.p x < ‖A x‖ := by580 have hpx_nonneg : 0 ≤ M.p x := apply_nonneg M.p x581 have hpx_ne : M.p x ≠ 0 := by582 intro hzero583 exact hx (M.eq_zero_of_apply_eq_zero hzero)584 have hpx : 0 < M.p x := lt_of_le_of_ne hpx_nonneg (Ne.symm hpx_ne)585 let u : Coord n := (M.p x)⁻¹ • x586 have hu : M.p u = 1 := by587 rw [show u = (M.p x)⁻¹ • x by rfl, map_smul_eq_mul]588 simp only [Real.norm_eq_abs, abs_of_pos (inv_pos.mpr hpx),589 inv_mul_cancel₀ hpx.ne']590 have hlower := hA u hu591 have hnorm : ‖A u‖ = (M.p x)⁻¹ * ‖A x‖ := by592 simp [u, norm_smul]593 rw [hnorm] at hlower594 calc595 (1 - ε) * M.p x = M.p x * (1 - ε) := mul_comm _ _596 _ < M.p x * ((M.p x)⁻¹ * ‖A x‖) :=597 mul_lt_mul_of_pos_left hlower hpx598 _ = ‖A x‖ := by simp [hpx.ne']599600end MathlibAnnex.FiniteSup