OAI/Analysis/PeriodicLattice/TorusDerivatives.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Translation derivatives and smooth periodic lifts.

  1. theorem OAI.PeriodicLattice.TorusCalculus.mk_isOpenQuotientMap line 18
  2. theorem OAI.PeriodicLattice.TorusCalculus.continuous_iff_lifted line 23
  3. theorem OAI.PeriodicLattice.TorusCalculus.single_eq_smul line 28
  4. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_eq_fderiv line 37
  5. theorem OAI.PeriodicLattice.TorusCalculus.contDiff_spaceD line 51
  6. def OAI.PeriodicLattice.TorusCalculus.fullTimeD line 67
  7. theorem OAI.PeriodicLattice.TorusCalculus.contDiff_fullTimeD line 69
  8. theorem OAI.PeriodicLattice.TorusCalculus.timeD_eq_fullTimeD line 76
  9. theorem OAI.PeriodicLattice.TorusCalculus.contDiff_laplacian line 83
  10. theorem OAI.PeriodicLattice.TorusCalculus.cylinderContinuous line 88
  11. theorem OAI.PeriodicLattice.TorusCalculus.timeD_cylinderContinuous line 91
  12. theorem OAI.PeriodicLattice.TorusCalculus.contDiff_advection line 100
  13. theorem OAI.PeriodicLattice.TorusCalculus.classical_of_smooth line 109
  14. theorem OAI.PeriodicLattice.TorusCalculus.mk_zero line 136
  15. theorem OAI.PeriodicLattice.TorusCalculus.single_zero line 140
  16. instance OAI.PeriodicLattice.TorusCalculus.volume_probability line 145
  17. instance OAI.PeriodicLattice.TorusCalculus.volume_rightInvariant line 149
  18. theorem OAI.PeriodicLattice.TorusCalculus.slice_integrable line 157
  19. theorem OAI.PeriodicLattice.TorusCalculus.smooth_slice_integrable line 162
  20. theorem OAI.PeriodicLattice.TorusCalculus.hasDerivAt_translation line 166
  21. theorem OAI.PeriodicLattice.TorusCalculus.integral_spaceD line 185
  22. theorem OAI.PeriodicLattice.TorusCalculus.integral_laplacian line 212
  23. def OAI.PeriodicLattice.Residual.fullForce line 227
  24. theorem OAI.PeriodicLattice.Residual.fullForce_contDiff line 230
  25. theorem OAI.PeriodicLattice.Residual.fullForce_eq line 235
  26. theorem OAI.PeriodicLattice.Residual.fullForce_equations line 239
  27. def OAI.PeriodicLattice.FluidLift.force line 254
  28. theorem OAI.PeriodicLattice.FluidLift.force_contDiff line 256
  29. theorem OAI.PeriodicLattice.FluidLift.force_smooth line 259
  30. theorem OAI.PeriodicLattice.FluidLift.equations line 262
  31. theorem OAI.PeriodicLattice.FluidLift.classical_solution line 265
  32. theorem OAI.PeriodicLattice.TorusCalculus.contDiff_component line 276
  33. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_smul line 280
  34. theorem OAI.PeriodicLattice.TorusCalculus.advection_eq_tensor_divergence line 289
  35. theorem OAI.PeriodicLattice.TorusCalculus.integral_advection line 297
  36. theorem OAI.PeriodicLattice.FluidLift.timeDerivative_half_shift line 314
  37. theorem OAI.PeriodicLattice.FluidLift.integral_timeDerivative line 321
  38. theorem OAI.PeriodicLattice.FluidLift.force_meanZero line 325
  39. theorem OAI.PeriodicLattice.FluidLift.residual_computation line 338