OAI/Geometry/EinsteinFour/FlowVariationalRegularity.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The variational lift loses exactly one finite derivative.
- theorem
OAI.PositiveEinsteinFour.FlowCalculus.variationalField_contDiffAt_orderline 15