OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TranslationGates.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.TranslationGates.window line 14

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:150 (same declaration text).

  2. def OAI.VelocityDetection.TranslationGates.windowD line 16
  3. theorem OAI.VelocityDetection.TranslationGates.contDiff_window line 19
  4. theorem OAI.VelocityDetection.TranslationGates.hasDerivAt_window line 24
  5. theorem OAI.VelocityDetection.TranslationGates.deriv_window line 32
  6. theorem OAI.VelocityDetection.TranslationGates.contDiff_windowD line 34
  7. theorem OAI.VelocityDetection.TranslationGates.window_one line 38
  8. theorem OAI.VelocityDetection.TranslationGates.windowD_zero_inside line 43
  9. theorem OAI.VelocityDetection.TranslationGates.window_zero_outside line 48
  10. theorem OAI.VelocityDetection.TranslationGates.windowD_zero_outside line 53
  11. def OAI.VelocityDetection.TranslationGates.potential line 60
  12. def OAI.VelocityDetection.TranslationGates.field line 64
  13. theorem OAI.VelocityDetection.TranslationGates.contDiff_potential line 67
  14. theorem OAI.VelocityDetection.TranslationGates.divergence_field line 72
  15. theorem OAI.VelocityDetection.TranslationGates.potential_partial_zero line 76
  16. theorem OAI.VelocityDetection.TranslationGates.potential_partial_one line 90
  17. theorem OAI.VelocityDetection.TranslationGates.field_eq_velocity line 104
  18. theorem OAI.VelocityDetection.TranslationGates.field_zero_outside line 116
  19. theorem OAI.VelocityDetection.TranslationGates.field_zero_velocity line 134
  20. theorem OAI.VelocityDetection.TranslationGates.field_apply_zero line 138
  21. theorem OAI.VelocityDetection.TranslationGates.field_apply_one line 145
  22. theorem OAI.VelocityDetection.TranslationGates.contDiff_field line 152
  23. theorem OAI.VelocityDetection.TranslationGates.contDiff_movingField line 164
  24. theorem OAI.VelocityDetection.TranslationGates.compactSupport_field line 177
  25. theorem OAI.VelocityDetection.TranslationGates.finiteCylinderSupport line 187
  26. def OAI.VelocityDetection.TranslationGates.array line 207
  27. theorem OAI.VelocityDetection.TranslationGates.otherGate_zero line 210
  28. theorem OAI.VelocityDetection.TranslationGates.array_plateau line 222