OAI/Analysis/PeriodicLattice/Energy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Energy inequalities and uniqueness of classical periodic solutions.

  1. theorem OAI.PeriodicLattice.TorusCalculus.time_hasDerivAt line 22
  2. def OAI.PeriodicLattice.TorusCalculus.energy line 27
  3. theorem OAI.PeriodicLattice.TorusCalculus.energy_nonneg line 30
  4. theorem OAI.PeriodicLattice.TorusCalculus.energy_continuousOn line 34
  5. theorem OAI.PeriodicLattice.TorusCalculus.energy_hasDerivAt line 39
  6. theorem OAI.PeriodicLattice.TorusCalculus.eq_zero_of_linear_deriv_bound line 66
  7. theorem OAI.PeriodicLattice.TorusCalculus.cylinder_sub line 106
  8. theorem OAI.PeriodicLattice.TorusCalculus.timeD_sub line 109
  9. theorem OAI.PeriodicLattice.TorusCalculus.timeD_congr_nonneg line 114
  10. theorem OAI.PeriodicLattice.TorusCalculus.divergence_sub line 124
  11. theorem OAI.PeriodicLattice.TorusCalculus.gradient_sub line 131
  12. theorem OAI.PeriodicLattice.TorusCalculus.advection_sub line 137
  13. def OAI.PeriodicLattice.TorusCalculus.gradientSize line 146
  14. theorem OAI.PeriodicLattice.TorusCalculus.gradientSize_nonneg line 148
  15. theorem OAI.PeriodicLattice.TorusCalculus.gradientSize_cylinderContinuous line 151
  16. theorem OAI.PeriodicLattice.TorusCalculus.transport_norm_le line 156
  17. theorem OAI.PeriodicLattice.TorusCalculus.inner_transport_bound line 166
  18. theorem OAI.PeriodicLattice.TorusCalculus.gradientSize_bounded line 175
  19. theorem OAI.PeriodicLattice.TorusCalculus.timeD_sub_cylinderContinuous line 190
  20. theorem OAI.PeriodicLattice.TorusCalculus.classical_difference_equation line 200
  21. theorem OAI.PeriodicLattice.TorusCalculus.classical_energy_identity line 222
  22. theorem OAI.PeriodicLattice.TorusCalculus.classical_energy_derivative_le line 297
  23. theorem OAI.PeriodicLattice.TorusCalculus.classical_velocity_unique line 327
  24. theorem OAI.PeriodicLattice.TorusCalculus.classical_pressure_unique line 354
  25. theorem OAI.PeriodicLattice.TorusCalculus.classical_unique line 389