OAI/MathematicalPhysics/BFSS/MeasuredFields.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Measured normal fields with uniform moment and derivative bounds.

  1. def OAI.BFSSQuantum.AlgebraData.normalMeasuredField line 15
  2. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredField_continuous line 19
  3. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredField_compactSupport line 30
  4. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredField_norm_sq line 36
  5. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredField_square_integrable line 50
  6. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredField_moment_integrable line 57
  7. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredField_tail_moment line 65
  8. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalMeasuredCore_uniform_bounds line 87