OAI/Probability/LatticeSurface/Convexity/ElementaryKernels.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ClusterDisplacement.energy_difference line 15
  2. lemma OAI.ClusterDisplacement.firm_iff line 21
  3. def OAI.ClusterDisplacement.Kernel.mixture line 29
  4. lemma OAI.ClusterDisplacement.Kernel.mixture_apply line 43
  5. lemma OAI.ClusterDisplacement.Kernel.mixture_firm line 53
  6. def OAI.ClusterDisplacement.Kernel.cutoff line 70
  7. lemma OAI.ClusterDisplacement.Kernel.cutoff_apply line 77
  8. lemma OAI.ClusterDisplacement.Kernel.cutoff_firm line 80
  9. def OAI.ProjectionComparison.averagingKernel line 97
  10. lemma OAI.ProjectionComparison.averagingKernel_apply line 103
  11. lemma OAI.ProjectionComparison.averagingKernel_firm line 108
  12. theorem OAI.ProjectionComparison.projection_update_kernel line 115