Extension by reflection from a half-space, and the half-space trace #
Every Sobolev function on the half-space H = normalHalfSpace a = {x | a < x.fst} of the
Euclidean product ℝ × E extends to a Sobolev function on the whole space: its even reflection
across the boundary hyperplane {a} × E. This file packages that extension as a bounded linear
operator
TauCeti.W1p.extendByReflectionL a : W^{1,p}(H) →L[ℝ] W^{1,p}(ℝ × E),
for every 1 ≤ p ≤ ∞, with norm at most 2, and a right inverse of restriction to H. Its value
is u on H and u ∘ ρ on the other side, where ρ (t, y) = (2a - t, y); its gradient is
∇u on H and the reflected gradient R (∇u ∘ ρ) on the other side, R (s, z) = (-s, z). The
analytic content, that this pair is a weak derivative across the hyperplane, is
TauCeti.HasWeakFDerivOn.add_comp_normalReflection.
Composing with the whole-space trace TauCeti.W1p.hyperplaneTrace gives the trace of an
arbitrary W^{1,p} function on the half-space, TauCeti.W1p.halfSpaceTrace, for 1 ≤ p < ∞.
By the one-sided trace estimate TauCeti.W1p.norm_hyperplaneTrace_rpow_le_restrictL it is
controlled by the Sobolev norm on the half-space alone (with norm at most one for p = 2), and
it agrees with the trace of every whole-space extension.
Unlike extension by zero (TauCeti.W1p0.extendByZeroL), which needs the zero boundary condition
of W^{1,p}_0, the reflection extends every Sobolev function on the half-space. The half-space
is the local model for extension and trace on domains with Lipschitz boundary.
Main declarations #
TauCeti.W1p.extendByReflectionL: the extension operator, withTauCeti.W1p.restrictL_extendByReflectionL,TauCeti.W1p.norm_extendByReflectionL_le,TauCeti.W1p.opNorm_extendByReflectionL_le, and its value and gradientTauCeti.W1p.value_extendByReflectionL_aeandTauCeti.W1p.gradient_extendByReflectionL_ae.TauCeti.W1p.halfSpaceTrace: theLᵖtrace on{a} × Eof aW^{1,p}function on the half-space, withTauCeti.W1p.norm_halfSpaceTrace_rpow_le, the boundsTauCeti.W1p.norm_halfSpaceTrace_leandTauCeti.W1p.opNorm_halfSpaceTrace_lewith constantp ^ (1 / p), the sharperH¹boundsTauCeti.W1p.norm_halfSpaceTrace_le_normandTauCeti.W1p.opNorm_halfSpaceTrace_le_one, andTauCeti.W1p.halfSpaceTrace_restrictL. OnW^{1,p}_0of the half-space it agrees with the zero-boundary trace (TauCeti.W1p.halfSpaceTrace_coe_w1p0) and so vanishes (TauCeti.W1p.halfSpaceTrace_eq_zero_of_w1p0).
References #
H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Lemma 9.2; L. C. Evans, Partial Differential Equations, Chapter 5, §5.4 and §5.5.
The extension operator #
Extension by reflection from the half-space {x | a < x.fst} to the whole space: a
Sobolev function u on the half-space is sent to its even reflection, equal to u on the
half-space and to u ∘ ρ on the other side, ρ being the reflection in {a} × E. It is a
right inverse of restriction (TauCeti.W1p.restrictL_extendByReflectionL) with norm at most 2
(TauCeti.W1p.norm_extendByReflectionL_le).
Instances For
The value of the reflection extension is u on the half-space and u ∘ ρ on the other side,
almost everywhere.
The weak gradient of the reflection extension is ∇u on the half-space and the reflected
gradient R (∇u ∘ ρ) on the other side, almost everywhere, where R negates the normal
component.
Restricting the reflection extension back to the half-space recovers the original function.
The reflection extension at most doubles the Sobolev norm.
The reflection extension has operator norm at most 2.
The trace of a half-space Sobolev function #
The Lᵖ trace on the boundary hyperplane {a} × E of a W^{1,p} function on the half-space
{x | a < x.fst}: the whole-space hyperplane trace of its reflection extension. By
TauCeti.W1p.halfSpaceTrace_restrictL it agrees with the trace of any whole-space extension.
Instances For
The half-space trace is the hyperplane trace of the reflection extension.
For 1 ≤ p < ∞, the p-th power of the Lᵖ norm of the half-space trace of u is at most
(p - 1) ‖u‖ᵖ + ‖∇u‖ᵖ, with both norms taken on the half-space.
For 1 ≤ p < ∞, the half-space trace has norm at most p ^ (1 / p) times the Sobolev norm on
the half-space. The constant is 1 at p = 1.
For 1 ≤ p < ∞, the half-space trace has operator norm at most p ^ (1 / p), which is 1
at p = 1.
The H¹ half-space trace has norm at most the Sobolev norm on the half-space.
The H¹ half-space trace has operator norm at most one.
The half-space trace of the restriction of a whole-space W^{1,p} function is its hyperplane
trace. With TauCeti.W1p.hyperplaneTrace_ofTestFunction_apply_ae, this identifies the trace of
the restriction of a test function with its classical boundary values.
On W^{1,p}_0 of the half-space, the half-space trace agrees with the zero-boundary trace
TauCeti.W1p0.hyperplaneTrace, defined through extension by zero.
Functions in W^{1,p}_0 of the half-space have zero half-space trace: the flat-model inclusion
W^{1,p}_0(H) ⊆ ker(halfSpaceTrace).