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

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

The normalized Euclidean heat kernel, with its integrable first derivatives.

  1. def OAI.ForcedComputation.PlaneHeat.oneDim line 17
  2. def OAI.ForcedComputation.PlaneHeat.oneDimDerivative line 20
  3. theorem OAI.ForcedComputation.PlaneHeat.oneDim_nonneg line 22
  4. theorem OAI.ForcedComputation.PlaneHeat.oneDim_integrable line 26
  5. theorem OAI.ForcedComputation.PlaneHeat.oneDim_integral line 29
  6. theorem OAI.ForcedComputation.PlaneHeat.oneDim_hasDerivAt line 36
  7. theorem OAI.ForcedComputation.PlaneHeat.oneDim_smooth line 45
  8. theorem OAI.ForcedComputation.PlaneHeat.firstMoment_Ioi line 50
  9. theorem OAI.ForcedComputation.PlaneHeat.absoluteFirstMoment line 67
  10. theorem OAI.ForcedComputation.PlaneHeat.oneDimDerivative_integrable line 76
  11. theorem OAI.ForcedComputation.PlaneHeat.oneDimDerivative_abs_integral line 86
  12. theorem OAI.ForcedComputation.PlaneHeat.oneDimDerivative_abs_integral_le line 101
  13. def OAI.ForcedComputation.PlaneHeat.kernel line 109
  14. def OAI.ForcedComputation.PlaneHeat.kernelDerivative line 111
  15. theorem OAI.ForcedComputation.PlaneHeat.kernel_smooth line 114
  16. theorem OAI.ForcedComputation.PlaneHeat.kernel_fderiv_basis line 119

    Source documentation

    The explicit first derivative in each Cartesian direction.

    theorem kernel_fderiv_basis {t : ℝ} (ht : 0 < t) (x : Plane) (j : Fin 2) :
    fderiv ℝ (kernel t) x (Pi.single j 1) = kernelDerivative t j x := by
…

    Mentions: OAI.ForcedComputation.PlaneHeat.kernel, OAI.ForcedComputation.PlaneHeat.kernelDerivative

  17. theorem OAI.ForcedComputation.PlaneHeat.integrable_coordinate_product line 132
  18. theorem OAI.ForcedComputation.PlaneHeat.integral_coordinate_product line 137
  19. theorem OAI.ForcedComputation.PlaneHeat.kernel_nonneg line 144
  20. theorem OAI.ForcedComputation.PlaneHeat.kernel_integrable line 147
  21. theorem OAI.ForcedComputation.PlaneHeat.kernel_integral line 150
  22. theorem OAI.ForcedComputation.PlaneHeat.kernelDerivative_zero line 154
  23. theorem OAI.ForcedComputation.PlaneHeat.kernelDerivative_one line 159
  24. theorem OAI.ForcedComputation.PlaneHeat.kernelDerivative_integrable line 164
  25. theorem OAI.ForcedComputation.PlaneHeat.kernelDerivative_abs_integral line 178
  26. theorem OAI.ForcedComputation.PlaneHeat.kernelDerivative_abs_integral_le line 197

    Source documentation

    The integrable gradient bound used in the short-time Volterra contraction.

    theorem kernelDerivative_abs_integral_le {t : ℝ} (ht : 0 < t) (j : Fin 2) :
    (∫ x : Plane, |kernelDerivative t j x|) ≤ 2 / Real.sqrt t := by
…

    Mentions: OAI.ForcedComputation.PlaneHeat.kernelDerivative