While this submission is a draft, it cannot be used by other submissions.

Proof of `Elementary properties of Bernstein numbers` (8th statement)

groundedproofs/Lax606786Proofs/GrassmannianContraction.lean · lax-606786

What this proof establishes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitLab

Description

For A,B∈𝓑(X)A, B ∈ 𝓑(X) and V,W∈𝒢kXV, W ∈ 𝒢_k X with d(V,W)<δd(V, W) < δ, take a minimiser x0x₀ of ‖A⋅‖‖A ·‖ on the compact unit sphere of VV and a point y0y₀ of the unit sphere of WW within δδ of it; then gB(W)≤gA(V)+(‖A‖+‖B−A‖)δ+‖B−A‖g_B(W) ≤ g_A(V) + (‖A‖ + ‖B - A‖) δ + ‖B - A‖. The same bound with the roles exchanged gives continuity.