OAI/MathematicalPhysics/BFSS/LocalL2.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Local L2 restriction and bounded varying multipliers.

  1. def OAI.BFSSLocalL2.restrictLinear line 14
  2. lemma OAI.BFSSLocalL2.restrictLinear_norm_le line 33
  3. def OAI.BFSSLocalL2.restrict line 38
  4. lemma OAI.BFSSLocalL2.restrict_ae line 41
  5. lemma OAI.BFSSLocalL2.norm_le_of_ae_norm_le line 46
  6. lemma OAI.BFSSLocalL2.norm_le_mul_of_ae_norm_le line 51
  7. lemma OAI.BFSSLocalL2.boundedMul_mem line 66
  8. def OAI.BFSSLocalL2.boundedMul line 75
  9. lemma OAI.BFSSLocalL2.boundedMul_ae line 79
  10. lemma OAI.BFSSLocalL2.boundedMul_dist_le line 86
  11. lemma OAI.BFSSLocalL2.lp_norm_sq line 97
  12. theorem OAI.BFSSLocalL2.boundedMul_fixed_tendsto line 101
  13. theorem OAI.BFSSLocalL2.boundedMul_tendsto line 139