OAI/Analysis/CoulombIonization/FieldAnalysis/LocalFieldBootstrapBarrier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.localHistory_field_bound line 16
  2. lemma OAI.CoulombAtom.localFieldEnvelope_quadratic line 52
  3. theorem OAI.CoulombAtom.ensemble_local_field_estimate line 81
  4. def OAI.CoulombAtom.localFieldScale line 105
  5. def OAI.CoulombAtom.localFieldUniversalConstant line 108
  6. lemma OAI.CoulombAtom.localFieldUniversalConstant_pos line 111
  7. lemma OAI.CoulombAtom.localFieldScale_nonneg line 117
  8. lemma OAI.CoulombAtom.sqrt_count_reciprocal_young line 120
  9. lemma OAI.CoulombAtom.localFieldScale_mono line 129
  10. lemma OAI.CoulombAtom.field_explicit_bound_le_scale line 135
  11. theorem OAI.CoulombAtom.ensemble_local_field_scale line 170