Tentative formalization of the stability of the error estimation of a robot tilt#43

Draft

affeldt-aist wants to merge 67 commits intomasterfrom

Commits on Nov 17, 2025

upd opam
affeldt-aist
committed
start tilt formalization
affeldt-aist
committed
basic facts update (#44)

yosakaon
authored and
affeldt-aist
committed
equilibrium point
affeldt-aist
committed
started lyapunov function formalization

yosakaon
authored and
affeldt-aist
committed
fixes
affeldt-aist
committed
update lyapunov

yosakaon
authored and
affeldt-aist
committed
fix
affeldt-aist
committed
derive norm lemma

yosakaon
authored and
affeldt-aist
committed
wip
affeldt-aist
committed
upd

yosakaon
authored and
affeldt-aist
committed
wip
affeldt-aist
committed
working on is lyapunov

yosakaon
authored and
affeldt-aist
committed
upd

yosakaon
authored and
affeldt-aist
committed
cleaning, wip
affeldt-aist
committed
proved V1 Lie derivative matches the one in the paper + LieDerivative properties + tidying of the file

yosakaon
authored and
affeldt-aist
committed
fix naming

yosakaon
authored and
affeldt-aist
committed
working towards the end of the proof v1 is a lyapunov fx

yosakaon
authored and
affeldt-aist
committed
derive_sqrt and norm update

yosakaon
authored and
affeldt-aist
committed
complete proof of defposmx and such

yosakaon
authored and
affeldt-aist
committed
refactoring

yosakaon
authored and
affeldt-aist
committed
clean

yosakaon
authored and
affeldt-aist
committed
upd

yosakaon
authored and
affeldt-aist
committed
proved derivative is equal to 0 + bureaucratie lsubmx/rsubmx

yosakaon
authored and
affeldt-aist
committed
upd

yosakaon
authored and
affeldt-aist
committed
proved first implication of thm11a

yosakaon
authored and
affeldt-aist
committed
preuve thm11a sans cauchy

yosakaon
authored and
affeldt-aist
committed
cleaning
affeldt-aist
committed
tentative d'enonce

yosakaon
authored and
affeldt-aist
committed
split file
affeldt-aist
committed
cleaning + towards context formalization

yosakaon
authored and
affeldt-aist
committed
getting rid of admits (wip)
affeldt-aist
committed
upd

yosakaon
authored and
affeldt-aist
committed
bricolage y_a
affeldt-aist
committed
upd

yosakaon
authored and
affeldt-aist
committed
less admits
affeldt-aist
committed
part 3B

yosakaon
authored and
affeldt-aist
committed
velocity is not derived anymore but a measure

yosakaon
authored and
affeldt-aist
committed
checkpoint

yosakaon
authored and
affeldt-aist
committed
working state

yosakaon
authored and
affeldt-aist
committed
fix solves_equations

yosakaon
authored and
affeldt-aist
committed
rocq 9 update

yosakaon
authored and
affeldt-aist
committed
frames + diff

yosakaon
authored and
affeldt-aist
committed
upd

yosakaon
authored and
affeldt-aist
committed
a few lemmas about derivation
affeldt-aist
committed
propagate deriv hypo (broken state)

yosakaon
authored and
affeldt-aist
committed
cleaning

yosakaon
authored and
affeldt-aist
committed
wip lyapunov + closed ball

yosakaon
authored and
affeldt-aist
committed
use closed_ball_
affeldt-aist
committed
wip lyapunov

yosakaon
authored and
affeldt-aist
committed
fix compilation of tilt.v

yosakaon
authored and
affeldt-aist
committed
doc formatting, cleaning
affeldt-aist
committed
remove differentiability admits

yosakaon
authored and
affeldt-aist
committed

Commits on Dec 12, 2025

renaming of part A

yosakaon
authored and
affeldt-aist
committed
removed continuity admits from lyapunov proof

yosakaon
authored and
affeldt-aist
committed
fix notation

yosakaon
authored and
affeldt-aist
committed
trying to prove 0 is stable

yosakaon
authored and
affeldt-aist
committed
progress, cleaning, fix
affeldt-aist
committed
upd lnd

yosakaon
authored and
affeldt-aist
committed
fix derive norm squared
affeldt-aist
committed
progress lyapunov application

yosakaon
authored and
affeldt-aist
committed
evt for rV
affeldt-aist
committed
finished lyapunov

yosakaon
authored and
affeldt-aist
committed
various fixes:
affeldt-aist
committed
cleaning of tilt files

yosakaon
authored and
affeldt-aist
committed
minor renaming
affeldt-aist
committed
minor cleaning

yosakaon
authored and
affeldt-aist
committed