OAI/Analysis/PeriodicLattice/PeriodicInverse.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Periodic primitives and regularity of the inverse operator.

  1. theorem OAI.PeriodicLattice.PeriodicInverse.hasFDerivAt_intervalIntegral line 24
  2. theorem OAI.PeriodicLattice.PeriodicInverse.contDiff_intervalIntegral line 47
  3. theorem OAI.PeriodicLattice.PeriodicInverse.hasDerivAt_intervalIntegral line 70
  4. def OAI.PeriodicLattice.PeriodicInverse.first line 84
  5. theorem OAI.PeriodicLattice.PeriodicInverse.first_contDiff line 87
  6. theorem OAI.PeriodicLattice.PeriodicInverse.first_periodic line 96
  7. theorem OAI.PeriodicLattice.PeriodicInverse.first_space_deriv line 106
  8. theorem OAI.PeriodicLattice.PeriodicInverse.first_time_deriv line 122
  9. theorem OAI.PeriodicLattice.PeriodicInverse.first_biD line 137
  10. theorem OAI.PeriodicLattice.PeriodicInverse.first_wordD line 145
  11. theorem OAI.PeriodicLattice.PeriodicInverse.first_equation line 152
  12. theorem OAI.PeriodicLattice.PeriodicInverse.first_weighted_bound line 183
  13. theorem OAI.PeriodicLattice.PeriodicInverse.first_rapid line 211
  14. theorem OAI.PeriodicLattice.RapidCalculus.biD_add line 226
  15. theorem OAI.PeriodicLattice.RapidCalculus.wordD_add line 236
  16. theorem OAI.PeriodicLattice.RapidCalculus.biD_scale line 243
  17. theorem OAI.PeriodicLattice.RapidCalculus.wordD_scale line 251
  18. theorem OAI.PeriodicLattice.RapidCalculus.Rapid2.add line 258
  19. theorem OAI.PeriodicLattice.RapidCalculus.Rapid2.scale line 269
  20. theorem OAI.PeriodicLattice.RapidCalculus.Rapid2.neg line 278
  21. theorem OAI.PeriodicLattice.RapidCalculus.Rapid2.sub line 281
  22. theorem OAI.PeriodicLattice.RapidCalculus.biD_mul line 285
  23. theorem OAI.PeriodicLattice.RapidCalculus.Rapid2.mul line 295
  24. def OAI.PeriodicLattice.PeriodicInverse.screened line 328
  25. theorem OAI.PeriodicLattice.PeriodicInverse.screened_contDiff line 330
  26. theorem OAI.PeriodicLattice.PeriodicInverse.screened_periodic line 335
  27. theorem OAI.PeriodicLattice.PeriodicInverse.screened_rapid line 340
  28. theorem OAI.PeriodicLattice.PeriodicInverse.screened_equation line 343