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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian heat equation transferred to bounded smooth initial data.

  1. def OAI.ForcedComputation.PlaneHeat.spatialPartial line 14
  2. theorem OAI.ForcedComputation.PlaneHeat.partial_smooth line 17
  3. theorem OAI.ForcedComputation.PlaneHeat.slice_one_hasDerivAt line 21
  4. theorem OAI.ForcedComputation.PlaneHeat.slice_zero_hasDerivAt line 33
  5. theorem OAI.ForcedComputation.PlaneHeat.kernelSecond_zero line 45
  6. theorem OAI.ForcedComputation.PlaneHeat.kernelSecond_one line 50
  7. theorem OAI.ForcedComputation.PlaneHeat.kernelSecond_transfer line 56

    Source documentation

    A Gaussian second derivative can be moved onto the bounded data.

    theorem kernelSecond_transfer {t : ℝ} (ht : 0 < t) {f : Plane → F}
    (hf : ContDiff ℝ ∞ f) (j : Fin 2) (C D E : ℝ)
    (hC : ∀ x, ‖f x‖ ≤ C) (hD : ∀ x, ‖spatialPartial F j f x‖ ≤ D)
    (hE : ∀ x, ‖spatialPartial F j (spatialPartial F j f) x‖ ≤ E) :
    (∫ x, kernelSecond t j x • f x) =
      ∫ x, kernel t x • spatialPartial F j (spatialPartial F j f) x := by
…

    Mentions: OAI.ForcedComputation.PlaneHeat.spatialPartial, OAI.ForcedComputation.PlaneHeat.kernelSecond, OAI.ForcedComputation.PlaneHeat.kernel

  8. theorem OAI.ForcedComputation.PlaneHeat.partial_reflection line 76
  9. theorem OAI.ForcedComputation.PlaneHeat.partial_reflection_twice line 87
  10. theorem OAI.ForcedComputation.PlaneHeat.kernelSecond_convolve line 100
  11. theorem OAI.ForcedComputation.PlaneHeat.hasDerivAt_heatConvolution_data line 116

    Source documentation

    The time derivative is the sum of heat evolutions of the actual second partials.

    theorem hasDerivAt_heatConvolution_data {t : ℝ} (ht : 0 < t) {f : Plane → F}
    (hf : ContDiff ℝ ∞ f) (C D E : ℝ)
    (hC : ∀ x, ‖f x‖ ≤ C) (hD : ∀ j x, ‖spatialPartial F j f x‖ ≤ D)
    (hE : ∀ j x, ‖spatialPartial F j (spatialPartial F j f) x‖ ≤ E) (x : Plane) :
    HasDerivAt (fun s => heatConvolution F s f x)
      (∑ j : Fin 2, heatConvolution F t (spatialPartial F j (spatialPartial F j f)) x) t := by
…

    Mentions: OAI.ForcedComputation.PlaneHeat.spatialPartial, OAI.ForcedComputation.PlaneHeat.heatConvolution

  12. theorem OAI.ForcedComputation.PlaneHeat.norm_partial_le line 135
  13. theorem OAI.ForcedComputation.PlaneHeat.partial_heatConvolution line 141
  14. theorem OAI.ForcedComputation.PlaneHeat.gradient_convolve_data line 155
  15. theorem OAI.ForcedComputation.PlaneHeat.hasDerivAt_heatConvolution_equation line 164

    Source documentation

    The actual heat convolution solves the heat equation, with no assumed PDE input.

    theorem hasDerivAt_heatConvolution_equation {t : ℝ} (ht : 0 < t) {f : Plane → F}
    (hf : ContDiff ℝ ∞ f) (C D E : ℝ)
    (hC : ∀ x, ‖f x‖ ≤ C) (hD : ∀ x, ‖fderiv ℝ f x‖ ≤ D)
    (hE : ∀ j x, ‖fderiv ℝ (spatialPartial F j f) x‖ ≤ E) (x : Plane) :
    HasDerivAt (fun s => heatConvolution F s f x)
      (∑ j : Fin 2, spatialPartial F j (spatialPartial F j (heatConvolution F t f)) x) t := by
…

    Mentions: OAI.ForcedComputation.PlaneHeat.spatialPartial, OAI.ForcedComputation.PlaneHeat.heatConvolution