OAI/Geometry/Perimeter/Regularity/VectorEnergy.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RPI.vectorEnergy line 14
  2. theorem OAI.RPI.memLp_two_iff_vectorEnergy line 17
  3. theorem OAI.RPI.eLpNorm_two_eq_vectorEnergy_rpow line 25
  4. theorem OAI.RPI.eLpNorm_two_eq_vectorEnergy_rpow_of_aestronglyMeasurable line 33
  5. theorem OAI.RPI.vectorEnergy_le_of_ae_tendsto line 40
  6. theorem OAI.RPI.tendsto_eLpNorm_two_of_vectorEnergy_zero line 59
  7. theorem OAI.RPI.tendsto_eLpNorm_two_toReal_of_vectorEnergy_zero line 66
  8. theorem OAI.RPI.tendsto_eLpNorm_two_of_vectorEnergy_zero_of_aestronglyMeasurable line 73
  9. theorem OAI.RPI.tendsto_eLpNorm_two_toReal_of_vectorEnergy_zero_of_aestronglyMeasurable line 81
  10. theorem OAI.RPI.vectorEnergy_bounded_smul line 95
  11. theorem OAI.RPI.vectorEnergy_add_le line 110
  12. theorem OAI.RPI.vectorEnergy_omitted_tendsto_zero line 141
  13. theorem OAI.RPI.vectorEnergy_bounded_smul_tendsto_zero line 167
  14. theorem OAI.RPI.memLp_of_capacity_energy_bounds line 177
  15. theorem OAI.RPI.capacity_productGradient_tendsto line 196
  16. theorem OAI.RPI.capacity_product_pair_tendsto line 232
  17. theorem OAI.RPI.truncation_test_pointwise line 298
  18. theorem OAI.RPI.truncation_test_energy line 308
  19. theorem OAI.RPI.Boundary.capacity_trace_mem_sobolevGraph line 349
  20. theorem OAI.RPI.vectorEnergy_eq_enorm_toLp_sq line 399
  21. theorem OAI.RPI.vectorEnergy_tendsto_of_toLp_tendsto line 406
  22. theorem OAI.RPI.memLp_of_regular_caccioppoli line 418