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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Pointwise convolution and differentiation for integrable kernels and bounded spatial jets.

  1. def OAI.ForcedComputation.BoundedKernel.convolve line 18
  2. theorem OAI.ForcedComputation.BoundedKernel.integrand_integrable line 22
  3. theorem OAI.ForcedComputation.BoundedKernel.norm_convolve_le line 33
  4. theorem OAI.ForcedComputation.BoundedKernel.hasFDerivAt_convolve line 52

    Source documentation

    Dominated differentiation transfers a spatial derivative to the bounded input function.

    theorem hasFDerivAt_convolve (μ : Measure E) (w : E → ℝ) (f : E → F)
    (hw : Integrable w μ) (hf : ContDiff ℝ 1 f)
    (C D : ℝ) (hC : ∀ x, ‖f x‖ ≤ C) (hD : ∀ x, ‖fderiv ℝ f x‖ ≤ D)
    (x : E) :
    HasFDerivAt (convolve E F μ w f)
      (∫ y, w y • fderiv ℝ f (x - y) ∂μ) x := by
…

    Mentions: OAI.ForcedComputation.BoundedKernel.convolve

  5. theorem OAI.ForcedComputation.BoundedKernel.fderiv_convolve line 77