OAI/Analysis/CoulombRadii/RandomFields/ObservationWidthSquareSum.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.arrayEventLikelihood_le_one line 16
  2. theorem OAI.NeutralAtom.arrayEventLikelihood_integral line 21
  3. def OAI.NeutralAtom.observationWidthSquareSum line 38
  4. theorem OAI.NeutralAtom.observationWidthSquareSum_nonneg line 41
  5. theorem OAI.NeutralAtom.arrayEventLikelihood_direction_bound line 44
  6. theorem OAI.NeutralAtom.configuration_coordinate_expansion line 68
  7. theorem OAI.NeutralAtom.arrayEventLikelihood_gradient_bound line 74
  8. def OAI.NeutralAtom.permuteObservationArray line 101
  9. theorem OAI.NeutralAtom.arrayEventLikelihood_symmetric line 105
  10. def OAI.NeutralAtom.eventRootDerivative line 134
  11. def OAI.NeutralAtom.regularizedEventRoot line 138
  12. theorem OAI.NeutralAtom.regularizedEventRoot_derivative line 141
  13. theorem OAI.NeutralAtom.root_gradient_square_bound line 153
  14. theorem OAI.NeutralAtom.eventRootDerivative_gradient_bound line 173
  15. theorem OAI.NeutralAtom.coordinate_square_le_sum line 182
  16. theorem OAI.NeutralAtom.regularizedEventRoot_tendsto line 188
  17. theorem OAI.NeutralAtom.likelihood_log_fifth_nonneg line 195
  18. theorem OAI.NeutralAtom.likelihood_log_fifth_bounded line 200
  19. theorem OAI.NeutralAtom.likelihood_gradient_zero line 206
  20. theorem OAI.NeutralAtom.regularizedEventRoot_contDiff line 216
  21. theorem OAI.NeutralAtom.regularizedEventRoot_bound line 222
  22. theorem OAI.NeutralAtom.regularizedEventRoot_derivative_bound line 233
  23. theorem OAI.NeutralAtom.regularizedEventRoot_derivative_tendsto line 254
  24. theorem OAI.NeutralAtom.eventRootDerivative_measurable line 269
  25. theorem OAI.NeutralAtom.eventRootDerivative_bound line 275
  26. theorem OAI.NeutralAtom.FormDomain.eventRoot line 288
  27. theorem OAI.NeutralAtom.likelihood_smoothMultiplier line 305
  28. theorem OAI.NeutralAtom.eventRoot_square_derivative line 323
  29. theorem OAI.NeutralAtom.stateWeighted_integrable line 336
  30. theorem OAI.NeutralAtom.stateWeightedIntegral_le_one line 343
  31. theorem OAI.NeutralAtom.stateWeightedIntegral_log_fifth line 355
  32. theorem OAI.NeutralAtom.explicitLocalizationError_eventRoot_le line 401