OAI/MathematicalPhysics/BFSS/SharpCutoffs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Sharp weighted cutoff bounds and joint gradient lower limits.

  1. lemma OAI.BFSSSliceSobolev.closedGraph_unique line 19
  2. theorem OAI.BFSSSliceSobolev.closedGraph_norm_sq_add_le line 25
  3. lemma OAI.BFSSSliceSobolev.norm_add_sq_young line 51
  4. lemma OAI.BFSSSliceSobolev.scaledCutoff_fderiv_young line 66
  5. theorem OAI.BFSSSliceSobolev.scaledCutoff_sharp_bound line 92
  6. lemma OAI.BFSSSliceSobolev.exists_sharp_weight_cutoff line 189
  7. theorem OAI.BFSSSliceSobolev.weighted_gradient_add_liminf line 214
  8. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_gradient_add_le_limit line 308