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

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomially weighted Fourier modes for the classical periodic heat solution. The positive-time Gaussian majorants are explicit.

  1. def OAI.ForcedComputation.VelocityDetector.heatModeLinear line 15
  2. def OAI.ForcedComputation.VelocityDetector.heatMode line 21
  3. def OAI.ForcedComputation.VelocityDetector.heatModeBound line 24
  4. theorem OAI.ForcedComputation.VelocityDetector.heatModeLinear_re line 27
  5. theorem OAI.ForcedComputation.VelocityDetector.heatMode_smooth line 31
  6. theorem OAI.ForcedComputation.VelocityDetector.heatMode_hasFDerivAt line 34
  7. theorem OAI.ForcedComputation.VelocityDetector.heatMode_norm line 40
  8. theorem OAI.ForcedComputation.VelocityDetector.heatModeBound_summable line 45
  9. theorem OAI.ForcedComputation.VelocityDetector.heatMode_norm_le line 55
  10. theorem OAI.ForcedComputation.VelocityDetector.heatModeLinear_norm_le line 65
  11. def OAI.ForcedComputation.VelocityDetector.heatModeDerivativeBound line 87
  12. theorem OAI.ForcedComputation.VelocityDetector.heatModeDerivativeBound_summable line 91
  13. theorem OAI.ForcedComputation.VelocityDetector.heatMode_derivative_norm_le line 96