Each satellite norms its coefficient preimage in absolute value

MathlibAnnex.Satellite.absoluteMaximizer_satellite_norms_preimage

theorem

Varying one functional at an absolute maximizer forces endpoint attainment.

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. Suppose and the admissible absolute maximizer also has . For every fixed , put . Then

Assumptions

Finiteness of , the positive comparison constants for , the positive determinant gap, admissibility, near-maximality of the base, and absolute maximality are required. The weight is any real number. No positive-weight or budget assumption is added.

Conclusion

Every satellite attains the norm in absolute value at its own coefficient preimage. This gives neither nor a common positive sign for all satellites.

Notes

The configuration polynomial evaluates on a pair. the product configuration type, satellite families, their contraction subset and the admissible product set retain both components of . The selected absolute maximizer is a choice from the compact product, not a uniqueness assertion. The proof-local scalar called p in the source is the number here; it is not a second norm.

Proof route

Separate one satellite contribution, use dominated Hahn–Banach endpoints, and apply rigidity of an affine absolute maximum.

theorem absoluteMaximizer_satellite_norms_preimage {n : ℕ}
    (M : NormModel n) {J : Type u} [Fintype J] [DecidableEq J]
    {η weight : ℝ} (hηD : η < detMax M)
    (coeff : J → Coord n)
    {C : SatelliteConfiguration n J}
    (hC : C ∈ satelliteConfigurationSet M J)
    (hnear : C.1 ∈ nearMaxFrames M η)
    (hmax : ∀ D ∈ satelliteConfigurationSet M J,
      |configurationPolynomial weight coeff D| ≤
        |configurationPolynomial weight coeff C|)
    (a : J) :
    |C.2 a (framePreimage C.1 (coeff a))| =
      M.p (framePreimage C.1 (coeff a))

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

private abbrev framePreimage {n : ℕ} (B : DualFrame n) (c : Coord n) := (dualFrameMatrix B)⁻¹.mulVec c
private abbrev IsDualContraction {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) := ∀ x, |r x| ≤ M.p x

private abbrev detMax {n : ℕ} (M : NormModel n) := DeterminantFrame.determinantMaximum (modelBasis M)
private abbrev NearMaxInverseBound {n : ℕ} (M : NormModel n) := DeterminantFrame.NearMaxInverseBound (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