OAI/Analysis/CoulombIonization/Localization/QuantumMultiplierLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.finite_product_integral line 17
  2. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.apply_rawDensity line 38
  3. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.apply_rawLaw line 48
  4. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.apply_norm_sq line 59
  5. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.deriv_component_integrable line 67
  6. lemma OAI.CoulombAtom.FermionLipschitzMultiplier.gradient_rawLaw line 82
  7. lemma OAI.CoulombObservation.event_raw_marginal line 107
  8. lemma OAI.CoulombObservation.event_probability_lintegral line 128
  9. def OAI.CoulombAtom.quantumObservationEvent line 144
  10. lemma OAI.CoulombAtom.quantumObservationEvent_measurable line 149
  11. lemma OAI.CoulombAtom.quantumEventLikelihood_ofReal line 156
  12. lemma OAI.CoulombAtom.quantumEventProbability_ofReal line 166
  13. lemma OAI.CoulombAtom.quantumEventMultiplier_rawLaw line 181