OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/TorusHeatEvolutionSmooth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Smoothness of the prescribed heat convolution at every positive time. Compact parameter integration applies after using logarithmic time.

  1. abbrev OAI.ForcedComputation.VelocityDetector.HeatCell line 14
  2. instance OAI.ForcedComputation.VelocityDetector.(instance at line 15) line 15
  3. instance OAI.ForcedComputation.VelocityDetector.(instance at line 19) line 19
  4. theorem OAI.ForcedComputation.VelocityDetector.torusHeatEvolution_exp_smooth line 24
  5. theorem OAI.ForcedComputation.VelocityDetector.torusHeatEvolution_smooth_positive line 49