Crossing a level with positive derivative

Let g : ℝ → ℝ be continuous on [a, b], and suppose that at every point of [a, b] where g takes the value c it is differentiable with positive derivative. Then g can cross the level c only upwards: once g ≥ c, it stays strictly above c at every later time of [a, b] (TauCeti.lt_image_of_deriv_pos_boundary), and once g ≤ c, it was strictly below c at every earlier time (TauCeti.image_lt_of_deriv_pos_boundary).

No differentiability is assumed away from the level. The statements are the strict, one-level counterpart of Mathlib's fencing inequalities such as image_le_of_deriv_right_lt_deriv_boundary, which assume a derivative estimate at every point of [a, b). They are what is needed to show that the trajectories of a vector field which crosses a hypersurface transversally in one direction cross it only in that direction.

Main results

• TauCeti.lt_image_of_deriv_pos_boundary: if c ≤ g a, then c < g t for every t ∈ (a, b].
• TauCeti.image_lt_of_deriv_pos_boundary: if g b ≤ c, then g t < c for every t ∈ [a, b).

theorem TauCeti.lt_image_of_deriv_pos_boundary {g g' : ℝ → ℝ} {a b c : ℝ} (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Icc a b, g t = c → HasDerivAt g (g' t) t ∧ 0 < g' t) (ha : c ≤ g a) ⦃t : ℝ⦄ : t ∈ Set.Ioc a b → c < g t

A level crossed with positive derivative is crossed only upwards. Let g be continuous on [a, b], with a positive derivative at every point of [a, b] where it takes the value c. If c ≤ g a, then c < g t for every t ∈ (a, b].

theorem TauCeti.image_lt_of_deriv_pos_boundary {g g' : ℝ → ℝ} {a b c : ℝ} (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Icc a b, g t = c → HasDerivAt g (g' t) t ∧ 0 < g' t) (hb : g b ≤ c) ⦃t : ℝ⦄ : t ∈ Set.Ico a b → g t < c

A level crossed with positive derivative is crossed only upwards, looking backwards. Let g be continuous on [a, b], with a positive derivative at every point of [a, b] where it takes the value c. If g b ≤ c, then g t < c for every t ∈ [a, b).