OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Periodization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.Periodization.lattice line 12
  2. theorem OAI.VelocityDetection.Periodization.lattice_zero line 14
  3. theorem OAI.VelocityDetection.Periodization.lattice_add line 16
  4. def OAI.VelocityDetection.Periodization.extend line 19
  5. def OAI.VelocityDetection.Periodization.box line 22
  6. theorem OAI.VelocityDetection.Periodization.extend_finite line 25
  7. theorem OAI.VelocityDetection.Periodization.contDiff_extend line 46
  8. theorem OAI.VelocityDetection.Periodization.extend_add_lattice line 64
  9. theorem OAI.VelocityDetection.Periodization.cover_eq_iff line 77
  10. theorem OAI.VelocityDetection.Periodization.periodic_extend line 101
  11. theorem OAI.VelocityDetection.Periodization.extend_eq_chart line 107
  12. theorem OAI.VelocityDetection.Periodization.extend_eventuallyEq_chart line 131