OAI/Analysis/CoulombIonization/FieldAnalysis/ThinFieldFeedbackBarrier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.thinFieldBase line 15
2. def OAI.CoulombAtom.thinOutMajorant line 17
3. def OAI.CoulombAtom.thinFieldMajorant line 20
4. lemma OAI.CoulombAtom.CoreObservationEnsemble.thin_observe_field line 25
5. lemma OAI.CoulombAtom.CoreObservationEnsemble.thin_out_feedback line 61
6. theorem OAI.CoulombAtom.CoreObservationEnsemble.thin_out_bound line 92
7. theorem OAI.CoulombAtom.CoreObservationEnsemble.thin_field_bound line 114
8. lemma OAI.CoulombAtom.core_field_sq_le_ball_average line 138