Exact source: MathlibAnnex/Analysis/Normed/Dual/DeterminantFrame.lean
Pinned GitHub source · Raw UTF-8 source
Back to Positivity of the determinant maximum · Back to An attained absolute determinant maximum · Back to A common inverse estimate from row Cramer · Back to The set of near-maximal dual frames
1import MathlibAnnex.LinearAlgebra.Matrix.MaximalMinor2import Mathlib.LinearAlgebra.Matrix.NonsingularInverse3import Mathlib.Analysis.Normed.Module.FiniteDimension4import Mathlib.Topology.MetricSpace.ProperSpace5import Mathlib.Tactic67/-!8# Determinant-maximizing dual frames910This module is the R07 generalization candidate. It is deliberately stated for11an arbitrary finite-dimensional real normed space together with an explicit12basis indexed by `Fin n`. The numerical determinant maximum therefore retains13its dependence on the chosen basis.1415The proof has three parts.1617* The product of the dual unit ball is compact, so the absolute determinant has18 an attained maximum. A uniformly scaled coordinate frame belongs to that19 product and has positive determinant, including when `n = 0`.20* Replacing one row gives the row form of Cramer's identity, using Mathlib's21 `Matrix.det_smul_inv_vecMul_eq_cramer_transpose`.22* A frame whose determinant is within `η` of the maximum has an explicit common23 inverse bound. The estimate is coordinatewise and is then transported back24 through the inverse coordinate equivalence.2526The R03 read-only dependency is used only through27`MathlibAnnex.Matrix.mulVec_injective_of_maximalMinor_ne_zero`; this module does28not re-declare maximal minors or determinant perturbation bounds.2930This source preserves the dispatch statement design, with explicit basis31coordinates and the zero-dimensional boundary. Local qualification and repair32evidence are recorded separately; formal admission is outside this module.33-/3435noncomputable section3637set_option autoImplicit false3839open Set Module40open scoped BigOperators4142namespace MathlibAnnex43namespace DeterminantFrame4445universe u4647variable {n : ℕ}48variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]49 [FiniteDimensional ℝ E]5051/-- An ordered family of continuous linear functionals. -/52abbrev Frame (n : ℕ) (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] :=53 Fin n → (E →L[ℝ] ℝ)5455/-- The continuous coordinate equivalence attached to the displayed basis. -/56noncomputable def coordinateEquiv (b : Basis (Fin n) ℝ E) : E ≃L[ℝ] (Fin n → ℝ) :=57 b.equivFun.toContinuousLinearEquiv5859/-- The inverse coordinate map, named so its operator norm can appear explicitly. -/60noncomputable def inverseCoordinateMap (b : Basis (Fin n) ℝ E) :61 (Fin n → ℝ) →L[ℝ] E :=62 (coordinateEquiv b).symm.toContinuousLinearMap6364/-- Matrix of a dual frame in the displayed basis. -/65def frameMatrix (b : Basis (Fin n) ℝ E) (B : Frame n E) :66 Matrix (Fin n) (Fin n) ℝ :=67 fun i j => B i (b j)6869/-- Determinant of a dual frame in the displayed basis. -/70def frameDeterminant (b : Basis (Fin n) ℝ E) (B : Frame n E) : ℝ :=71 Matrix.det (frameMatrix b B)7273/-- Evaluation map associated to a frame. -/74def frameMap (B : Frame n E) : E →L[ℝ] (Fin n → ℝ) :=75 ContinuousLinearMap.pi fun i => B i7677/-- Coordinate vector produced by a frame. -/78def frameCoordinates (B : Frame n E) (x : E) : Fin n → ℝ :=79 fun i => B i x8081/-- A dual row belongs to the closed operator-norm unit ball. -/82def unitRowSet (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] :83 Set (E →L[ℝ] ℝ) :=84 Metric.closedBall 0 18586/-- Product of the dual operator-norm unit balls. -/87def unitFrameSet (n : ℕ) (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] :88 Set (Frame n E) :=89 {B | ∀ i, B i ∈ unitRowSet E}9091@[simp] theorem mem_unitRowSet {r : E →L[ℝ] ℝ} :92 r ∈ unitRowSet E ↔ ‖r‖ ≤ 1 := by93 simp [unitRowSet, Metric.mem_closedBall, dist_eq_norm]9495@[simp] theorem mem_unitFrameSet {B : Frame n E} :96 B ∈ unitFrameSet n E ↔ ∀ i, ‖B i‖ ≤ 1 := by97 simp [unitFrameSet]9899/-- Frame coordinates equal matrix multiplication on basis coordinates. -/100theorem frameCoordinates_eq_mulVec (b : Basis (Fin n) ℝ E)101 (B : Frame n E) (x : E) :102 frameCoordinates B x = (frameMatrix b B).mulVec (coordinateEquiv b x) := by103 funext i104 change B i x = ∑ j : Fin n, B i (b j) * coordinateEquiv b x j105 calc106 B i x = B i (∑ j : Fin n, (coordinateEquiv b x j) • b j) := by107 change B i x = B i (∑ j : Fin n, b.equivFun x j • b j)108 rw [b.sum_equivFun]109 _ = ∑ j : Fin n, B i ((coordinateEquiv b x j) • b j) := by110 rw [map_sum]111 _ = ∑ j : Fin n, B i (b j) * coordinateEquiv b x j := by112 apply Finset.sum_congr rfl113 intro j _114 simp [mul_comm]115116/-- Continuity of the frame determinant. -/117theorem continuous_frameDeterminant (b : Basis (Fin n) ℝ E) :118 Continuous (frameDeterminant b : Frame n E → ℝ) := by119 apply Continuous.matrix_det120 apply continuous_matrix121 intro i j122 change Continuous fun B : Frame n E => B i (b j)123 fun_prop124125/-- The dual unit ball is compact in finite dimension. -/126theorem isCompact_unitRowSet : IsCompact (unitRowSet E) := by127 letI : ProperSpace (E →L[ℝ] ℝ) := FiniteDimensional.proper ℝ (E →L[ℝ] ℝ)128 exact isCompact_closedBall 0 1129130/-- The frame set is a compact finite product. -/131theorem isCompact_unitFrameSet : IsCompact (unitFrameSet n E) := by132 have heq : unitFrameSet n E = Set.univ.pi (fun _ : Fin n => unitRowSet E) := by133 ext B134 simp [unitFrameSet]135 rw [heq]136 exact isCompact_univ_pi fun _ => isCompact_unitRowSet137138/-- The zero frame witnesses nonemptiness. -/139theorem unitFrameSet_nonempty : (unitFrameSet n E).Nonempty := by140 refine ⟨fun _ => 0, ?_⟩141 simp142143/-- Existence of an attained absolute determinant maximum. -/144theorem exists_maximizingFrame (b : Basis (Fin n) ℝ E) :145 ∃ B ∈ unitFrameSet n E,146 ∀ C ∈ unitFrameSet n E,147 |frameDeterminant b C| ≤ |frameDeterminant b B| := by148 rcases isCompact_unitFrameSet.exists_isMaxOn unitFrameSet_nonempty149 (continuous_frameDeterminant b).abs.continuousOn with ⟨B, hB, hmax⟩150 exact ⟨B, hB, hmax⟩151152/-- A selected maximizing frame. -/153noncomputable def maximizingFrame (b : Basis (Fin n) ℝ E) : Frame n E :=154 Classical.choose (exists_maximizingFrame b)155156/-- The selected frame lies in the product of dual unit balls. -/157theorem maximizingFrame_mem (b : Basis (Fin n) ℝ E) :158 maximizingFrame b ∈ unitFrameSet n E :=159 (Classical.choose_spec (exists_maximizingFrame b)).1160161/-- Every admissible determinant is bounded by the selected maximum. -/162theorem abs_frameDeterminant_le_maximizingFrame (b : Basis (Fin n) ℝ E)163 {B : Frame n E} (hB : B ∈ unitFrameSet n E) :164 |frameDeterminant b B| ≤ |frameDeterminant b (maximizingFrame b)| :=165 (Classical.choose_spec (exists_maximizingFrame b)).2 B hB166167/-- The attained absolute determinant maximum for the displayed basis. -/168noncomputable def determinantMaximum (b : Basis (Fin n) ℝ E) : ℝ :=169 |frameDeterminant b (maximizingFrame b)|170171/-- Raw coordinate rows, before the common contraction factor is applied. -/172noncomputable def rawCoordinateRow (b : Basis (Fin n) ℝ E) (i : Fin n) :173 E →L[ℝ] ℝ :=174 (ContinuousLinearMap.proj i).comp (coordinateEquiv b).toContinuousLinearMap175176/-- Sum of the operator norms of the coordinate rows. -/177noncomputable def coordinateRowSize (b : Basis (Fin n) ℝ E) : ℝ :=178 ∑ i : Fin n, ‖rawCoordinateRow b i‖179180/-- A positive common scaling factor placing every coordinate row in the dual unit ball. -/181noncomputable def coordinateScale (b : Basis (Fin n) ℝ E) : ℝ :=182 (1 + coordinateRowSize b)⁻¹183184/-- The coordinate-row size is nonnegative. -/185theorem coordinateRowSize_nonneg (b : Basis (Fin n) ℝ E) :186 0 ≤ coordinateRowSize b := by187 exact Finset.sum_nonneg fun i _ => norm_nonneg (rawCoordinateRow b i)188189/-- The common coordinate scaling factor is strictly positive, also for `n = 0`. -/190theorem coordinateScale_pos (b : Basis (Fin n) ℝ E) :191 0 < coordinateScale b := by192 apply inv_pos.mpr193 linarith [coordinateRowSize_nonneg b]194195/-- Each raw coordinate row is bounded by the aggregate size. -/196theorem norm_rawCoordinateRow_le_size (b : Basis (Fin n) ℝ E) (i : Fin n) :197 ‖rawCoordinateRow b i‖ ≤ coordinateRowSize b := by198 unfold coordinateRowSize199 exact Finset.single_le_sum (fun j _ => norm_nonneg (rawCoordinateRow b j))200 (Finset.mem_univ i)201202/-- Scaled coordinate row. -/203noncomputable def coordinateRow (b : Basis (Fin n) ℝ E) (i : Fin n) :204 E →L[ℝ] ℝ :=205 coordinateScale b • rawCoordinateRow b i206207/-- Explicit scaled coordinate frame. -/208noncomputable def coordinateFrame (b : Basis (Fin n) ℝ E) : Frame n E :=209 fun i => coordinateRow b i210211/-- Evaluation of a scaled coordinate row. -/212@[simp] theorem coordinateRow_apply (b : Basis (Fin n) ℝ E)213 (i : Fin n) (x : E) :214 coordinateRow b i x = coordinateScale b * coordinateEquiv b x i := by215 simp [coordinateRow, rawCoordinateRow]216217/-- Every scaled coordinate row has operator norm at most one. -/218theorem coordinateFrame_mem (b : Basis (Fin n) ℝ E) :219 coordinateFrame b ∈ unitFrameSet n E := by220 rw [mem_unitFrameSet]221 intro i222 rw [show coordinateFrame b i = coordinateScale b • rawCoordinateRow b i from rfl,223 norm_smul, Real.norm_eq_abs, abs_of_pos (coordinateScale_pos b)]224 have hden : 0 < 1 + coordinateRowSize b := by225 linarith [coordinateRowSize_nonneg b]226 have hrow := norm_rawCoordinateRow_le_size b i227 rw [coordinateScale]228 apply (inv_mul_le_one₀ hden).2229 linarith230231/-- Matrix of the explicit coordinate frame. -/232theorem frameMatrix_coordinateFrame (b : Basis (Fin n) ℝ E) :233 frameMatrix b (coordinateFrame b) =234 coordinateScale b • (1 : Matrix (Fin n) (Fin n) ℝ) := by235 ext i j236 by_cases hij : i = j237 · subst j238 simp [frameMatrix, coordinateFrame, coordinateRow_apply, coordinateEquiv]239 · simp [frameMatrix, coordinateFrame, coordinateRow_apply, coordinateEquiv, hij, Ne.symm hij]240241/-- Determinant of the explicit coordinate frame. -/242theorem frameDeterminant_coordinateFrame (b : Basis (Fin n) ℝ E) :243 frameDeterminant b (coordinateFrame b) = coordinateScale b ^ n := by244 rw [frameDeterminant, frameMatrix_coordinateFrame]245 simp246247/-- The basis-dependent determinant maximum is positive. In dimension zero,248`coordinateRowSize = 0`, the empty determinant is `1`, and the same proof applies. -/249theorem determinantMaximum_pos (b : Basis (Fin n) ℝ E) :250 0 < determinantMaximum b := by251 unfold determinantMaximum252 have hle := abs_frameDeterminant_le_maximizingFrame b (coordinateFrame_mem b)253 have hpos : 0 < |frameDeterminant b (coordinateFrame b)| := by254 rw [frameDeterminant_coordinateFrame,255 abs_of_pos (pow_pos (coordinateScale_pos b) n)]256 exact pow_pos (coordinateScale_pos b) n257 exact hpos.trans_le hle258259/-- Replace one row of a frame. -/260def replaceRow (B : Frame n E) (i : Fin n) (r : E →L[ℝ] ℝ) : Frame n E :=261 Function.update B i r262263/-- Determinant after replacing one row. -/264def replacementDeterminant (b : Basis (Fin n) ℝ E)265 (B : Frame n E) (i : Fin n) (r : E →L[ℝ] ℝ) : ℝ :=266 frameDeterminant b (replaceRow B i r)267268/-- Coordinates of one functional in the displayed basis. -/269def functionalCoordinates (b : Basis (Fin n) ℝ E) (r : E →L[ℝ] ℝ) :270 Fin n → ℝ :=271 fun j => r (b j)272273/-- Replacing a frame row is matrix row replacement. -/274@[simp] theorem frameMatrix_replaceRow (b : Basis (Fin n) ℝ E)275 (B : Frame n E) (i : Fin n) (r : E →L[ℝ] ℝ) :276 frameMatrix b (replaceRow B i r) =277 (frameMatrix b B).updateRow i (functionalCoordinates b r) := by278 ext k j279 by_cases hki : k = i280 · subst k281 simp [frameMatrix, replaceRow, functionalCoordinates]282 · simp [frameMatrix, replaceRow, hki]283284/-- A continuous linear functional is the dot product with its basis-coordinate row. -/285theorem functional_apply_eq_sum (b : Basis (Fin n) ℝ E)286 (r : E →L[ℝ] ℝ) (x : E) :287 r x = ∑ j : Fin n, functionalCoordinates b r j * coordinateEquiv b x j := by288 calc289 r x = r (∑ j : Fin n, (coordinateEquiv b x j) • b j) := by290 change r x = r (∑ j : Fin n, b.equivFun x j • b j)291 rw [b.sum_equivFun]292 _ = ∑ j : Fin n, r ((coordinateEquiv b x j) • b j) := by293 rw [map_sum]294 _ = ∑ j : Fin n, functionalCoordinates b r j * coordinateEquiv b x j := by295 apply Finset.sum_congr rfl296 intro j _297 simp [functionalCoordinates, mul_comm]298299/-- One row-replacement determinant is the matching row-Cramer coordinate. -/300theorem replacementDeterminant_eq_cramerTranspose301 (b : Basis (Fin n) ℝ E) (B : Frame n E)302 (i : Fin n) (r : E →L[ℝ] ℝ) :303 replacementDeterminant b B i r =304 Matrix.cramer (Matrix.transpose (frameMatrix b B))305 (functionalCoordinates b r) i := by306 rw [Matrix.cramer_transpose_apply]307 simp [replacementDeterminant, frameDeterminant]308309/-- Reassociation used after row Cramer. Kept private because it is a technical310matrix/coordinate bridge rather than a separate mathematical API. -/311private theorem sum_mul_vecMul_eq_functional_inv_mulVec312 (b : Basis (Fin n) ℝ E) (A : Matrix (Fin n) (Fin n) ℝ)313 (r : E →L[ℝ] ℝ) (c : Fin n → ℝ) :314 (∑ i : Fin n, c i * Matrix.vecMul (functionalCoordinates b r) A i) =315 r ((coordinateEquiv b).symm (Matrix.mulVec A c)) := by316 calc317 (∑ i : Fin n, c i * Matrix.vecMul (functionalCoordinates b r) A i) =318 dotProduct c (Matrix.vecMul (functionalCoordinates b r) A) := rfl319 _ = dotProduct (Matrix.vecMul (functionalCoordinates b r) A) c :=320 dotProduct_comm _ _321 _ = dotProduct (functionalCoordinates b r) (Matrix.mulVec A c) :=322 (Matrix.dotProduct_mulVec (functionalCoordinates b r) A c).symm323 _ = r ((coordinateEquiv b).symm (Matrix.mulVec A c)) := by324 simpa only [dotProduct, (coordinateEquiv b).apply_symm_apply] using325 (functional_apply_eq_sum b r326 ((coordinateEquiv b).symm (Matrix.mulVec A c))).symm327328/-- Exact row-replacement Cramer identity in an arbitrary displayed basis. -/329theorem sum_mul_replacementDeterminant (b : Basis (Fin n) ℝ E) (B : Frame n E)330 (hB : frameDeterminant b B ≠ 0) (r : E →L[ℝ] ℝ) (c : Fin n → ℝ) :331 (∑ i : Fin n, c i * replacementDeterminant b B i r) =332 frameDeterminant b B *333 r ((coordinateEquiv b).symm ((frameMatrix b B)⁻¹.mulVec c)) := by334 let A : Matrix (Fin n) (Fin n) ℝ := frameMatrix b B335 have hdet : A.det ≠ 0 := by simpa [A, frameDeterminant] using hB336 have hunit : IsUnit A.det := (isUnit_iff_ne_zero).2 hdet337 have hcramer :338 A.det • Matrix.vecMul (functionalCoordinates b r) (A⁻¹) =339 Matrix.cramer (Matrix.transpose A) (functionalCoordinates b r) := by340 exact Matrix.det_smul_inv_vecMul_eq_cramer_transpose341 A (functionalCoordinates b r) hunit342 calc343 (∑ i : Fin n, c i * replacementDeterminant b B i r) =344 ∑ i : Fin n,345 c i * Matrix.cramer (Matrix.transpose A) (functionalCoordinates b r) i := by346 apply Finset.sum_congr rfl347 intro i _348 exact congrArg (fun z : ℝ => c i * z) (by349 simpa [A] using replacementDeterminant_eq_cramerTranspose b B i r)350 _ = ∑ i : Fin n,351 c i * (A.det • Matrix.vecMul (functionalCoordinates b r) (A⁻¹)) i := by352 apply Finset.sum_congr rfl353 intro i _354 rw [hcramer]355 _ = A.det * ∑ i : Fin n,356 c i * Matrix.vecMul (functionalCoordinates b r) (A⁻¹) i := by357 rw [Finset.mul_sum]358 apply Finset.sum_congr rfl359 intro i _360 change c i * (A.det * Matrix.vecMul (functionalCoordinates b r) (A⁻¹) i) =361 A.det * (c i * Matrix.vecMul (functionalCoordinates b r) (A⁻¹) i)362 ring363 _ = A.det * r ((coordinateEquiv b).symm (Matrix.mulVec (A⁻¹) c)) := by364 rw [sum_mul_vecMul_eq_functional_inv_mulVec]365 _ = frameDeterminant b B *366 r ((coordinateEquiv b).symm ((frameMatrix b B)⁻¹.mulVec c)) := by367 rfl368369/-- R03 bridge: nonzero determinant gives injective coordinate matrix action.370The full square matrix is viewed as its canonical maximal minor. -/371private theorem frameMatrix_mulVec_injective_of_det_ne_zero372 (b : Basis (Fin n) ℝ E) (B : Frame n E)373 (hB : frameDeterminant b B ≠ 0) :374 Function.Injective (frameMatrix b B).mulVec := by375 let s : MathlibAnnex.Matrix.MaximalMinorIndex n (Fin n) :=376 MathlibAnnex.Matrix.MaximalMinorIndex.ofOrderEmbedding (OrderEmbedding.id (Fin n))377 apply MathlibAnnex.Matrix.mulVec_injective_of_maximalMinor_ne_zero378 (frameMatrix b B) s379 simpa [s, frameDeterminant] using hB380381/-- A nonzero frame determinant makes the frame evaluation map injective. -/382theorem frameMap_injective_of_det_ne_zero (b : Basis (Fin n) ℝ E)383 (B : Frame n E) (hB : frameDeterminant b B ≠ 0) :384 Function.Injective (frameMap B) := by385 intro x y hxy386 apply (coordinateEquiv b).injective387 apply frameMatrix_mulVec_injective_of_det_ne_zero b B hB388 change frameCoordinates B x = frameCoordinates B y at hxy389 rwa [frameCoordinates_eq_mulVec b B x, frameCoordinates_eq_mulVec b B y] at hxy390391/-- Frames whose determinant is within `η` of the attained maximum. -/392def nearMaxFrames (b : Basis (Fin n) ℝ E) (η : ℝ) : Set (Frame n E) :=393 {B | B ∈ unitFrameSet n E ∧394 determinantMaximum b - η ≤ |frameDeterminant b B|}395396/-- Near-maximal frames form a compact subset of the compact frame set. -/397theorem isCompact_nearMaxFrames (b : Basis (Fin n) ℝ E) (η : ℝ) :398 IsCompact (nearMaxFrames b η) := by399 have hclosed : IsClosed400 {B : Frame n E | determinantMaximum b - η ≤ |frameDeterminant b B|} :=401 isClosed_le continuous_const (continuous_frameDeterminant b).abs402 exact isCompact_unitFrameSet.inter_right hclosed403404/-- The selected maximizing frame belongs to every near-maximal set with405nonnegative slack. -/406theorem nearMaxFrames_nonempty (b : Basis (Fin n) ℝ E) {η : ℝ}407 (hη : 0 ≤ η) : (nearMaxFrames b η).Nonempty := by408 refine ⟨maximizingFrame b, maximizingFrame_mem b, ?_⟩409 simp only [determinantMaximum]410 linarith411412/-- Determinant lower bound carried by near-maximal membership. -/413theorem nearMaxFrame_abs_det_lower (b : Basis (Fin n) ℝ E) {η : ℝ}414 {B : Frame n E} (hB : B ∈ nearMaxFrames b η) :415 determinantMaximum b - η ≤ |frameDeterminant b B| :=416 hB.2417418/-- Positive determinant gap implies a nonzero determinant. -/419theorem nearMaxFrame_det_ne_zero (b : Basis (Fin n) ℝ E) {η : ℝ}420 (hη : η < determinantMaximum b) {B : Frame n E}421 (hB : B ∈ nearMaxFrames b η) : frameDeterminant b B ≠ 0 := by422 have hgap : 0 < determinantMaximum b - η := sub_pos.mpr hη423 have habs : 0 < |frameDeterminant b B| :=424 hgap.trans_le (nearMaxFrame_abs_det_lower b hB)425 exact abs_pos.mp habs426427/-- The determinant of a near-maximal coordinate matrix is a unit. -/428theorem isUnit_nearMaxFrame_det (b : Basis (Fin n) ℝ E) {η : ℝ}429 (hη : η < determinantMaximum b) {B : Frame n E}430 (hB : B ∈ nearMaxFrames b η) : IsUnit (frameMatrix b B).det := by431 exact isUnit_iff_ne_zero.mpr (by432 simpa [frameDeterminant] using nearMaxFrame_det_ne_zero b hη hB)433434/-- The inverse matrix and inverse coordinate equivalence reconstruct a vector. -/435theorem inverse_mulVec_frameCoordinates (b : Basis (Fin n) ℝ E) {η : ℝ}436 (hη : η < determinantMaximum b) {B : Frame n E}437 (hB : B ∈ nearMaxFrames b η) (x : E) :438 (coordinateEquiv b).symm439 ((frameMatrix b B)⁻¹.mulVec (frameCoordinates B x)) = x := by440 rw [frameCoordinates_eq_mulVec, Matrix.mulVec_mulVec]441 rw [Matrix.nonsing_inv_mul _ (isUnit_nearMaxFrame_det b hη hB)]442 rw [Matrix.one_mulVec]443 exact (coordinateEquiv b).symm_apply_apply x444445/-- Replacing one row of an admissible frame by another unit-dual row preserves446admissibility. -/447theorem replaceRow_mem_unitFrameSet {B : Frame n E}448 (hB : B ∈ unitFrameSet n E) (i : Fin n) {r : E →L[ℝ] ℝ}449 (hr : r ∈ unitRowSet E) : replaceRow B i r ∈ unitFrameSet n E := by450 intro j451 by_cases hji : j = i452 · subst j453 simpa [replaceRow] using hr454 · simpa [replaceRow, hji] using hB j455456/-- Every admissible row replacement determinant is bounded by the global maximum. -/457theorem abs_replacementDeterminant_le_maximum458 (b : Basis (Fin n) ℝ E) {B : Frame n E}459 (hB : B ∈ unitFrameSet n E) (i : Fin n) {r : E →L[ℝ] ℝ}460 (hr : r ∈ unitRowSet E) :461 |replacementDeterminant b B i r| ≤ determinantMaximum b := by462 simpa [determinantMaximum, replacementDeterminant] using463 abs_frameDeterminant_le_maximizingFrame b464 (replaceRow_mem_unitFrameSet hB i hr)465466/-- The Cramer numerator is controlled by row count, coefficient sup norm, and467maximum determinant. -/468theorem abs_cramerNumerator_le (b : Basis (Fin n) ℝ E)469 {B : Frame n E} (hB : B ∈ unitFrameSet n E)470 (c : Fin n → ℝ) {r : E →L[ℝ] ℝ} (hr : r ∈ unitRowSet E) :471 |∑ i : Fin n, c i * replacementDeterminant b B i r| ≤472 (n : ℝ) * ‖c‖ * determinantMaximum b := by473 calc474 |∑ i : Fin n, c i * replacementDeterminant b B i r| ≤475 ∑ i : Fin n, |c i * replacementDeterminant b B i r| :=476 Finset.abs_sum_le_sum_abs _ _477 _ ≤ ∑ _i : Fin n, ‖c‖ * determinantMaximum b := by478 apply Finset.sum_le_sum479 intro i _480 rw [abs_mul]481 exact mul_le_mul (norm_le_pi_norm c i)482 (abs_replacementDeterminant_le_maximum b hB i hr)483 (abs_nonneg _) (norm_nonneg c)484 _ = (n : ℝ) * ‖c‖ * determinantMaximum b := by485 simp [mul_assoc]486487/-- Coordinatewise inverse estimate. -/488theorem abs_inverse_mulVec_apply_le (b : Basis (Fin n) ℝ E)489 {η : ℝ} (hηD : η < determinantMaximum b) {B : Frame n E}490 (hB : B ∈ nearMaxFrames b η) (c : Fin n → ℝ) (j : Fin n) :491 |((frameMatrix b B)⁻¹.mulVec c) j| ≤492 ((n : ℝ) * determinantMaximum b /493 (coordinateScale b * (determinantMaximum b - η))) * ‖c‖ := by494 let x : Fin n → ℝ := (frameMatrix b B)⁻¹.mulVec c495 let r : E →L[ℝ] ℝ := coordinateRow b j496 have hgap : 0 < determinantMaximum b - η := sub_pos.mpr hηD497 have hden : 0 < coordinateScale b * (determinantMaximum b - η) :=498 mul_pos (coordinateScale_pos b) hgap499 have hr : r ∈ unitRowSet E := by500 simpa [r, coordinateFrame] using coordinateFrame_mem b j501 have hcramer := sum_mul_replacementDeterminant b B502 (nearMaxFrame_det_ne_zero b hηD hB) r c503 have hnum := abs_cramerNumerator_le b hB.1 c hr504 have heq :505 |frameDeterminant b B| * (coordinateScale b * |x j|) =506 |∑ i : Fin n, c i * replacementDeterminant b B i r| := by507 rw [hcramer]508 simp [x, r, abs_mul, coordinateRow_apply,509 abs_of_pos (coordinateScale_pos b)]510 have hlower :511 (determinantMaximum b - η) * (coordinateScale b * |x j|) ≤512 |frameDeterminant b B| * (coordinateScale b * |x j|) := by513 exact mul_le_mul_of_nonneg_right (nearMaxFrame_abs_det_lower b hB)514 (mul_nonneg (coordinateScale_pos b).le (abs_nonneg _))515 have hmain :516 coordinateScale b * (determinantMaximum b - η) * |x j| ≤517 (n : ℝ) * determinantMaximum b * ‖c‖ := by518 calc519 coordinateScale b * (determinantMaximum b - η) * |x j| =520 (determinantMaximum b - η) * (coordinateScale b * |x j|) := by ring521 _ ≤ |frameDeterminant b B| * (coordinateScale b * |x j|) := hlower522 _ = |∑ i : Fin n, c i * replacementDeterminant b B i r| := heq523 _ ≤ (n : ℝ) * ‖c‖ * determinantMaximum b := hnum524 _ = (n : ℝ) * determinantMaximum b * ‖c‖ := by ring525 change |x j| ≤ _526 calc527 |x j| ≤ ((n : ℝ) * determinantMaximum b * ‖c‖) /528 (coordinateScale b * (determinantMaximum b - η)) := by529 apply (le_div_iff₀ hden).2530 calc531 |x j| * (coordinateScale b * (determinantMaximum b - η)) =532 coordinateScale b * (determinantMaximum b - η) * |x j| := by ring533 _ ≤ (n : ℝ) * determinantMaximum b * ‖c‖ := hmain534 _ = ((n : ℝ) * determinantMaximum b /535 (coordinateScale b * (determinantMaximum b - η))) * ‖c‖ := by536 ring537538/-- Coordinate-space factor in the common inverse estimate. -/539noncomputable def coordinateInverseFactor (b : Basis (Fin n) ℝ E) (η : ℝ) : ℝ :=540 (n : ℝ) * determinantMaximum b /541 (coordinateScale b * (determinantMaximum b - η))542543/-- Explicit common inverse constant. The leading one preserves strict544positivity in dimension zero. -/545noncomputable def inverseBoundConstant (b : Basis (Fin n) ℝ E) (η : ℝ) : ℝ :=546 1 + ‖inverseCoordinateMap b‖ * coordinateInverseFactor b η547548/-- The explicit inverse constant is positive whenever the determinant gap is positive. -/549theorem inverseBoundConstant_pos (b : Basis (Fin n) ℝ E)550 {η : ℝ} (hηD : η < determinantMaximum b) :551 0 < inverseBoundConstant b η := by552 have hgap : 0 < determinantMaximum b - η := sub_pos.mpr hηD553 have hdet : 0 ≤ determinantMaximum b := (determinantMaximum_pos b).le554 have hn : 0 ≤ (n : ℝ) := Nat.cast_nonneg n555 have hfactor : 0 ≤ coordinateInverseFactor b η := by556 unfold coordinateInverseFactor557 exact div_nonneg (mul_nonneg hn hdet)558 (mul_nonneg (coordinateScale_pos b).le hgap.le)559 unfold inverseBoundConstant560 nlinarith [norm_nonneg (inverseCoordinateMap b)]561562/-- The explicit Cramer estimate transported back through the inverse coordinate map. -/563theorem inverseBoundConstant_bound (b : Basis (Fin n) ℝ E)564 {η : ℝ} (hηD : η < determinantMaximum b) {B : Frame n E}565 (hB : B ∈ nearMaxFrames b η) (c : Fin n → ℝ) :566 ‖(coordinateEquiv b).symm ((frameMatrix b B)⁻¹.mulVec c)‖ ≤567 inverseBoundConstant b η * ‖c‖ := by568 let C : ℝ := coordinateInverseFactor b η569 have hC : 0 ≤ C := by570 dsimp [C, coordinateInverseFactor]571 have hgap : 0 < determinantMaximum b - η := sub_pos.mpr hηD572 exact div_nonneg573 (mul_nonneg (Nat.cast_nonneg n) (determinantMaximum_pos b).le)574 (mul_nonneg (coordinateScale_pos b).le hgap.le)575 have hcoord : ‖(frameMatrix b B)⁻¹.mulVec c‖ ≤ C * ‖c‖ := by576 apply (pi_norm_le_iff_of_nonneg (mul_nonneg hC (norm_nonneg c))).2577 intro j578 simpa [C, coordinateInverseFactor] using579 abs_inverse_mulVec_apply_le b hηD hB c j580 have hop :581 ‖(coordinateEquiv b).symm ((frameMatrix b B)⁻¹.mulVec c)‖ ≤582 ‖inverseCoordinateMap b‖ * ‖(frameMatrix b B)⁻¹.mulVec c‖ := by583 exact (inverseCoordinateMap b).le_opNorm _584 calc585 ‖(coordinateEquiv b).symm ((frameMatrix b B)⁻¹.mulVec c)‖ ≤586 ‖inverseCoordinateMap b‖ * ‖(frameMatrix b B)⁻¹.mulVec c‖ := hop587 _ ≤ ‖inverseCoordinateMap b‖ * (C * ‖c‖) :=588 mul_le_mul_of_nonneg_left hcoord (norm_nonneg _)589 _ ≤ (1 + ‖inverseCoordinateMap b‖ * C) * ‖c‖ := by590 nlinarith [norm_nonneg c]591 _ = inverseBoundConstant b η * ‖c‖ := by592 simp [inverseBoundConstant, C]593594/-- Packaged common inverse estimate on the near-maximal frame set. -/595structure NearMaxInverseBound (b : Basis (Fin n) ℝ E) (η : ℝ) where596 /-- Common bound for every near-maximal inverse frame. -/597 boundConstant : ℝ598 /-- Strict positivity, including dimension zero. -/599 boundConstant_pos : 0 < boundConstant600 /-- Uniform estimate from the coordinate sup norm to the ambient norm. -/601 bound : ∀ {B : Frame n E}, B ∈ nearMaxFrames b η → ∀ c : Fin n → ℝ,602 ‖(coordinateEquiv b).symm ((frameMatrix b B)⁻¹.mulVec c)‖ ≤ boundConstant * ‖c‖603604namespace NearMaxInverseBound605606variable {b : Basis (Fin n) ℝ E} {η : ℝ}607608/-- The stored common bound is nonnegative. -/609theorem boundConstant_nonneg (H : NearMaxInverseBound b η) : 0 ≤ H.boundConstant := H.boundConstant_pos.le610611/-- Apply the stored estimate to a coefficient difference. -/612theorem bound_sub (H : NearMaxInverseBound b η) {B : Frame n E}613 (hB : B ∈ nearMaxFrames b η) (c d : Fin n → ℝ) :614 ‖(coordinateEquiv b).symm ((frameMatrix b B)⁻¹.mulVec (c - d))‖ ≤615 H.boundConstant * ‖c - d‖ :=616 H.bound hB (c - d)617618end NearMaxInverseBound619620/-- A common inverse bound exists for every nonnegative slack strictly below the621basis-dependent determinant maximum. -/622theorem nonempty_nearMaxInverseBound (b : Basis (Fin n) ℝ E) {η : ℝ}623 (_hη0 : 0 ≤ η) (hηD : η < determinantMaximum b) :624 Nonempty (NearMaxInverseBound b η) := by625 refine ⟨⟨inverseBoundConstant b η, inverseBoundConstant_pos b hηD, ?_⟩⟩626 intro B hB c627 exact inverseBoundConstant_bound b hηD hB c628629end DeterminantFrame630end MathlibAnnex