OAI/Geometry/IsometricImmersion/Energy/MultiplierIntegral.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Weighted.boxPoint line 16
  2. def OAI.SmoothLocal.Weighted.closedRectangle line 19
  3. def OAI.SmoothLocal.Weighted.rectangleIntegral line 22
  4. def OAI.SmoothLocal.Weighted.zeroRectangleBoundary line 25
  5. theorem OAI.SmoothLocal.Weighted.boxPoint_mem line 29
  6. theorem OAI.SmoothLocal.Weighted.boxPoint_hasDerivAt_t line 34
  7. theorem OAI.SmoothLocal.Weighted.boxPoint_hasDerivAt_s line 40
  8. theorem OAI.SmoothLocal.Weighted.rectangle_area_integrable line 50
  9. theorem OAI.SmoothLocal.Weighted.rectangleIntegral_swap line 60
  10. theorem OAI.SmoothLocal.Weighted.rectangleIntegral_eq_area line 69
  11. theorem OAI.SmoothLocal.Weighted.rectangleIntegral_congr line 81
  12. theorem OAI.SmoothLocal.Weighted.rectangleIntegral_add line 93
  13. theorem OAI.SmoothLocal.Weighted.rectangleIntegral_partial_t_zero line 105
  14. theorem OAI.SmoothLocal.Weighted.rectangleIntegral_partial_s_zero line 134
  15. def OAI.SmoothLocal.Weighted.multiplierQuadratic line 163
  16. theorem OAI.SmoothLocal.Weighted.multiplierTestProduct_contDiffOn line 168
  17. theorem OAI.SmoothLocal.Weighted.multiplierFluxes_contDiffOn line 184
  18. theorem OAI.SmoothLocal.Weighted.multiplierQuadratic_contDiffOn line 200
  19. theorem OAI.SmoothLocal.Weighted.multiplier_integrands_integrable line 225
  20. theorem OAI.SmoothLocal.Weighted.integrated_multiplier_identity line 241
  21. def OAI.SmoothLocal.Weighted.cutoffM line 295
  22. def OAI.SmoothLocal.Weighted.cutoffN line 298
  23. theorem OAI.SmoothLocal.Weighted.cutoff_test_factor line 301
  24. theorem OAI.SmoothLocal.Weighted.integrated_cutoff_directed_identity line 309