Research proof index

Distributions on Space d.succ from distributions on Space d given a direction i. These distributions are constant on slices in the i direction.. -/ def constantSliceDist {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (i : Fin d.succ) : ((Space d) →d[ℝ] M) →ₗ[ℝ] (Space d.succ) →d[ℝ] M where toFun f := f ∘L sliceSchwartz i map_add' f g...

The distributional spatial derivative of the distribution associated to a differentiable function is the distribution associated to the corresponding pointwise spatial derivative.

The distributional divergence of the radial field x ↦ ‖x‖ ^ (-d) • x (i.e. x / ‖x‖ ^ d) equals d * volume (Metric.ball 0 1) , the surface area of the unit sphere S^{d-1} , times the Dirac delta at the origin. This is the Gauss-law identity underlying the fundamental solution of the Laplacian: away from 0 the field is divergence-free, and all of...

The divergence of a distribution from a bounded function.

The gradient of a distribution (Space d) →d[ℝ] ℝ as a distribution (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)). -/ noncomputable def distGrad {d} : ((Space d) →d[ℝ] ℝ) →ₗ[ℝ] (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)) where toFun f := basis.repr.toContinuousLinearMap ∘L ((InnerProductSpace.toDual ℝ (Space d)).symm.toContinuousLinearMap).comp (fderivD ℝ...

The gradient of a distribution (Space d) →d[ℝ] ℝ as a distribution (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)). -/ noncomputable def distGrad {d} : ((Space d) →d[ℝ] ℝ) →ₗ[ℝ] (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)) where toFun f := basis.repr.toContinuousLinearMap ∘L ((InnerProductSpace.toDual ℝ (Space d)).symm.toContinuousLinearMap).comp (fderivD ℝ...