OAI/MathematicalPhysics/BFSS/EnergyLimits.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Moment-controlled quadratic fields and limiting profile energies.

  1. lemma OAI.BFSSNormalAnalysis.field_memLp_moment line 17
  2. lemma OAI.BFSSNormalAnalysis.field_moment_norm_le line 32
  3. lemma OAI.BFSSNormalAnalysis.field_quadratic_integrable line 46
  4. lemma OAI.BFSSNormalAnalysis.field_quadratic_abs_le line 54
  5. lemma OAI.BFSSNormalAnalysis.constant_quadratic_eq line 72
  6. lemma OAI.BFSSNormalAnalysis.constant_quadratic_tendsto line 80
  7. theorem OAI.BFSSNormalAnalysis.affine_quadratic_tendsto line 88
  8. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_moment_norm_le line 132
  9. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_fermion_energy_tendsto line 147
  10. theorem OAI.BFSSNormalAnalysis.varying_weight_norm_sq_le_limit line 194
  11. lemma OAI.BFSSQuantum.AlgebraData.normalEffectivePotential_nonneg line 234
  12. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_potential_mem line 250
  13. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_potential_norm_sq line 268
  14. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_bosonic_energy_le_limit line 279
  15. lemma OAI.BFSSSliceAnalytic.contraction_basis_independent line 316