A zero theorem for outward-pointing Euclidean vector fields

This is the finite-dimensional topological input used by the equal-area power-weight existence proof. A continuous vector field on Euclidean space that points strictly outward along the unit sphere must vanish in the closed unit ball.

The proof uses the project's unconditional integral degree of positive-dimensional spheres. Under the contrary assumption, radial normalization gives a map from the closed ball to its boundary. Its restriction to the boundary is both nullhomotopic (because it extends over the contractible ball) and homotopic to the identity (by the strictly outward scalar-product condition), contradicting degree.

@[reducible, inline]

abbrev NRR.Topology.Ambient (d : ℕ) : Type

Euclidean ambient space for the sphere of dimension d.

Equations

• NRR.Topology.Ambient d = EuclideanSpace ℝ (Fin (d + 1))

theorem NRR.Topology.exists_zero_closedBall_of_inner_pos_on_sphere {d : ℕ} (hd : 1 ≤ d) (F : Ambient d → Ambient d) (hF : Continuous F) (hout : ∀ (x : Ambient d), ‖x‖ = 1 → 0 < inner ℝ x (F x)) : ∃ x ∈ Metric.closedBall 0 1, F x = 0

A continuous vector field that is strictly outward on the unit sphere has a zero in the closed unit ball. The positive-dimensional assumption is exactly what is needed by the integral sphere-degree API.