OAI/Analysis/CoulombRadii/RandomFields/ObservationProductDensity.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.setIntegral_abs_pow_le line 15
  2. theorem OAI.NeutralAtom.square_le_log_fifth_of_moments line 45
  3. theorem OAI.NeutralAtom.observationScorePi_event_bound line 93
  4. def OAI.NeutralAtom.observationProductDensity line 125
  5. theorem OAI.NeutralAtom.observationProductDensity_nonneg line 128
  6. theorem OAI.NeutralAtom.observationProductDensity_contDiff line 132
  7. theorem OAI.NeutralAtom.observationProductDensity_compact line 138
  8. theorem OAI.NeutralAtom.observationProductDensity_integrable line 151
  9. theorem OAI.NeutralAtom.observationProductDensity_even line 155
  10. theorem OAI.NeutralAtom.observationNoiseLaw_pi_density line 159
  11. theorem OAI.NeutralAtom.observationNoiseLaw_pi_integral line 179
  12. theorem OAI.NeutralAtom.observationProductDensity_fderiv line 187
  13. def OAI.NeutralAtom.observationEventLikelihood line 211
  14. theorem OAI.NeutralAtom.observationEventLikelihood_contDiff line 215
  15. theorem OAI.NeutralAtom.observationEventLikelihood_integral line 221
  16. theorem OAI.NeutralAtom.observationEventLikelihood_probability line 236
  17. theorem OAI.NeutralAtom.observationEventLikelihood_fderiv line 249
  18. theorem OAI.NeutralAtom.observationEventLikelihood_nonneg line 279
  19. theorem OAI.NeutralAtom.observationEventLikelihood_le_one line 285
  20. def OAI.NeutralAtom.observationScoreConstant line 291
  21. theorem OAI.NeutralAtom.observationScoreConstant_pos line 294
  22. theorem OAI.NeutralAtom.observationEventLikelihood_derivative_bound line 299
  23. theorem OAI.NeutralAtom.likelihood_log_fifth_majorant line 318
  24. theorem OAI.NeutralAtom.integral_likelihood_log_fifth line 361
  25. def OAI.NeutralAtom.coordinateLinear line 391
  26. theorem OAI.NeutralAtom.coordinateLinear_apply line 394
  27. def OAI.NeutralAtom.observationArrayCenter line 397
  28. def OAI.NeutralAtom.observationArrayRescale line 401
  29. def OAI.NeutralAtom.arrayEventLikelihood line 405
  30. theorem OAI.NeutralAtom.arrayEventLikelihood_contDiff line 409
  31. theorem OAI.NeutralAtom.arrayEventLikelihood_nonneg line 415