OAI/Geometry/Perimeter/Regularity/ExistsCompactTraceOnBounded.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPI.Boundary.exists_compact_trace_on_bounded line 11
  2. theorem OAI.RPI.Boundary.exists_compact_approximants_of_mem_sobolevGraph line 35
  3. def OAI.RPI.modelCapacityBump line 84
  4. def OAI.RPI.ballCapacityCutoff line 87
  5. theorem OAI.RPI.ballCapacityCutoff_contDiff line 90
  6. theorem OAI.RPI.ballCapacityCutoff_mem_Icc line 96
  7. theorem OAI.RPI.ballCapacityCutoff_zero line 102
  8. theorem OAI.RPI.ballCapacityCutoff_one line 111
  9. theorem OAI.RPI.exists_ballCapacityCutoff_gradient_bound line 120
  10. theorem OAI.RPI.ballCapacityCutoff_gradient_zero line 155
  11. def OAI.RPI.capacityGate line 170
  12. def OAI.RPI.bumpScore line 173
  13. def OAI.RPI.smoothCutoffAggregate line 176
  14. theorem OAI.RPI.bumpScore_nonneg line 180
  15. theorem OAI.RPI.smoothCutoffAggregate_contDiff line 185
  16. theorem OAI.RPI.smoothCutoffAggregate_mem_Icc line 193
  17. theorem OAI.RPI.smoothCutoffAggregate_zero line 198
  18. theorem OAI.RPI.smoothCutoffAggregate_zero_of_one line 204
  19. theorem OAI.RPI.smoothCutoffAggregate_one line 213
  20. theorem OAI.RPI.norm_sum_smul_sq_le line 224
  21. theorem OAI.RPI.bumpScore_fderiv line 239
  22. theorem OAI.RPI.bumpScore_norm_fderiv_sq_le line 250
  23. theorem OAI.RPI.exists_smoothCutoffAggregate_gradient_bound line 261
  24. def OAI.RPI.smoothDirichletEnergy line 322
  25. theorem OAI.RPI.smoothDirichletEnergy_le_ball line 325
  26. def OAI.RPI.innerCapacityBump line 344
  27. theorem OAI.RPI.innerCapacityBump_contDiff line 348
  28. theorem OAI.RPI.innerCapacityBump_gradient line 353
  29. theorem OAI.RPI.innerCapacityBump_one line 360
  30. theorem OAI.RPI.innerCapacityBump_zero line 365
  31. theorem OAI.RPI.innerCapacityBump_energy_le line 369
  32. theorem OAI.RPI.smoothCutoffAggregate_energy_le line 381