OAI/Analysis/CoulombIonization/FieldAnalysis/LocalFieldScalarBoundBarrier.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.localFieldScale_linear_bound line 13
  2. lemma OAI.CoulombAtom.thinFieldBase_linear_bound line 41
  3. def OAI.CoulombAtom.radialOutLinearConstant line 63
  4. lemma OAI.CoulombAtom.radialOutLinearConstant_one_le line 66
  5. lemma OAI.CoulombAtom.thinOutMajorant_linear_bound line 75
  6. lemma OAI.CoulombAtom.thinFieldBase_collar_bound line 111
  7. def OAI.CoulombAtom.actualCellMomentConstant line 140
  8. lemma OAI.CoulombAtom.actualCellMomentConstant_one_le line 141
  9. lemma OAI.CoulombAtom.priced_enlarged_cell_count line 147
  10. def OAI.CoulombAtom.sharpFreshFieldConstant line 160
  11. lemma OAI.CoulombAtom.sharpFreshFieldConstant_one_le line 162
  12. lemma OAI.CoulombAtom.sharpFreshField_square line 171
  13. theorem OAI.CoulombAtom.sharp_cell_fresh_field_mass line 190