MATHLIBANNEX / CANONICAL DECLARATION CARD

A nearby norming point gives an almost-norming evaluation

MathlibAnnex.Satellite.abs_eval_lower_of_norms_nearby

theorem

Two triangle inequalities transfer absolute norm attainment to a unit vector.

Statement

Let and use reference coordinates with the sup norm. Let be a continuous seminorm with specified constants such that The lower comparison makes a norm. Let be continuous and real linear, with for every and let , satisfy Then .

Assumptions

The four hypotheses are contraction for all , the unit condition at , the error bound at , and absolute norm attainment at . No independent or hypothesis is imposed; nonnegativity follows from .

Conclusion

The same functional gives . It norms exactly and evaluates the nearby unit vector approximately; these points are not interchanged.

Proof route

Compare the norm at the nearby point with the unit norm, then bound the change in the same linear functional.

Proof steps
  1. The seminorm triangle inequality gives , hence . By linearity and contraction, Combining the two displayed bounds yields . This also covers and estimates whose lower bound is negative.

The contraction is evaluated at the difference of the two displayed points; the estimate is an elementary seminorm calculation.

Main citations

Lean source signature (exact)

theorem abs_eval_lower_of_norms_nearby {n : ℕ} (M : NormModel n)
    {r : Coord n →L[ℝ] ℝ} (hr : IsDualContraction M r)
    {x z : Coord n} (hx : M.p x = 1)
    {δ : ℝ} (hδ : M.p (x - z) ≤ δ)
    (hnorm : |r z| = M.p z) :
    1 - 2 * δ ≤ |r x|

The four named proof arguments are precisely the four mathematical hypotheses. The final inequality is the conclusion.

In the source Mathematical meaning
Coord n The reference space with its sup norm; Coord n abbreviates Fin n → ℝ. Lean uses indices and the formulas use .
M : NormModel n; M.p The input M contains the continuous seminorm and constants with for every . M.p x is the scalar .
r : Coord n →L[ℝ] ℝ; hr : IsDualContraction M r The given is continuous and real linear, with for every .
hx : M.p x = 1 The point at which we want an approximate evaluation satisfies .
hδ : M.p (x - z) ≤ δ The nearby point satisfies , with .
In the source Mathematical meaning
hnorm : |r z| = M.p z The same attains the norm at in absolute value: .
1 - 2 * δ ≤ |r x| The conclusion is an evaluation at , not at .

M.p (x - z) evaluates the norm on a difference; r x evaluates the given functional. Braces permit inference of , without changing their mathematical roles.

Relevant surrounding context (separate exact excerpts)

Exact source lines 13–14:

private abbrev Coord (n : ℕ) := Fin n → ℝ
private abbrev NormModel (n : ℕ) := EquivalentSeminorm (Coord n)

Exact source lines 21–21:

private abbrev IsDualContraction {n : ℕ} (M : NormModel n) (r : Coord n →L[ℝ] ℝ) := ∀ x, |r x| ≤ M.p x

Full surrounding source. These excerpts are separate from the declaration above.

Surrounding assumptions and aliases: exact source, lines 7–55. The full original context is retained with the source evidence.

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

Exact content identity

Declaration: MathlibAnnex.Satellite.abs_eval_lower_of_norms_nearby

Accepted content SHA-256: 76a978dcc00e16703cf5650212cdf371c6a0d7983de05960d47b27b416cfd983

Accepted source guide SHA-256: c7d5421eb642679086963db6dd65e1f774bc89a39629ad92ffec02e9e14429c5

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑