Difference quotients of W^{1,p}(Ω) functions #
For u ∈ W^{1,p}(Ω), 1 ≤ p < ∞, a direction v and a compact K ⊆ Ω, the difference
quotients of u are bounded on K by the directional derivative of u:
‖t⁻¹ (u(· + t v) - u)‖_{Lᵖ(K)} ≤ ‖⟪v, ∇u⟫‖_{Lᵖ(Ω)}
as soon as the segments [x, x + t v], x ∈ K, stay inside Ω, and in particular for all
sufficiently small t. No boundary regularity of Ω is needed. This is the half of the
difference-quotient characterisation of Sobolev functions that is used, in the difference-quotient
method, to bound the difference quotients of a weak solution in the energy estimate; the converse
half is TauCeti.exists_norm_le_hasWeakLineDerivOn_of_frequently_eLpNorm_inv_mul_sub_le.
The bound comes from a local translation estimate,
‖u(· + h) - u‖_{Lᵖ(K)} ≤ ‖⟪h, ∇u⟫‖_{Lᵖ(T)}
whenever the segments [x, x + h], x ∈ K, lie in T ⊆ Ω. For smooth functions this is
ContDiff.eLpNorm_comp_add_sub_le_eLpNorm_fderiv_apply; it passes to W^{1,p}(ℝⁿ) by density of
the test functions. A general u ∈ W^{1,p}(Ω) is first multiplied by a smooth cutoff equal to
one near the segments and compactly supported in Ω, and then extended by zero to the whole
space; neither operation changes u or its gradient near the segments.
Main declarations #
TauCeti.W1p.differenceQuotient: the local Sobolev difference quotient, whose value and weak gradient are characterized by_aelemmas and whose defining formula isTauCeti.W1p.differenceQuotient_def.TauCeti.W1p.eLpNorm_value_comp_add_sub_le: the local translation estimate onW^{1,p}(Ω).TauCeti.W1p.eLpNorm_inv_mul_value_comp_add_smul_sub_le: the difference-quotient bound.TauCeti.W1p.eventually_eLpNorm_inv_mul_value_comp_add_smul_sub_le: the difference-quotient bound for all sufficiently smallt.TauCeti.W1p.norm_value_differenceQuotient_le: on the whole space the bound holds for every stept, with no compactness, in the form‖D^t_v u‖_p ≤ ‖v‖ ‖∇u‖_p.
References #
- L. C. Evans, Partial Differential Equations, §5.8.2, Theorem 3 (i).
- D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Lemma 7.23.
Local difference quotients #
The local Sobolev difference quotient. For V ⊆ Ω and V + t • w ⊆ Ω, this is the
element of W^{1,p}(V) represented by x ↦ t⁻¹ (u (x + t • w) - u x).
No assumption t ≠ 0 is needed for the definition: at t = 0 both the value and gradient are
zero. Applications approximating a derivative impose t ≠ 0 through their estimates.
Equations
- TauCeti.W1p.differenceQuotient hV w t hVO u = t⁻¹ • (TauCeti.W1p.translate hVO u - (TauCeti.W1p.restrictL hV) u)
Instances For
The local Sobolev difference quotient as a scaled difference of a translate and a
restriction. The body of TauCeti.W1p.differenceQuotient is not exposed to importing modules,
so this is how downstream files unfold it.
The value of the local Sobolev difference quotient has the expected representative.
The weak gradient of the local Sobolev difference quotient is the corresponding difference quotient of the weak gradient.
Difference-quotient estimates #
The local translation estimate on W^{1,p}(ℝⁿ). If T is measurable and every segment
[x, x + h] with x ∈ K lies in T, then
‖w(· + h) - w‖_{Lᵖ(K)} ≤ ‖⟪h, ∇w⟫‖_{Lᵖ(T)}.
This holds for 1 ≤ p < ∞; neither K nor T needs to be compact.
The local translation estimate on W^{1,p}(Ω). Let u ∈ W^{1,p}(Ω), 1 ≤ p < ∞, and
let K be compact. If every segment [x, x + h] with x ∈ K lies in a set T ⊆ Ω, then
‖u(· + h) - u‖_{Lᵖ(K)} ≤ ‖⟪h, ∇u⟫‖_{Lᵖ(T)}.
No boundary regularity of Ω is needed: the estimate only sees u near the segments.
Difference quotients of a W^{1,p}(Ω) function are bounded by its directional
derivative. Let u ∈ W^{1,p}(Ω), 1 ≤ p < ∞, and let K be compact. If every segment
[x, x + t v] with x ∈ K lies in a set T ⊆ Ω, then
‖t⁻¹ (u(· + t v) - u)‖_{Lᵖ(K)} ≤ ‖⟪v, ∇u⟫‖_{Lᵖ(T)}.
For t = 0 the left-hand side is zero.
Uniform bound on difference quotients near a compact set. Let u ∈ W^{1,p}(Ω),
1 ≤ p < ∞, and let K ⊆ Ω be compact. Then for all sufficiently small t,
‖t⁻¹ (u(· + t v) - u)‖_{Lᵖ(K)} ≤ ‖⟪v, ∇u⟫‖_{Lᵖ(Ω)}.
The whole-space difference-quotient bound. On Ω = ⊤ no compactness is needed: the
Lᵖ norm of the difference quotient of u ∈ W^{1,p}(ℝⁿ) in the direction v is at most
‖v‖ ‖∇u‖_p, uniformly in the step t. This is the form of
TauCeti.W1p.eLpNorm_inv_mul_value_comp_add_smul_sub_le that a difference-quotient argument on
the whole space consumes, stated for the bundled quotient
TauCeti.W1p.differenceQuotient.