Back to Project mathematical routes
An attained positive determinant maximum supplies well-conditioned dual frames. Weighted satellite arguments and a finite almost-norming family control the vectors needed for approximate linear recovery; the exact lower-unit condition remains explicit.
11 direct Cards + 1 reused prerequisite = 12 unique Cards. This count is a selected Card closure, not a source-declaration count.
Route reading PDF · Preserved source exploration
Read this route with prerequisites
Direct references: SR190 — An attained absolute determinant maximum · SR207 — Positivity of the determinant maximum · SR216 — The set of near-maximal dual frames · SR230 — A common inverse estimate from row Cramer · SR235 — A weighted determinant polynomial with satellites · SR253 — Absolute maximization forces a near-maximal base · SR255 — Each satellite norms its coefficient preimage in absolute value · SR257 — A nearby norming point gives an almost-norming evaluation · SR258 — One fixed satellite family almost norms every detected unit vector · SR263 — A finite absolute-maximizing family almost norms the unit sphere · SR325 — A strict lower bound on a norm’s unit sphere
Reused prerequisites: SR264 — A seminorm with two-sided bounds against a reference norm
Read selected Card prerequisites before their uses. Levels are recomputed from the selected reachability-preserving projection; omitted source helpers remain traceable in the source exploration.
No Cards match this search. Clear search to recover this reading scope.
Adds linear row-replacement contributions to a base determinant.
MathlibAnnex.Satellite.satellitePolynomial
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Absolute maximization forces a near-maximal base · Each satellite norms its coefficient preimage in absolute value
Selects a maximizing dual frame for a specified basis.
MathlibAnnex.DeterminantFrame.exists_maximizingFrame
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Absolute maximization forces a near-maximal base · The set of near-maximal dual frames · Positivity of the determinant maximum
Records a norm through a seminorm, two positive comparison constants and continuity on the original normed space.
MathlibAnnex.EquivalentSeminorm
Immediate Card prerequisites: None in this selected scope
Used by in this scope: A strict lower bound on a norm’s unit sphere · Absolute maximization forces a near-maximal base · Each satellite norms its coefficient preimage in absolute value · A nearby norming point gives an almost-norming evaluation
A dominant determinant term prevents a large deficit in the base frame.
MathlibAnnex.Satellite.absoluteMaximizer_base_nearMax
Immediate Card prerequisites: A seminorm with two-sided bounds against a reference norm · A weighted determinant polynomial with satellites · An attained absolute determinant maximum
Used by in this scope: A finite absolute-maximizing family almost norms the unit sphere
A uniformly scaled dual basis supplies a positive comparison determinant.
MathlibAnnex.DeterminantFrame.determinantMaximum_pos
Immediate Card prerequisites: An attained absolute determinant maximum
Used by in this scope: A common inverse estimate from row Cramer
Defines the strict lower condition on a fixed norm unit sphere.
MathlibAnnex.FiniteSup.FinMapAlmostIsometric
Immediate Card prerequisites: A seminorm with two-sided bounds against a reference norm
Used by in this scope: None in this selected scope
Records a determinant deficit while keeping all dual rows contractive.
MathlibAnnex.DeterminantFrame.nearMaxFrames
Immediate Card prerequisites: An attained absolute determinant maximum
Used by in this scope: A common inverse estimate from row Cramer · Each satellite norms its coefficient preimage in absolute value
Two triangle inequalities transfer absolute norm attainment to a unit vector.
MathlibAnnex.Satellite.abs_eval_lower_of_norms_nearby
Immediate Card prerequisites: A seminorm with two-sided bounds against a reference norm
Used by in this scope: One fixed satellite family almost norms every detected unit vector
Controls all near-maximal inverse frames by an explicit basis-dependent constant.
MathlibAnnex.DeterminantFrame.inverseBoundConstant_bound
Immediate Card prerequisites: The set of near-maximal dual frames · Positivity of the determinant maximum
Used by in this scope: A finite absolute-maximizing family almost norms the unit sphere
Varying one functional at an absolute maximizer forces endpoint attainment.
MathlibAnnex.Satellite.absoluteMaximizer_satellite_norms_preimage
Immediate Card prerequisites: A seminorm with two-sided bounds against a reference norm · A weighted determinant polynomial with satellites · The set of near-maximal dual frames
Used by in this scope: One fixed satellite family almost norms every detected unit vector
Uses a detecting coefficient and its matching satellite without replacing the family.
MathlibAnnex.Satellite.absoluteMaximizer_satellites_almost_norm
Immediate Card prerequisites: Each satellite norms its coefficient preimage in absolute value · A nearby norming point gives an almost-norming evaluation
Used by in this scope: A finite absolute-maximizing family almost norms the unit sphere
Chooses the inverse bound, net and weight before fixing one satellite family.
MathlibAnnex.Satellite.exists_goodSatellitePackage
Immediate Card prerequisites: A common inverse estimate from row Cramer · Absolute maximization forces a near-maximal base · One fixed satellite family almost norms every detected unit vector
Used by in this scope: None in this selected scope