OAI/MathematicalPhysics/BFSS/WeightedGradients.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Weighted smooth cutoff approximation and limiting profile gradients.

  1. theorem OAI.BFSSSliceSobolev.exists_small_weight_cutoff line 18
  2. def OAI.BFSSSliceSobolev.cutoffRatio line 34
  3. lemma OAI.BFSSSliceSobolev.cutoffRatio_continuous line 38
  4. lemma OAI.BFSSSliceSobolev.cutoffRatio_bound line 45
  5. lemma OAI.BFSSSliceSobolev.cutoffRatio_zero line 54
  6. lemma OAI.BFSSSliceSobolev.cutoffRatio_mul line 60
  7. theorem OAI.BFSSSliceSobolev.smooth_raw_tendsto line 74
  8. lemma OAI.BFSSSliceSobolev.op_derivative_sq_integrable line 117
  9. theorem OAI.BFSSSliceSobolev.scaledCutoff_gradient_bound line 129
  10. theorem OAI.BFSSSliceSobolev.local_bounds_closedGradient line 183
  11. def OAI.BFSSQuantum.AlgebraData.normalCoordinateCore line 243
  12. lemma OAI.BFSSQuantum.AlgebraData.normalCoordinateCore_apply line 248
  13. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.normalCoordinateCore_local_bounds line 264
  14. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.coordinateWeight_zero_pos line 305
  15. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_limit_gradient line 310