Rays chained along a partition

Mathlib's SameRay.trans chains two ray relations SameRay R x y and SameRay R y z into SameRay R x z, provided the middle vector y vanishes only when x or z does. This file iterates that step along a finite ordered partition of an interval in a linear order: if a map w into a normed additive group with an ordered scalar module structure lies, on each piece of the partition, on the ray of its value at the end of that piece, and the norm of w is nondecreasing, then every value of w lies on the ray of the final value. Monotonicity of the norm supplies the side condition of SameRay.trans: a partition point where w vanishes is preceded only by zeros. No compatibility between the norm and scalar multiplication is needed.

The explicit-partition induction follows the pattern of the Apache-2.0 frenzymath/Poincare-Conjecture formalization, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, as used in TauCeti/Geometry/Manifold/Riemannian/EDistComparison.lean.

Main results

• TauCeti.sameRay_of_partition_of_monotoneOn_norm: rays chain through a partition when the norm is nondecreasing.

theorem TauCeti.sameRay_of_partition_of_monotoneOn_norm {R : Type u_1} {α : Type u_2} {F : Type u_3} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [LinearOrder α] [NormedAddCommGroup F] [Module R F] {w : α → F} {k : ℕ} (τ : Fin (k + 2) → α) (hτ : ∀ (i : Fin (k + 1)), τ i.castSucc ≤ τ i.succ) (hpiece : ∀ (i : Fin (k + 1)), ∀ t ∈ Set.Icc (τ i.castSucc) (τ i.succ), SameRay R (w t) (w (τ i.succ))) (hmono : MonotoneOn (fun (t : α) => ‖w t‖) (Set.Icc (τ 0) (τ (Fin.last (k + 1))))) {t : α} (ht : t ∈ Set.Icc (τ 0) (τ (Fin.last (k + 1)))) : SameRay R (w t) (w (τ (Fin.last (k + 1))))

Rays chain through a partition. If a map w into a normed additive group with an ordered scalar module structure lies, on each piece of an ordered partition, on the ray of its value at the end of that piece, and its norm is nondecreasing, then every value lies on the ray of the final value. Monotonicity of the norm rules out a zero at a partition point preceded by a nonzero value.