OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/CompactDetectorExpressions.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite clocked expressions relative to the given planar-field evaluator. Input atoms are derivatives of the input field, not derivatives of the constructed force. Product and chain rules remain part of the compiler.

  1. abbrev OAI.ForcedComputation.VelocityDetector.PlanarComponents line 13
  2. def OAI.ForcedComputation.VelocityDetector.componentJet line 15
  3. theorem OAI.ForcedComputation.VelocityDetector.componentJet_smooth line 18
  4. structure OAI.ForcedComputation.VelocityDetector.PlanarJetOracle line 28

    Source documentation

    The numerical information supplied with the effectively specified input planar field. All bounds are global input-derivative bounds.

    structure PlanarJetOracle (F : PlanarComponents) where
…

    Mentions: OAI.ForcedComputation.VelocityDetector.PlanarComponents

  5. inductive OAI.ForcedComputation.VelocityDetector.DetectorExpr line 38
  6. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.val line 47
  7. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.Valid line 53
  8. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.diff line 59
  9. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.valid_diff line 67
  10. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.smooth line 75
  11. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.val_diff line 83
  12. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.diffWord line 114
  13. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.valid_diffWord line 118
  14. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.val_diffWord line 124
  15. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.bound line 135
  16. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.bound_nonneg line 141
  17. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.val_bound line 149