OAI/MathematicalPhysics/BFSS/CoreCompactness.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Normal-coordinate smooth fields and local compactness of core families.

  1. lemma OAI.BFSSQuantum.AlgebraData.derivative_integral_le_coordinate_sum line 17
  2. lemma OAI.BFSSSliceAnalytic.affine_contDiff line 42
  3. lemma OAI.BFSSSliceAnalytic.affine_compactSupport line 46
  4. lemma OAI.BFSSSliceAnalytic.affine_fderiv line 55
  5. lemma OAI.BFSSSliceAnalytic.affine_fderiv_norm_sq line 63
  6. def OAI.BFSSQuantum.AlgebraData.normalCoreField line 82
  7. lemma OAI.BFSSQuantum.AlgebraData.normalCoreField_contDiff line 85
  8. lemma OAI.BFSSQuantum.AlgebraData.normalCoreField_compactSupport line 89
  9. lemma OAI.BFSSQuantum.AlgebraData.normalCoreField_norm_sq line 93
  10. lemma OAI.BFSSQuantum.AlgebraData.normalCoreField_fderiv line 100
  11. lemma OAI.BFSSQuantum.AlgebraData.normalCoreField_fderiv_norm_sq line 109
  12. lemma OAI.BFSSQuantum.AlgebraData.normalCoreField_derivative_integrable line 119
  13. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalCoreField_local_bounds line 129
  14. lemma OAI.BFSSSliceAnalytic.isometry_fderiv_norm_le line 218
  15. lemma OAI.BFSSSliceAnalytic.isometry_closedBall_integral line 231
  16. lemma OAI.BFSSSliceAnalytic.isometry_derivative_integral_le line 241
  17. abbrev OAI.BFSSQuantum.AlgebraData.NormalCoordinates line 270
  18. def OAI.BFSSQuantum.AlgebraData.normalCoordinateIsometry line 273
  19. def OAI.BFSSQuantum.AlgebraData.normalCoordinateField line 276
  20. lemma OAI.BFSSQuantum.AlgebraData.normalCoordinateField_contDiff line 280
  21. lemma OAI.BFSSQuantum.AlgebraData.normalCoordinateField_integral line 284
  22. lemma OAI.BFSSQuantum.AlgebraData.normalCoordinateField_derivative_integral line 291
  23. theorem OAI.BFSSRellich.localRellich_on line 312
  24. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalCore_locallyCompact line 435