New member - advice appreciated

Stream: new members

[Jeremy Parker]

Hello! I'm an applied mathematician based in Scotland, interested in dynamical systems and fluid dynamics. I've just started playing around in Lean.

I've written this first result, which is a simple Lyapunov theorem. I would greatly appreciate any advice before I start trying to anything more complicated. In particular, I spent a lot of time trying to prove continuity of my integrand. Are there shortcuts that would speed this up?

import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.ODE.PicardLindelof
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

/-- Suppose we have a solution to a system dx/dt = f(x) defined for all time,
    and a Lyapunov function V such that
    f.∇ V ≤ 0 and V ≥ x^2.
    Then the trajectory is bounded forwards in time. -/
theorem Lyapunov
   {n : ℕ}
   (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hf : LipschitzWith 1 f)
   (V : EuclideanSpace ℝ (Fin n) → ℝ) (hV : ContDiff ℝ 1 V)
   (hV_inequality_1 : ∀ x, (fderiv ℝ V x) (f x) ≤ 0) (hV_inequality_2 : ∀ x, V x ≥ ‖x‖ ^ 2)
   (x : ℝ → EuclideanSpace ℝ (Fin n)) (hx : ∀ t, HasDerivAt x (f (x t)) t) :
   ∃ C, ∀ t > 0, ‖x t‖^2 ≤ C := by
  have h_V_deriv : ∀ t, HasDerivAt (V ∘ x) (fderiv ℝ V (x t) (f (x t))) t := by
    intro t
    convert (HasFDerivAt.comp t (hV.differentiable le_rfl (x t)).hasFDerivAt (hx t)).hasDerivAt
    simp

  have h_integrable (T : ℝ) : IntervalIntegrable (deriv  (V ∘ x)) MeasureTheory.volume 0 T := by
    have hx_cont : Continuous x := by
      exact continuous_iff_continuousAt.mpr (fun t => (hx t).continuousAt)

    have hfx_cont : Continuous (fun t => f (x t)) := by
      exact Continuous.comp' hf.continuous hx_cont

    have hcomp_cont : Continuous (fun t => fderiv ℝ V (x t)) := by
      exact Continuous.comp' (hV.continuous_fderiv le_rfl) hx_cont

    have hfull_cont : Continuous (fun t => fderiv ℝ V (x t) (f (x t))) := by
      exact Continuous.clm_apply hcomp_cont hfx_cont

    have h_integrand_cont : Continuous (deriv  (V ∘ x)) := by
      rw [deriv_eq h_V_deriv]
      exact hfull_cont

    exact Continuous.intervalIntegrable h_integrand_cont 0 T

  have h_V_decreasing : ∀ t, -(deriv (V ∘ x) t) ≥ 0 := by
    intro t
    calc
      -(deriv (V ∘ x) t) = -(fderiv ℝ V (x t) (f (x t))) := by rw [(h_V_deriv t).deriv]
      _ ≥ -0 := by grw[hV_inequality_1 (x t)]
      _ = 0 := by ring

  let C := V (x 0)
  use C
  intro T ht

  have int_inequality : ∫ t in 0..T, -(deriv (V ∘ x) t) ≥ 0 := by
    exact intervalIntegral.integral_nonneg_of_forall ht.le h_V_decreasing

  have h_diff : ∀ t ∈ Set.uIcc 0 T, DifferentiableAt ℝ (V ∘ x) t :=
    fun t ht => (h_V_deriv t).differentiableAt

  calc
    ‖x T‖ ^ 2 ≤ V (x T) := by grw [hV_inequality_2 (x T)]
    _ = V (x 0) + ((V ∘ x) T - (V ∘ x) 0) := by simp
    _ = V (x 0) +∫ t in 0..T, (deriv (V ∘ x) t) := by
      rw[intervalIntegral.integral_deriv_eq_sub h_diff (h_integrable T)]
    _ = V (x 0) -∫ t in 0..T, -(deriv (V ∘ x) t) := by rw [intervalIntegral.integral_neg];simp
    _ = C -∫ t in 0..T, -(deriv (V ∘ x) t) := by ring
  exact sub_le_self _ int_inequality

I was trying to get ChatGPT to guide me through things, which strikes me as one of the major opportunities for math in 2025, but I found that to be more painful than it was worth. Any other LLMs work better? Or are people still many writing everything by hand?

[Michael Rothgang]

Hi, welcome! I'm among the "write by hand" crowd: in my opinion, AI is often not good enough yet. (Putting ecological or ethical concerns aside.) Others may me able to tell you more.
Writing by hand can certainly be helpful for learning: feel free to ask for help here if you get stuck!

[Michael Rothgang]

For your continuity proofs, there are ways to do better. Are you aware of the fun_prop tactic? For goals of the form "this is just a composition of functions which we know are continuous", it often works well.

[Jeremy Parker]

Thanks @Michael Rothgang , I wasn't aware of fun_prop (I've only gone through a few basic tutorials so far) but it doesn't immediately seem to work for my case

[Michael Rothgang]

Indeed! I started playing with your proof; the first lemma is outside of what fun_prop can do. However, once you provide a few basic facts, it can help you. Here's a shorter version of your continuity proofs:

  have h_integrable (T : ℝ) : IntervalIntegrable (deriv  (V ∘ x)) MeasureTheory.volume 0 T := by
    have hx_cont : Continuous x := continuous_iff_continuousAt.mpr (fun t => (hx t).continuousAt)
    have := hf.continuous
    have := hV.continuous_fderiv le_rfl
    have h_integrand_cont : Continuous (deriv  (V ∘ x)) := by
      rw [deriv_eq h_V_deriv]
      fun_prop
    exact Continuous.intervalIntegrable h_integrand_cont 0 T

[Michael Rothgang]

I have put the facts hf.continuous ("a Lipschitz function is continuous") and hV.continuous_fderiv le_rfl into the local context. With these and hx_cont, fun_prop can prove your goal.

[Michael Rothgang]

Another small trick: if you write by exact ..., usually you can remove these two words.

[Michael Rothgang]

And a last one: you can use dot notation to shorten the last line to exact h_integrand_cont.intervalIntegrable 0 T.

[Michael Rothgang]

Dot notation means: if you want to call a theorem Continuous.foo and the first argument a is something of type Continuous ..., you can write a.foo instead of Continuous.foo a. Especially when chaining continuity lemmas, this can make proofs quite a bit shorter.

[Ben Eltschig]

Michael Rothgang said:

Dot notation means: if you want to call a theorem Continuous.foo and the first argument a is something of type Continuous ..., you can write a.foo instead of Continuous.foo a. Especially when chaining continuity lemmas, this can make proofs quite a bit shorter.

It doesn't even have to be the first argument, just the first argument of type Continuous .... I.e., hf.foo a for Continuous.foo a hf with a some other argument works too

[Jeremy Parker]

Thanks both - this is exactly the sort of tip I need