Positive normal derivative of half-space coordinate transitions

At a boundary point, the zeroth coordinate of a chart transition has a local minimum within the model half-space. Fermat's theorem on the positive tangent cone makes its derivative vanish on the coordinate hyperplane and nonnegative in the inward direction. The inverse chart transition makes the inward coefficient strictly positive. Thus outward signs are independent of the preferred chart, including at boundary points.

theorem TauCeti.tangentCoordChange_normal_nonneg {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] {α β x : M} (hx : x ∈ ModelWithCorners.boundary M) (hα : x ∈ (extChartAt (modelWithCornersEuclideanHalfSpace (n + 1)) α).source) (hβ : x ∈ (extChartAt (modelWithCornersEuclideanHalfSpace (n + 1)) β).source) (v : EuclideanSpace ℝ (Fin (n + 1))) (hv : 0 ≤ v.ofLp 0) : 0 ≤ ((tangentCoordChange (modelWithCornersEuclideanHalfSpace (n + 1)) α β x) v).ofLp 0

At a boundary point an actual coordinate transition maps the closed inward half-space 0 ≤ v 0 into itself: the normal coordinate of the image of an inward vector is nonnegative.

theorem TauCeti.tangentCoordChange_normal_pos {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] {α β x : M} (hx : x ∈ ModelWithCorners.boundary M) (hα : x ∈ (extChartAt (modelWithCornersEuclideanHalfSpace (n + 1)) α).source) (hβ : x ∈ (extChartAt (modelWithCornersEuclideanHalfSpace (n + 1)) β).source) : ∃ (a : ℝ), 0 < a ∧ ∀ (v : EuclideanSpace ℝ (Fin (n + 1))), ((tangentCoordChange (modelWithCornersEuclideanHalfSpace (n + 1)) α β x) v).ofLp 0 = a * v.ofLp 0

At a boundary point an actual coordinate transition scales the normal coordinate by a strictly positive number. No block structure or orientation identity is assumed.