OptimalSpeedTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transferring a fixed initial speed from one optimizer to another

The common initial marginal identifies the slope-square integral. Equality of optimal costs then turns the pointwise speed bound into equality, even when the second plan has no compression estimate.

theorem OAI.RegularPointCoordinates.optimal_initial_speed_transfer line 20