OAI/Geometry/RCD/Heat/KernelHeatGeneratorDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Pointwise heat differentiation for arbitrary L2 initial data

  1. def OAI.RegularPointCoordinates.kernelHeatGeneratorSource line 15
  2. theorem OAI.RegularPointCoordinates.kernelHeat_generator_hasDerivAt line 18
  3. theorem OAI.RegularPointCoordinates.kernelHeatGeneratorSource_represents line 37
  4. theorem OAI.RegularPointCoordinates.continuous_kernelHeatGeneratorSource line 49