OAI/Analysis/PeriodicLattice/TorusIntegration.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Periodic integration and differentiation identities.

  1. instance OAI.PeriodicLattice.TorusCalculus.volume_haar line 19
  2. theorem OAI.PeriodicLattice.TorusCalculus.slice_continuous_iff line 27
  3. theorem OAI.PeriodicLattice.TorusCalculus.slice_contDiff_spaceD line 31
  4. theorem OAI.PeriodicLattice.TorusCalculus.translation_hasDerivAt line 42
  5. theorem OAI.PeriodicLattice.TorusCalculus.integral_spaceD_of_continuous line 59
  6. theorem OAI.PeriodicLattice.TorusCalculus.integral_spaceD_C1 line 86
  7. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_add line 94
  8. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_sub line 102
  9. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_inner line 115
  10. theorem OAI.PeriodicLattice.TorusCalculus.integration_by_parts line 124
  11. theorem OAI.PeriodicLattice.TorusCalculus.integral_inner_laplacian line 143
  12. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_congr_slice line 168
  13. theorem OAI.PeriodicLattice.TorusCalculus.laplacian_sub line 174
  14. theorem OAI.PeriodicLattice.TorusCalculus.eq_zero_of_integral_norm_sq_eq_zero line 188
  15. theorem OAI.PeriodicLattice.TorusCalculus.spatially_constant_of_partials_zero line 199
  16. theorem OAI.PeriodicLattice.TorusCalculus.harmonic_constant line 215
  17. theorem OAI.PeriodicLattice.TorusCalculus.harmonic_meanZero_eq_zero line 231
  18. theorem OAI.PeriodicLattice.TorusCalculus.poisson_unique line 238
  19. theorem OAI.PeriodicLattice.TorusCalculus.cylinder_slice_continuous line 264
  20. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_component line 270
  21. theorem OAI.PeriodicLattice.TorusCalculus.contDiff_component_slice line 277
  22. theorem OAI.PeriodicLattice.TorusCalculus.spaceD_smul_slice line 282
  23. def OAI.PeriodicLattice.TorusCalculus.transport line 292
  24. theorem OAI.PeriodicLattice.TorusCalculus.transport_continuous line 295
  25. theorem OAI.PeriodicLattice.TorusCalculus.transport_eq_divergence_tensor line 304
  26. theorem OAI.PeriodicLattice.TorusCalculus.integral_inner_transport line 315
  27. theorem OAI.PeriodicLattice.TorusCalculus.integral_inner_transport_self line 351
  28. theorem OAI.PeriodicLattice.TorusCalculus.integral_inner_gradient line 363