The chosen support slice consists of almost-isometric generators

MathlibAnnex.FiniteRecovery.targetRawSupportMaximizer_good

theorem

Obtains one almost-isometric map from each point of the specified raw maximum slice.

Statement

Let . Use reference coordinates with the sup norm and standard basis. The supplied continuous seminorm has constants satisfying Thus is a norm; it can differ from the reference sup norm. With standard Lebesgue measure put and . For a real linear map , its matrix is . The vector has coordinates , one for each increasing -tuple of distinct rows. Define A base family consists of real linear functionals on . Put . Let and Fix , , and one such that for all and all . Set Take a finite covering that annulus at sup-distance at most ; its center gives . Fix with For a family of real linear functionals , call admissible when and for all . For this configuration put Here the replaced row is . Put . In minor space let select the base rows and select all base rows except , then satellite , and let be the corresponding minor-coordinate unit vector. Define Choose an admissible absolute maximizer of . Set if and otherwise, and define the linear functional (oriented support). If then one real linear satisfies

Assumptions

The inputs are the continuous norm with the displayed comparison bounds; ; ; the common inverse bound ; the stated finite net at radius ; ; the strict budget; and a point in the displayed maximum slice of . All rows in the admissible configurations are real linear functionals. There is no assumption .

Conclusion

One has all three properties. For each unit vector the detecting satellite index may vary, while the map is fixed first.

Proof route

Recover the same generating map, transfer support maximality to absolute polynomial maximality, and use the finite-net estimate.

The sign belongs to the fixed functional , whereas represents the input raw generator. They have different roles. The raw set is compact and nonempty; its convex hull is the Plücker body. The hypothesis here concerns the raw maximum slice itself, not an arbitrary point of that convex hull.

theorem targetRawSupportMaximizer_good
    {m : ℕ} (M : NormModel (m + 1)) {η ε weight : ℝ}
    (hη0 : 0 ≤ η) (hηD : η < detMax M) (hε : 0 < ε)
    (H : NearMaxInverseBound M η)
    (Cnet : FiniteCoefficientNet (n := m + 1) H.boundConstant
      (satelliteRadiusNNReal ε H.boundConstant hε H.boundConstant_pos))
    (hweight : 0 < weight)
    (hgap : satelliteBudget M (centerValue Cnet) < weight * η)
    {z : PluckerCoord (m + 1)
      (positiveSatelliteAmbientDim m Cnet.centers)}
    (hz : z ∈ MathlibAnnex.NonemptyCompacts.maxSlice (rawPluckerCompact
      (N := positiveSatelliteAmbientDim m Cnet.centers) M)
        (orientedSatelliteSupport weight (centerValue Cnet)
          (maxSatelliteConfiguration M Cnet.centers
            weight (centerValue Cnet)))) :
    PluckerGeneratorGood M ε z

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