Absolute maximization forces a near-maximal base

MathlibAnnex.Satellite.absoluteMaximizer_base_nearMax

theorem

A dominant determinant term prevents a large deficit in the base frame.

Statement

Let and use reference coordinates with the sup norm. Let be a continuous seminorm with specified constants such that Thus is a norm. We use for the model distance and for reference-coordinate estimates; the two norms are allowed to coincide. A -dual contraction is a continuous real linear functional satisfying for every . Let be the standard coordinate vectors. For an ordered family of continuous real linear functionals on , put For a real number , define the attained maximum and near-maximal set by Admissibility is measured with ; the matrices are written in the fixed reference coordinates.

Let be a finite index set, possibly empty; choose coefficients for . A configuration is a pair , where is a frame and is a family of additional continuous real linear functionals, called satellites. Write For any real weight , let replace row by and set An absolute maximizer means a single with for every . It need not maximize the signed polynomial. Set Suppose , , , and is an admissible absolute maximizer. Then .

Assumptions

The stated positive comparison constants for , finiteness of , nonnegative deficit, positive weight, strict budget inequality, admissibility of and its global absolute maximality are required. There is no assumption in this theorem.

Conclusion

The base frame has while remaining -dual contractive. Invertibility requires the separate additional condition .

Proof route

Bound the satellite sum and compare against an attained maximum frame with zero satellites.

The budget is defined by the determinant-scaled coefficient sum. For later applications with , a weight dominating that budget chooses , giving and . This weight choice is a contextual result with the stronger positive-deficit input, not an additional assumption on this theorem.

theorem absoluteMaximizer_base_nearMax {n : ℕ} {J : Type u}
    [Fintype J] (M : NormModel n) {η weight : ℝ}
    (hη0 : 0 ≤ η) (hweight : 0 < weight)
    (coeff : J → Coord n)
    (hgap : satelliteBudget M coeff < weight * η)
    {C : SatelliteConfiguration n J}
    (hC : C ∈ satelliteConfigurationSet M J)
    (hmax : ∀ D ∈ satelliteConfigurationSet M J,
      |configurationPolynomial weight coeff D| ≤
        |configurationPolynomial weight coeff C|) :
    C.1 ∈ nearMaxFrames M η

private abbrev Coord (n : ℕ) := Fin n → ℝ
private abbrev NormModel (n : ℕ) := EquivalentSeminorm (Coord n)
private abbrev DualFrame (n : ℕ) := DeterminantFrame.Frame n (Coord n)

private abbrev detMax {n : ℕ} (M : NormModel n) := DeterminantFrame.determinantMaximum (modelBasis M)

private abbrev nearMaxFrames {n : ℕ} (M : NormModel n) (η : ℝ) := {B : DualFrame n | B ∈ dualFrameSet M ∧ detMax M - η ≤ |frameDet B|}

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project