OAI/MathematicalPhysics/BFSS/RellichCompactness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Totally bounded smoothing families and local Rellich compactness.

  1. theorem OAI.BFSSRellich.lipschitz_family_totallyBounded line 15
  2. theorem OAI.BFSSRellich.kernel_family_totallyBounded line 34
  3. lemma OAI.BFSSRellich.totallyBounded_of_uniform_approximation line 58
  4. lemma OAI.BFSSRellich.opNorm_sq_le_coordinate_sum line 74
  5. lemma OAI.BFSSRellich.integral_norm_le_volume_add_square line 101
  6. lemma OAI.BFSSRellich.continuousLp_dist_square line 131
  7. instance OAI.BFSSRellich.compact_comap_finite line 142
  8. def OAI.BFSSRellich.localLp line 149
  9. lemma OAI.BFSSRellich.localLp_dist_square line 154
  10. theorem OAI.BFSSRellich.localRellich line 163