OAI/MathematicalPhysics/BFSS/MassiveCoercivity.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Matrix potential coercivity via normalized escaping configurations.

  1. abbrev OAI.BFSS.Mat line 13
  2. def OAI.BFSS.Color line 15
  3. abbrev OAI.BFSS.Configuration line 17
  4. def OAI.BFSS.realBracket line 19
  5. def OAI.BFSS.hsNormSq line 22
  6. def OAI.BFSS.configurationNormSq line 25
  7. def OAI.BFSS.massivePotential line 28
  8. def OAI.BFSS.MassiveCoercivity line 36
  9. lemma OAI.BFSS.hsNormSq_nonneg line 41
  10. lemma OAI.BFSS.hsNormSq_real_smul line 44
  11. lemma OAI.BFSS.hsNormSq_complex_smul line 49
  12. lemma OAI.BFSS.hsNormSq_trace line 54
  13. lemma OAI.BFSS.hsNormSq_unitary line 65
  14. lemma OAI.BFSS.realBracket_real_smul line 83
  15. lemma OAI.BFSS.internal_commutator_trace line 92
  16. lemma OAI.BFSS.block_commutator_trace line 103
  17. lemma OAI.BFSS.tendsto_of_mul_tendsto line 118
  18. lemma OAI.BFSS.diagonal_escape_vanishes line 127
  19. lemma OAI.BFSS.hsNormSq_zero line 222
  20. lemma OAI.BFSS.normSq_entry_le_hsNormSq line 225
  21. lemma OAI.BFSS.norm_le_one_of_hsNormSq_le_one line 233
  22. lemma OAI.BFSS.continuous_hsNormSq line 241
  23. lemma OAI.BFSS.tendsto_entry_zero_of_hsNormSq line 249
  24. lemma OAI.BFSS.hsNormSq_conjStarAlgAut line 260
  25. lemma OAI.BFSS.realBracket_conjStarAlgAut line 265
  26. lemma OAI.BFSS.map_realBracket line 271
  27. lemma OAI.BFSS.normalized_triple_first_norm_zero line 275
  28. lemma OAI.BFSS.configurationNormSq_nonneg line 367
  29. lemma OAI.BFSS.hsNormSq_le_configurationNormSq line 370
  30. lemma OAI.BFSS.hsNormSq_ofReal_smul line 375
  31. lemma OAI.BFSS.massivePotential_bounds line 379
  32. theorem OAI.BFSS.massive_coercivity line 422