Outward-pointing vectors at the boundary #
For a manifold modeled on Mathlib's Euclidean half-space, this file records the sign convention
for an outward tangent vector. Mathlib puts the boundary coordinate in slot 0; outward vectors
therefore have a negative slot-0 derivative. The definition uses the preferred chart through
mfderiv; the positive normal derivative of actual chart transitions proves coordinate
independence in isOutwardPointing_iff_tangentCoordChange. This is the interface used by boundary
orientation and Stokes
constructions. When the inward coordinate of the preferred chart is a nonzero multiple of g - c
for a real function g, outwardness is the sign of the derivative of g
(isOutwardPointing_iff_mul_mvfderiv_neg); this is how a boundary defining function, such as the
function cutting out a sublevel, detects the outward direction.
The sign convention follows J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Proposition
15.33, adapted to Mathlib's convention that the constrained coordinate is in slot 0.
The standard half-space supplies a concrete witness: the constant negative first-coordinate vector is outward at every boundary point.
A tangent vector at a boundary point points outward when its preferred half-space coordinate
has negative derivative. The zeroth coordinate is the constrained coordinate of
EuclideanHalfSpace; this sign convention agrees with the outward-first boundary orientation.
Instances For
An outward-pointing vector is based at the boundary, with negative zeroth coordinate derivative in the preferred half-space chart.
Outwardness can be tested in any preferred chart containing the boundary point.
Suppose that, near a boundary point x, the inward coordinate (slot 0) of the preferred
chart at x is s * (g - c) for a real function g and constants c and s ≠ 0. Then a
tangent vector v at x points outward exactly when s times the derivative of g is negative
on it. For s = -1 this says that g increases along outward vectors.
An outward-pointing vector is based at a boundary point.
The preferred-chart derivative of an outward-pointing vector is negative in slot 0.
Positive rescaling preserves the outward half-space of tangent vectors.
The sum of two outward vectors is outward.
The outward-pointing vectors at a fixed point form a convex set. This is the pointwise interface used when smooth local outward fields are glued by a partition of unity.
An outward vector is nonzero.
On the standard half-space, the constant vector -e₀ is outward at every boundary point.
A smooth vector field is outward-pointing when each of its boundary values points out of the half-space. Smoothness is recorded as regularity of the corresponding tangent-bundle section, so the predicate does not depend on a choice of tangent-bundle trivialization.
Instances For
Characterization of a smooth outward-pointing field by its smoothness and boundary values.
Construct a smooth outward-pointing field from its smoothness and boundary values.
The field component of an outward-pointing field is smooth.
Every boundary value of an outward-pointing field points out.
The sum of two smooth outward-pointing fields is outward-pointing.
Multiplication by a smooth positive scalar preserves an outward-pointing field.
Smooth convex combinations of outward-pointing fields remain outward-pointing. The coefficients are smooth globally, nonnegative on the boundary, and sum to one there.
The constant negative normal field on the standard Euclidean half-space.
Instances For
The standard field has constant negative zeroth coordinate.
The standard negative normal field is smooth as a tangent-bundle section.
The standard Euclidean half-space has a smooth outward-pointing field.