OAI/Analysis/CoulombIonization/RadialBounds/LocalDensityTraceBarrier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombLT.infiniteDensity_aemeasurable line 20
  2. lemma OAI.CoulombLT.family_trace_eq_lintegral line 25
  3. lemma OAI.CoulombLT.smoothMultiply_trace line 37
  4. lemma OAI.CoulombLT.complex_norm_add_sq_bound line 44
  5. lemma OAI.CoulombLT.smoothDerivative_density_bound line 48
  6. lemma OAI.CoulombLT.smoothDerivative_trace_bound line 77
  7. def OAI.CoulombLT.indexedFermionFamily line 105
  8. lemma OAI.CoulombLT.indexed_density_eq line 111
  9. lemma OAI.CoulombLT.indexed_density_weighted line 131
  10. def OAI.CoulombLT.coordinateWeightedTrace line 157
  11. lemma OAI.CoulombLT.fermionFamily_weighted line 162