OAI/Analysis/PeriodicLattice/Signals.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Smooth machine signals and planar residual fields.

  1. def OAI.PeriodicLattice.Signal.inSlot line 18
  2. theorem OAI.PeriodicLattice.Signal.start line 22
  3. theorem OAI.PeriodicLattice.Signal.nonhalting_end line 25
  4. theorem OAI.PeriodicLattice.Signal.halting_end line 30
  5. theorem OAI.PeriodicLattice.Signal.nonhalting_interval line 35
  6. theorem OAI.PeriodicLattice.Signal.halting_interval line 53
  7. theorem OAI.PeriodicLattice.Signal.displacement_in_plateau line 60
  8. theorem OAI.PeriodicLattice.Signal.history_in_plateau line 76
  9. def OAI.PeriodicLattice.Residual.force line 95
  10. theorem OAI.PeriodicLattice.Residual.spaceD_zero line 98
  11. theorem OAI.PeriodicLattice.Residual.gradient_zero line 102
  12. theorem OAI.PeriodicLattice.Residual.spaceD_neg line 107
  13. theorem OAI.PeriodicLattice.Residual.gradient_neg line 111
  14. theorem OAI.PeriodicLattice.Residual.divergence_gradient line 117
  15. theorem OAI.PeriodicLattice.Residual.equations line 120
  16. theorem OAI.PeriodicLattice.Residual.projection_equations line 128
  17. def OAI.PeriodicLattice.Scales.crudeSlotBound line 145
  18. theorem OAI.PeriodicLattice.Scales.slotSize_le_crude line 148
  19. def OAI.PeriodicLattice.Scales.allSlotsBound line 169
  20. theorem OAI.PeriodicLattice.Scales.weighted_slotSize_bound_all line 172