OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/BoundedSpatialJetTimeDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lift the pointwise scalar equation to the finite spatial-jet Banach space by FTC.

  1. theorem OAI.ForcedComputation.BoundedSpatialJets.integral_eq_sub_of_pointwise_derivative line 16
  2. theorem OAI.ForcedComputation.BoundedSpatialJets.hasDerivWithinAt_of_pointwise_derivative line 39