OAI/Analysis/PeriodicLattice/RapidBounds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Rapid decay estimates for all profile derivatives.

  1. structure OAI.PeriodicLattice.RapidCalculus.BoundedProfile line 19
  2. theorem OAI.PeriodicLattice.RapidCalculus.BoundedProfile.deriv line 23
  3. theorem OAI.PeriodicLattice.RapidCalculus.BoundedProfile.neg line 28
  4. inductive OAI.PeriodicLattice.RapidCalculus.Algebra line 34
  5. theorem OAI.PeriodicLattice.RapidCalculus.Algebra.smooth line 43
  6. theorem OAI.PeriodicLattice.RapidCalculus.Algebra.bound line 56
  7. theorem OAI.PeriodicLattice.RapidCalculus.tensor_spaceD_zero line 99
  8. theorem OAI.PeriodicLattice.RapidCalculus.tensor_spaceD_one line 108
  9. theorem OAI.PeriodicLattice.RapidCalculus.tensor_spaceD_two line 119
  10. theorem OAI.PeriodicLattice.RapidCalculus.tensor_fullTimeD line 130
  11. theorem OAI.PeriodicLattice.RapidCalculus.Algebra.spaceDeriv line 137
  12. theorem OAI.PeriodicLattice.RapidCalculus.Algebra.timeDeriv line 166
  13. theorem OAI.PeriodicLattice.RapidCalculus.boundedProfile_of_periodic line 197
  14. def OAI.PeriodicLattice.RapidCalculus.VectorAlgebra line 209
  15. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.smooth line 211
  16. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.spaceDeriv line 214
  17. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.timeDeriv line 223
  18. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.add line 233
  19. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.scale line 236
  20. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.sub line 239
  21. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.diffusion line 244
  22. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.selfTransport line 252
  23. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.fullForce line 265
  24. theorem OAI.PeriodicLattice.RapidCalculus.norm_le_sum_components line 268
  25. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.bound line 277
  26. theorem OAI.PeriodicLattice.RapidCalculus.iterate_timeD_eq_fullTimeD line 287
  27. theorem OAI.PeriodicLattice.RapidCalculus.VectorAlgebra.mixed_bound line 302
  28. theorem OAI.PeriodicLattice.RapidCalculus.rapidPair_of_algebra line 322
  29. theorem OAI.PeriodicLattice.FluidLift.velocity_algebra line 349
  30. theorem OAI.PeriodicLattice.FluidLift.force_rapid line 358