Test functions as elements of Lp #
This file provides the generic bridge from compactly supported test functions on an open set to
Lp classes. A test function belongs to every Lᵖ space for any measure finite on compact sets.
The construction is used by the closed-graph presentations of weak Sobolev spaces.
The bridge is linear: TauCeti.testFunctionLp_add and TauCeti.testFunctionLp_smul record that
passing to the Lᵖ class commutes with the vector space structure of the test functions. For an
inner product space, TauCeti.gradientTestFunctionLp provides the parallel construction for the
gradient. These facts make the image of C_c^∞(Ω) in an Lᵖ-based function space a subspace.
On that subspace of L²(Ω), a distributional derivative bounded by the L² norm of test functions
extends by Hahn–Banach to a bounded functional on L²(Ω), and the negative of its Riesz
representative is a weak derivative:
TauCeti.exists_norm_le_hasWeakLineDerivOn_of_abs_integral_lineDeriv_mul_le.
A test function on Omega lies in every Lᵠ(Omega): it is continuous with compact support.
A test function on Omega as an element of Lᵠ(Omega).
Equations
- TauCeti.testFunctionLp q phi = MeasureTheory.MemLp.toLp ⇑phi ⋯
Instances For
The norm of a test function's Lᵖ class is its eLpNorm, converted to ℝ.
The extended norm of a test function's Lᵖ class is its eLpNorm for the ambient measure:
the function vanishes outside Omega, so the restriction may be dropped.
Passing from a test function to its Lᵠ class is injective for a measure that is positive on
nonempty open sets, such as an additive Haar measure.
An L²-bounded distributional derivative is an L² weak derivative. Let u be locally
integrable on Omega. If for some C ≥ 0 every test function phi on Omega satisfies
|∫ ∂_v phi * u| ≤ C ‖phi‖₂,
then u has a weak derivative in the direction v on Omega that lies in L²(Omega) and has
norm at most C.
The gradient of a test function #
The gradient of a test function is smooth.
The gradient of a test function is continuous.
The gradient of a test function has compact support.
The gradient of a test function on Ω vanishes outside Ω.
The gradient of a test function on Ω is continuous with compact support, so it lies in every
Lᵠ(Ω).
The gradient of a test function on Ω, as an element of Lᵠ(Ω, E).
Equations
- TauCeti.gradientTestFunctionLp q phi = MeasureTheory.MemLp.toLp (fun (x : E) => gradient (⇑phi) x) ⋯
Instances For
The norm of a test function gradient's Lᵖ class is its eLpNorm, converted to ℝ.
The extended norm of a test function gradient's Lᵖ class is the eLpNorm of its Fréchet
derivative for the ambient measure: the gradient vanishes outside Omega, so the restriction
may be dropped, and ‖∇ phi x‖ = ‖fderiv ℝ phi x‖.