OAI/MathematicalPhysics/BFSS/KineticMeasures.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Gauge-invariant kinetic density and measured normal kinetic estimates.

  1. def OAI.BFSSQuantum.AlgebraData.kineticDensity line 15
  2. lemma OAI.BFSSQuantum.AlgebraData.kineticDensity_integral line 18
  3. lemma OAI.BFSSQuantum.AlgebraData.normalCoreField_kinetic_le line 24
  4. lemma OAI.BFSSQuantum.AlgebraData.kineticDensity_continuous line 45
  5. lemma OAI.BFSSQuantum.AlgebraData.kineticDensity_nonneg line 48
  6. lemma OAI.BFSSQuantum.AlgebraData.kineticDensity_compactSupport line 51
  7. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_kineticDensity line 65
  8. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_kineticDensity_unitary line 77
  9. def OAI.BFSSQuantum.AlgebraData.normalKineticDensity line 92
  10. lemma OAI.BFSSQuantum.AlgebraData.normalKineticDensity_continuous line 96
  11. lemma OAI.BFSSQuantum.AlgebraData.normalKineticDensity_compactSupport line 103
  12. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.slice_kinetic_integral_le line 113
  13. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalOrbit_kinetic line 178
  14. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.kinetic_le line 204
  15. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.kinetic_le_total line 213
  16. lemma OAI.BFSSQuantum.AlgebraData.normalCoordinateCore_kinetic line 243
  17. lemma OAI.BFSSQuantum.AlgebraData.normalCoordinateCore_weighted_kinetic line 266