MollifiedPrimitive #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: mollified fields carry smooth stationary primitives #
The cutoff core of part (i) of l.approximation.stationary.by.local
(Algsuperdiff/Section3/Provider/Corrector/PotentialApproximation.lean,
exists_isPotentialZeroTraceOn_limsup_le, ABK26) is stated on the class of
stationary fields possessing a stationary square-integrable primitive with
smooth spatial realizations:
∀ᵐ ω, ContDiff ℝ ⊤ (realize φ ω) ∧ ∀ x i, ∂ᵢ (realize φ ω) x = (realize p ω x)ᵢ.
This file shows that mollification produces members of that class outright.
For a smooth compactly supported kernel κ and any stationary φ ∈ L²(Ω),
mollify κ φis a stationaryL²field withC^∞realizations, and- its spatial gradient is again a stationary
L²field, namelymollifyGrad κ φ, whoseith component is the mollification ofφby theith partial derivative∂ᵢκof the kernel.
The gradient identity is the convolution derivative ∂ᵢ(κ ⋆ u) = (∂ᵢκ) ⋆ u,
which holds at every point, so no almost-everywhere upgrade in the space
variable is needed.
Partial derivatives of a smoothing kernel #
The ith partial derivative of a smoothing kernel.
Equations
Instances For
The directional derivative of a convolution falls on the kernel. This is
Mathlib's HasCompactSupport.hasFDerivAt_convolution_right transported through
convolution_flip and convolution_precompR_apply.
The mollified gradient #
The spatial gradient of a mollified scalar field, as a stationary field:
its ith component is the mollification of φ by ∂ᵢκ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The gradient identity for a mollified field. At every point of space,
the ith partial derivative of the realization of mollify κ φ is the
realization of the ith component of mollifyGrad κ φ.
The dense class: mollified fields satisfy the primitive hypothesis #
The mollified gradient is a measurable field.
The mollified gradient stays in the stationary L² layer.
The dense class of part (i). Every mollification of a stationary L²
scalar field is a stationary L² field whose realizations are smooth and whose
spatial gradient is the stationary L² field mollifyGrad κ φ. This is
exactly the hypothesis package hprim of
exists_isPotentialZeroTraceOn_limsup_le.