OAI/MathematicalPhysics/BFSS/SobolevGraphs.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Closed vector-valued gradient graphs and scaled smooth cutoffs.

  1. abbrev OAI.BFSSSliceSobolev.Core line 15
  2. def OAI.BFSSSliceSobolev.toL2 line 17
  3. lemma OAI.BFSSSliceSobolev.toL2_ae line 23
  4. lemma OAI.BFSSSliceSobolev.toL2_norm_sq line 27
  5. abbrev OAI.BFSSSliceSobolev.Gradient line 34
  6. def OAI.BFSSSliceSobolev.gradient line 36
  7. lemma OAI.BFSSSliceSobolev.gradient_apply line 41
  8. lemma OAI.BFSSSliceSobolev.norm_sq_compact line 46
  9. lemma OAI.BFSSSliceSobolev.derivative_sq_integrable line 54
  10. lemma OAI.BFSSSliceSobolev.gradient_norm_sq line 65
  11. def OAI.BFSSSliceSobolev.graph line 78
  12. def OAI.BFSSSliceSobolev.closedGraph line 81
  13. lemma OAI.BFSSSliceSobolev.core_mem_closedGraph line 85
  14. theorem OAI.BFSSSliceSobolev.closedGraph_extract line 101
  15. lemma OAI.BFSSSliceSobolev.toL2_inner line 138
  16. lemma OAI.BFSSSliceSobolev.core_inner_integrable line 146
  17. lemma OAI.BFSSSliceSobolev.directionalDerivative_skew line 152
  18. lemma OAI.BFSSSliceSobolev.toL2_dense line 163
  19. lemma OAI.BFSSSliceSobolev.closedGraph_pairing line 170
  20. lemma OAI.BFSSSliceSobolev.closedGraph_vertical line 186
  21. def OAI.BFSSSliceSobolev.scaledCutoff line 202
  22. lemma OAI.BFSSSliceSobolev.scaledCutoff_apply line 208
  23. lemma OAI.BFSSSliceSobolev.scaledCutoff_support line 211
  24. lemma OAI.BFSSSliceSobolev.scaledCutoff_fderiv line 224
  25. lemma OAI.BFSSSliceSobolev.scaledCutoff_fderiv_bound line 243