OAI/Analysis/CoulombIonization/Localization/TailObservationEventBarrier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.tailInvariantArraySpace line 16
2. lemma OAI.CoulombAtom.arrayObservationInformation_le_tailInvariant line 27
3. lemma OAI.CoulombAtom.observation_event_tail_representation line 43
4. def OAI.CoulombAtom.tailObservationCoefficient line 51
5. lemma OAI.CoulombAtom.tail_physicalObservationEvent_eq line 54
6. lemma OAI.CoulombAtom.tail_quantumEventProbability_eq_physical line 67
7. lemma OAI.CoulombObservation.geometric_tail_sum_le_two line 85
8. lemma OAI.CoulombAtom.tail_dyadicObservation_inv_sq_sum line 102
9. lemma OAI.CoulombAtom.tail_observationTiltEnergyCost_dyadic line 120