OAI/Probability/GaussianReplacement/KernelVolume.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentProjection.KernelHistory line 16
  2. def OAI.CurrentProjection.kernelInverseVolume line 18
  3. lemma OAI.CurrentProjection.measurable_kernelInverseVolume line 22
  4. lemma OAI.CurrentProjection.measurable_snoc_history line 29
  5. lemma OAI.CurrentProjection.kernelInverseVolume_snoc line 38
  6. lemma OAI.CurrentProjection.measurableSet_kernel_nondegenerate line 55
  7. lemma OAI.CurrentProjection.kernel_nondegenerate_snoc line 65
  8. def OAI.CurrentProjection.kernelHistoryLaw line 82
  9. instance OAI.CurrentProjection.kernelHistoryLaw_probability line 88
  10. lemma OAI.CurrentProjection.kernelHistory_step line 99
  11. lemma OAI.CurrentProjection.kernelHistory_step_nondegenerate line 127
  12. theorem OAI.CurrentProjection.independent_kernel_inverse_volume line 146
  13. lemma OAI.CurrentProjection.independent_kernel_inverse_volume_pi line 196
  14. lemma OAI.CurrentProjection.span_image_diagonal_smul line 243
  15. lemma OAI.CurrentProjection.gramSchmidt_diagonal_smul line 258
  16. lemma OAI.CurrentProjection.kernelInverseVolume_normalization line 265
  17. def OAI.CurrentProjection.normalizeKernelVector line 288
  18. lemma OAI.CurrentProjection.measurable_normalizeKernelVector line 292
  19. lemma OAI.CurrentProjection.normalizeKernelVector_support line 298
  20. lemma OAI.CurrentProjection.gaussian_single_kernel_bound line 308
  21. lemma OAI.CurrentProjection.kernel_normalized_projection_moment line 329