OAI/MathematicalPhysics/BFSS/DeformedCharge.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Deformed smooth charges and quadratic-linear derivative estimates.

  1. def OAI.BFSSQuantum.AlgebraData.kineticSkewSymbol line 14
  2. def OAI.BFSSQuantum.AlgebraData.deformedRealField line 18
  3. lemma OAI.BFSSQuantum.AlgebraData.deformedRealField_contDiff line 22
  4. lemma OAI.BFSSQuantum.AlgebraData.kineticSkewSymbol_skew line 27
  5. lemma OAI.BFSSQuantum.AlgebraData.deformedRealField_selfAdjoint line 40
  6. lemma OAI.BFSSQuantum.AlgebraData.deformedRealField_anticommutator line 48
  7. def OAI.BFSSQuantum.AlgebraData.deformedCoreCharge line 61
  8. lemma OAI.BFSSQuantum.AlgebraData.kineticSkewCore_eq line 65
  9. lemma OAI.BFSSQuantum.AlgebraData.deformedCoreCharge_apply line 75
  10. lemma OAI.BFSSQuantum.AlgebraData.kineticSkewCore_norm line 82
  11. def OAI.BFSSQuantum.AlgebraData.deformedFermionField line 90
  12. lemma OAI.BFSSQuantum.AlgebraData.averaged_core_energy line 93
  13. lemma OAI.BilinearGrowth.derivative_quadratic_linear line 158
  14. lemma OAI.BilinearGrowth.derivative_quadratic_linear_bound line 170