OAI/MathematicalPhysics/BFSS/WeightedCompactness.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Weighted tightness and compactness in local and global L2.

  1. def OAI.BFSSRellich.compactLp line 15
  2. lemma OAI.BFSSRellich.compactLp_ae line 20
  3. lemma OAI.BFSSRellich.compactLp_congr line 25
  4. lemma OAI.BFSSRellich.compactLp_dist_square line 32
  5. lemma OAI.BFSSRellich.compactLp_norm_square line 42
  6. lemma OAI.BFSSRellich.totallyBounded_range_of_dist_le line 50
  7. lemma OAI.BFSSRellich.compactLp_bump_dist_square_le line 70
  8. lemma OAI.BFSSRellich.compactLp_bump_error line 95
  9. lemma OAI.BFSSRellich.bump_family_totallyBounded line 122
  10. lemma OAI.BFSSRellich.compactLp_const_smul line 146
  11. lemma OAI.BFSSRellich.localLp_norm_square line 151
  12. lemma OAI.BFSSRellich.totallyBounded_of_tail line 161
  13. lemma OAI.BFSSRellich.totallyBounded_of_eventual_approximation line 169
  14. lemma OAI.BFSSRellich.weighted_bump_error line 186
  15. lemma OAI.BFSSRellich.continuous_weight_uniform_small line 206
  16. theorem OAI.BFSSRellich.weighted_tight_compactness line 219