OAI/Geometry/RCD/Heat/DiagonalConditionalKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A conditionally diagonal self-product is a measurable Dirac family

  1. theorem OAI.RegularPointCoordinates.probability_zeroOne_of_prod_diagonal line 15
  2. theorem OAI.RegularPointCoordinates.kernel_dirac_of_diagonal_self_product line 29