OAI/Analysis/PeriodicLattice/MeanBounds.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Mean-zero corrections and rapid derivative bounds.

  1. def OAI.PeriodicLattice.PeriodicInverse.mean line 18
  2. theorem OAI.PeriodicLattice.PeriodicInverse.mean_contDiff line 20
  3. theorem OAI.PeriodicLattice.PeriodicInverse.mean_periodic line 24
  4. theorem OAI.PeriodicLattice.PeriodicInverse.mean_timeD line 26
  5. theorem OAI.PeriodicLattice.PeriodicInverse.mean_spaceD line 31
  6. theorem OAI.PeriodicLattice.PeriodicInverse.biD_zero line 35
  7. theorem OAI.PeriodicLattice.PeriodicInverse.mean_wordD line 39
  8. theorem OAI.PeriodicLattice.PeriodicInverse.mean_rapid line 53
  9. theorem OAI.PeriodicLattice.TorusCalculus.directional_commute line 76
  10. theorem OAI.PeriodicLattice.TorusCalculus.lifted_spaceD_eq line 88
  11. theorem OAI.PeriodicLattice.TorusCalculus.lifted_fullTimeD_eq line 108
  12. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_commute line 115
  13. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_fullTimeD line 124
  14. theorem OAI.PeriodicLattice.TorusCalculus.smooth_slice_differentiable line 144
  15. theorem OAI.PeriodicLattice.TorusCalculus.fullTime_hasDerivAt line 148
  16. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_finite_sum line 153
  17. theorem OAI.PeriodicLattice.TorusCalculus.fullTimeD_finite_sum line 160
  18. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_scale line 166
  19. theorem OAI.PeriodicLattice.TorusCalculus.laplacian_as_sum line 172
  20. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_component_eq line 179
  21. theorem OAI.PeriodicLattice.TorusCalculus.fullTimeD_component_eq line 183
  22. theorem OAI.PeriodicLattice.TorusCalculus.divergence_as_sum line 189
  23. theorem OAI.PeriodicLattice.TorusCalculus.contDiff_divergence line 194
  24. theorem OAI.PeriodicLattice.TorusCalculus.divergence_fullTimeD line 198
  25. theorem OAI.PeriodicLattice.TorusCalculus.divergence_spaceD line 204
  26. theorem OAI.PeriodicLattice.TorusCalculus.divergence_finite_sum line 212
  27. theorem OAI.PeriodicLattice.TorusCalculus.divergence_laplacian line 222
  28. theorem OAI.PeriodicLattice.TorusCalculus.divergence_add line 227
  29. theorem OAI.PeriodicLattice.TorusCalculus.divergence_scale line 236
  30. theorem OAI.PeriodicLattice.TorusCalculus.divergence_fullForce line 243
  31. theorem OAI.PeriodicLattice.TorusCalculus.divergence_advection line 268
  32. def OAI.PeriodicLattice.PeriodicInverse.horizontal line 309
  33. theorem OAI.PeriodicLattice.PeriodicInverse.horizontal_cover line 312
  34. theorem OAI.PeriodicLattice.PeriodicInverse.horizontal_contDiff line 316
  35. theorem OAI.PeriodicLattice.PeriodicInverse.horizontal_algebra line 321
  36. theorem OAI.PeriodicLattice.PeriodicInverse.horizontal_integral line 328