OAI/Analysis/PeriodicLattice/Solenoidal.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Pressure potentials, solenoidal forcing and the analytic lattice conclusion.

  1. def OAI.PeriodicLattice.FluidLift.doubleSlope line 19
  2. theorem OAI.PeriodicLattice.FluidLift.doubleSlope_contDiff line 21
  3. theorem OAI.PeriodicLattice.FluidLift.doubleSlope_periodic line 24
  4. theorem OAI.PeriodicLattice.FluidLift.slope_hasDerivAt line 28
  5. theorem OAI.PeriodicLattice.FluidLift.eta_deriv line 37
  6. theorem OAI.PeriodicLattice.FluidLift.slope_deriv line 38
  7. theorem OAI.PeriodicLattice.FluidLift.vertical_energy line 41
  8. theorem OAI.PeriodicLattice.FluidLift.doubleSlope_second line 46
  9. def OAI.PeriodicLattice.FluidLift.pressureSource line 58
  10. theorem OAI.PeriodicLattice.FluidLift.pressureSource_contDiff line 61
  11. theorem OAI.PeriodicLattice.FluidLift.pressureSource_periodic line 66
  12. theorem OAI.PeriodicLattice.FluidLift.pressureSource_rapid line 71
  13. theorem OAI.PeriodicLattice.RapidCalculus.tensor_contDiff line 82
  14. theorem OAI.PeriodicLattice.RapidCalculus.tensor_laplacian line 91
  15. def OAI.PeriodicLattice.FluidLift.pressureBase line 109
  16. theorem OAI.PeriodicLattice.FluidLift.pressureBase_contDiff line 112
  17. theorem OAI.PeriodicLattice.FluidLift.pressureBase_periodic line 116
  18. theorem OAI.PeriodicLattice.FluidLift.pressureBase_rapid line 120
  19. theorem OAI.PeriodicLattice.FluidLift.pressureBase_deriv line 124
  20. theorem OAI.PeriodicLattice.FluidLift.pressureBase_second line 133
  21. def OAI.PeriodicLattice.FluidLift.pressureMode line 140
  22. theorem OAI.PeriodicLattice.FluidLift.pressureMode_contDiff line 142
  23. theorem OAI.PeriodicLattice.FluidLift.pressureMode_periodic line 145
  24. theorem OAI.PeriodicLattice.FluidLift.pressureMode_rapid line 148
  25. def OAI.PeriodicLattice.FluidLift.pressureOsc line 151
  26. theorem OAI.PeriodicLattice.FluidLift.pressureOsc_cover line 154
  27. theorem OAI.PeriodicLattice.FluidLift.pressureOsc_contDiff line 158
  28. theorem OAI.PeriodicLattice.FluidLift.pressureOsc_algebra line 161
  29. def OAI.PeriodicLattice.FluidLift.potential line 165
  30. theorem OAI.PeriodicLattice.FluidLift.potential_contDiff line 168
  31. theorem OAI.PeriodicLattice.FluidLift.potential_algebra line 171
  32. theorem OAI.PeriodicLattice.FluidLift.potential_meanZero line 174
  33. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_add_eq line 211
  34. theorem OAI.PeriodicLattice.TorusCalculus.laplacian_add line 217
  35. theorem OAI.PeriodicLattice.FluidLift.force_divergence line 231
  36. theorem OAI.PeriodicLattice.FluidLift.potential_poisson line 261
  37. theorem OAI.PeriodicLattice.TorusCalculus.contDiff_gradient line 289
  38. theorem OAI.PeriodicLattice.TorusCalculus.divergence_gradient line 293
  39. theorem OAI.PeriodicLattice.TorusCalculus.gradient_neg line 295
  40. theorem OAI.PeriodicLattice.TorusCalculus.integral_gradient line 300
  41. theorem OAI.PeriodicLattice.TorusCalculus.classical_of_smooth_pressure line 308
  42. def OAI.PeriodicLattice.FluidLift.solenoidalForce line 334
  43. theorem OAI.PeriodicLattice.FluidLift.solenoidalForce_contDiff line 336
  44. theorem OAI.PeriodicLattice.FluidLift.solenoidalForce_solenoidal line 340
  45. theorem OAI.PeriodicLattice.FluidLift.solenoidalForce_meanZero line 348
  46. theorem OAI.PeriodicLattice.FluidLift.solenoidalForce_equations line 355
  47. theorem OAI.PeriodicLattice.FluidLift.solenoidalForce_classical_solution line 366
  48. theorem OAI.PeriodicLattice.FluidLift.gradient_algebra line 374
  49. theorem OAI.PeriodicLattice.FluidLift.solenoidalForce_algebra line 377
  50. theorem OAI.PeriodicLattice.RapidCalculus.RapidPair.mono line 385
  51. theorem OAI.PeriodicLattice.FluidLift.analytic_lattice_conclusion line 398