One fixed satellite family almost norms every detected unit vector

MathlibAnnex.Satellite.absoluteMaximizer_satellites_almost_norm

theorem

Uses a detecting coefficient and its matching satellite without replacing the family.

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.

A common inverse bound consists of a number and the uniform estimate It is fixed independently of the particular frame and coefficient. When , every such frame has nonzero determinant. Suppose , is an admissible absolute maximizer with , and a real satisfies the coefficient-detection hypothesis Then, for any with , there is with .

Assumptions

A fixed common inverse bound with its uniform estimate, a fixed coefficient family, the full detection hypothesis, the positive determinant gap, admissibility, near-maximality and absolute maximality are required. There is no separate positivity assumption on or .

Conclusion

The index may depend on , but the entire satellite family and its maximizing configuration have already been fixed. The output evaluates the satellite having the same index as the detected coefficient.

Proof route

Detect one coefficient near the given unit vector, use its matching norming satellite, then apply the two-error estimate.

The full quantifier order is defined in coefficient detection. An actual finite net supplies it as follows. For a near-maximal and unit , contractive frame coordinates gives , while the uniform inverse estimate gives . Thus membership in the coefficient annulus puts in . A center within reference distance then gives, by inverse transport of the coefficient error, . This is a close preimage from the finite net. The present theorem assumes detection explicitly and does not itself select that net.

theorem absoluteMaximizer_satellites_almost_norm {n : ℕ}
    (M : NormModel n) {J : Type u} [Fintype J] [DecidableEq J]
    {η weight ρ : ℝ} (hηD : η < detMax M)
    (H : NearMaxInverseBound M η) (coeff : J → Coord n)
    (hdetect : CoefficientDetectsUnit M η H ρ coeff)
    {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|)
    {x : Coord n} (hx : M.p x = 1) :
    ∃ a : J, 1 - 2 * (H.boundConstant * ρ) ≤ |C.2 a x|

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