Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Second-order jets of separated functions

This file records the ordinary two-sided jet consequences of writing a function on R^n × R^n as a separated difference. The development lives in the SeparatedJets/ submodules; this file re-exports all of them.