OAI/Analysis/CoulombRadii/FieldAnalysis/HighProjection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.fiberContract_lowProjection line 18
  2. def OAI.Coulomb.highProjection line 35
  3. lemma OAI.Coulomb.highProjection_memLp line 39
  4. lemma OAI.Coulomb.fiberContract_highProjection line 48
  5. lemma OAI.Coulomb.fiberContract_finite_bessel line 65
  6. lemma OAI.Coulomb.fiberContract_norm_summable line 79
  7. def OAI.Coulomb.firstUnfiber line 86
  8. lemma OAI.Coulomb.firstFiber_firstUnfiber line 89
  9. lemma OAI.Coulomb.firstUnfiber_memLp line 94
  10. lemma OAI.Coulomb.firstUnfiber_norm_sq line 109
  11. lemma OAI.Coulomb.scalarCoefficient_congr line 120
  12. lemma OAI.Coulomb.scalarCoefficient_highFirst line 133
  13. lemma OAI.Coulomb.highProjection_norm_spectrum line 156