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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth coefficients define bounded continuous curves of every finite jet order.

  1. theorem OAI.ForcedComputation.collect_jet_bounds line 15
  2. theorem OAI.ForcedComputation.periodic_jet_bounds line 42
  3. theorem OAI.ForcedComputation.supported_spatialParameterDerivative line 61
  4. theorem OAI.ForcedComputation.supported_jet_bounds line 74
  5. theorem OAI.ForcedComputation.exists_periodic_jet_curve line 94
  6. theorem OAI.ForcedComputation.exists_supported_jet_curve line 103