OAI/MathematicalPhysics/RapidForcing/Energy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.RapidForcing.compactSpace_K line 9
  2. def OAI.RapidForcing.boxExtension line 14
  3. lemma OAI.RapidForcing.boxExtension_mem line 18
  4. lemma OAI.RapidForcing.boxExtension_notMem line 23
  5. lemma OAI.RapidForcing.boxExtension_measurable line 30
  6. lemma OAI.RapidForcing.boxExtension_bound line 35
  7. lemma OAI.RapidForcing.boxExtension_memLp line 43
  8. def OAI.RapidForcing.boxToL2Linear line 48
  9. lemma OAI.RapidForcing.coe_boxToL2Linear line 71
  10. lemma OAI.RapidForcing.boxToL2Linear_bound line 75
  11. def OAI.RapidForcing.boxToL2 line 93
  12. lemma OAI.RapidForcing.coe_boxToL2 line 96
  13. lemma OAI.RapidForcing.hasDerivAt_continuousMap line 101
  14. def OAI.RapidForcing.boxCurve line 124
  15. lemma OAI.RapidForcing.boxCurve_apply line 130
  16. lemma OAI.RapidForcing.boxToL2_curve_coe line 133
  17. lemma OAI.RapidForcing.l2Continuous_of_continuous_supported line 143
  18. lemma OAI.RapidForcing.spatialMulti_joint_smooth line 151
  19. lemma OAI.RapidForcing.l2C1_of_smooth_supported line 166
  20. theorem OAI.RapidForcing.energyRegularity_of_smooth_supported line 194
  21. theorem OAI.RapidForcing.addressed_energyClass line 207