The boundary trace of a bounded Lipschitz domain #
Let Ω ⊆ ℝ × E be a bounded Lipschitz domain and let σ be normalized dim E-dimensional
Euclidean Hausdorff measure restricted to frontier Ω. For 1 ≤ p < ∞, this file constructs
the trace operator
TauCeti.W1p.frontierTrace : W^{1,p}(Ω) →L[ℝ] Lᵖ(frontier Ω, σ),
the unique bounded linear operator that sends every u ∈ W^{1,p}(Ω) represented by a function f
continuous on closure Ω to the restriction of f to the frontier.
The construction glues the local chart traces. In one Lipschitz boundary chart, the local trace
is an Lᵖ function of the tangential parameter. Reading it at the tangential coordinate of each
boundary point transports it to Lᵖ of surface measure on the frontier patch; this is bounded
because surface measure pushes forward to at most (L + 1) ^ dim E times tangential Lebesgue
measure (Set.IsLipschitzChartWith.map_snd_euclideanHausdorffMeasure_frontier_inter_le).
Extension by zero gives TauCeti.W1p.lipschitzChartFrontierTrace. Summing over the charts of a
partition of unity, whose interior cutoff vanishes on the frontier, produces an operator with the
required boundary values. Uniqueness, and hence independence of all choices, follows because
restrictions of test functions are dense in W^{1,p}(Ω)
(TauCeti.W1p.denseRange_restrictL_ofTestFunctionₗ_top).
The same density argument shows that the trace commutes with multiplication by smooth bounded
functions, and that the frontier version of each local chart trace is the trace of the cutoff
product. Hence a function of zero trace has zero local trace in every chart, and the chart
characterization of W^{1,p}_0(Ω)
(TauCeti.W1p.mem_w1p0Submodule_iff_forall_lipschitzChartTrace_eq_zero) identifies the kernel
of the trace with W^{1,p}_0(Ω).
Main declarations #
TauCeti.W1p.lipschitzChartFrontierTrace: a local chart trace as anLᵖfunction on the frontier for surface measure.TauCeti.W1p.frontierTrace: the trace operator of a bounded Lipschitz domain.TauCeti.W1p.frontierTrace_ae_eq_of_continuousOn: the trace of a function continuous up to the boundary is its restriction to the frontier.TauCeti.W1p.eq_frontierTrace: any bounded operator with these boundary values is the trace.TauCeti.W1p.w1p0Submodule_le_ker_frontierTrace: functions inW^{1,p}_0(Ω)have zero trace.TauCeti.W1p.frontierTrace_contDiffSMul_ae: the trace ofψ uisψtimes the trace ofu.TauCeti.W1p.mem_w1p0Submodule_iff_frontierTrace_eq_zeroandTauCeti.W1p.ker_frontierTrace: the kernel of the trace isW^{1,p}_0(Ω).TauCeti.W1p.mem_w1p0Submodule_iff_frontierTrace_compAffineIsometryEquivL_eq_zeroandTauCeti.W1p.sub_mem_w1p0Submodule_iff_frontierTrace_compAffineIsometryEquivL_eq: the same for an open set of another inner product space that a rigid motion carries ontoΩ.
References #
- L. C. Evans, Partial Differential Equations, 2nd ed., §5.5, Theorems 1 and 2.
- J. Nečas, Direct Methods in the Theory of Elliptic Equations, Chapter 2, §4 (traces on Lipschitz domains by local flattening).
Local chart traces on the frontier #
A local chart trace on the frontier. The localized W^{1,p} trace through a Lipschitz
boundary chart, read at the tangential coordinate (e x).snd of each point x of the frontier
patch inside the chart cylinder, and extended by zero to the rest of the frontier. The result is
in Lᵖ for normalized Euclidean Hausdorff measure on frontier Ω.
Instances For
The frontier version of a local chart trace is the local trace evaluated at the tangential coordinate on the frontier patch of the chart, and zero elsewhere on the frontier.
A local chart trace on the frontier of a function continuous up to the boundary. If
u ∈ W^{1,p}(Ω) agrees almost everywhere with a function f continuous on closure Ω, then the
frontier version of its local chart trace is ψ f almost everywhere on the frontier.
Gluing local chart traces. If the cutoffs ψ i of finitely many Lipschitz boundary
charts sum to one on the frontier, then the sum of the frontier versions of the local traces
of a function continuous up to the boundary is its restriction to the frontier.
The trace operator #
Existence of the trace on a bounded Lipschitz domain. There is a bounded linear operator
W^{1,p}(Ω) → Lᵖ(frontier Ω), for p < ∞ and normalized Euclidean Hausdorff measure on the
frontier, sending every function continuous up to the boundary to its restriction to the
frontier.
The trace operator of a bounded Lipschitz domain, W^{1,p}(Ω) → Lᵖ(frontier Ω) for
p < ∞ and normalized dim E-dimensional Euclidean Hausdorff measure on the frontier. It is
characterized by TauCeti.W1p.frontierTrace_ae_eq_of_continuousOn and
TauCeti.W1p.eq_frontierTrace: it is the unique bounded linear operator sending every function
continuous up to the boundary to its restriction to the frontier.
Instances For
The trace of a function continuous up to the boundary is its boundary restriction. If
u ∈ W^{1,p}(Ω) agrees almost everywhere on Ω with a function f continuous on closure Ω, then
the trace of u is f almost everywhere on the frontier for surface measure.
Uniqueness of the trace. A bounded linear operator W^{1,p}(Ω) → Lᵖ(frontier Ω) that sends
the restriction to Ω of every test function on the whole space to its restriction to the
frontier is the trace operator.
Functions in W^{1,p}_0(Ω) have zero trace.
Localization and the kernel of the trace #
The trace commutes with smooth bounded multiplication. On a bounded Lipschitz domain, for
1 ≤ p < ∞, the trace of ψ u is ψ times the trace of u, for every smooth ψ bounded
together with its gradient on Ω. The density argument is adapted from the flat version
TauCeti.W1p.hyperplaneTrace_contDiffSMul_ae in TauCeti.Analysis.Sobolev.Trace.Multiplication.
A local chart trace on the frontier is the trace of the cutoff product. On a bounded
Lipschitz domain, for 1 ≤ p < ∞, the frontier version of the local trace through a Lipschitz
boundary chart with cutoff ψ is the trace of ψ u.
A local chart trace vanishes off the chart. On a bounded Lipschitz domain, for
1 ≤ p < ∞, the local trace through a Lipschitz boundary chart vanishes almost everywhere at
the tangential parameters whose graph point lies outside the chart cylinder.
Zero trace gives zero local chart traces. On a bounded Lipschitz domain, for
1 ≤ p < ∞, if the trace of u ∈ W^{1,p}(Ω) vanishes, then so does its local trace through
every Lipschitz boundary chart.
The functions of zero trace on a bounded Lipschitz domain are those of W^{1,p}_0. For
1 ≤ p < ∞, u ∈ W^{1,p}(Ω) lies in W^{1,p}_0(Ω) exactly when its trace on the frontier
vanishes.
The kernel of the trace on a bounded Lipschitz domain is W^{1,p}_0. For 1 ≤ p < ∞,
the trace W^{1,p}(Ω) → Lᵖ(frontier Ω) vanishes exactly on the closure of the test functions
supported in Ω.
Domains carried onto a Lipschitz domain by a rigid motion #
Zero trace in rigid coordinates. Let an affine isometry g carry the open set U ⊆ F
onto a bounded Lipschitz domain Ω, so that Ω = g.symm⁻¹(U). For 1 ≤ p < ∞, a function
u ∈ W^{1,p}(U) lies in W^{1,p}_0(U) exactly when the trace of u ∘ g⁻¹ on frontier Ω
vanishes.
Equal boundary values in rigid coordinates. Let an affine isometry g carry the open set
U ⊆ F onto a bounded Lipschitz domain Ω. For 1 ≤ p < ∞ and u, v ∈ W^{1,p}(U), the
difference u - v lies in W^{1,p}_0(U) exactly when u ∘ g⁻¹ and v ∘ g⁻¹ have the same
trace on frontier Ω.