Membership of a cut-off directional derivative in H₀¹(Ω) #
Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2 bootstraps interior
regularity by running the interior H² estimate on a derivative ∂_ℓ u of the weak solution.
EllipticPdes.Regularity.interior_H2_estimate quantifies its solution over H₀¹(Ω), and ∂_ℓ u has no boundary condition, so the derivative has to be cut off before it can be fed back in.
This file supplies the resulting admissibility statement: for the middle cutoff ξ of a cutoff
tower, the product ξ · ∂_ℓ u is again an element of H₀¹(Ω).
The route is a weak limit of the discrete family cutoffMul ξ (diffQuotG ℓ h u), every member
of which lies in H₀¹(Ω) by cutoffMul_diffQuotG_mem_H01. The family is bounded in the graph
norm uniformly in the step: the function coordinate and the second Leibniz summand of each
gradient coordinate are controlled by the first-order bound ‖Dₖ^h u‖ ≤ ‖∂ₖu‖, and the first
Leibniz summand ξ · Dₖ^h ∂ᵢu is exactly what the master energy estimate
interior_diffQuot_energy_bound controls. Weak sequential compactness then produces a limit,
which stays in H₀¹(Ω) because a closed subspace equals its double orthogonal complement, and
the function coordinate of the limit is pinned by the weak L² convergence of the difference
quotients.
Main declarations #
restrictL2_diffQuot_extendL2: the interior difference quotient as the restriction of the whole-space one.inner_mulTest_comm: multiplication by a cutoff is self-adjoint onL²(Ω).exists_mem_H01_mulTest_gradient: the cutoff of a directional derivative lies inH₀¹(Ω).interior_cutoffGrad_mem_H01: the same, together with the weak gradient it has.
Restricted and whole-space difference quotients #
Interior difference quotient as a restriction of the whole-space one. Both sides
evaluate to ((extendL2 g)(x + h eₖ) - g x) / h almost everywhere on Ω, because extension by
zero agrees with the class there. No support hypothesis is needed: the identity is read on Ω
only (Evans, Partial Differential Equations (2nd ed.), §6.3.1).
Extension by zero is a left inverse of restriction on Ω. Restricting the whole-space
extension of a class recovers the class.
First-order bound for the interior difference quotient. For u ∈ H₀¹(Ω) the interior
difference quotient of the function coordinate is bounded by the corresponding gradient
coordinate, uniformly in the step: extension by zero preserves the weak derivative
(hasWeakDeriv_extendL2_of_mem_H01), the whole-space bound ‖Dₖ^h g‖ ≤ ‖g'‖ applies, and
restriction is non-expansive (Evans, Partial Differential Equations (2nd ed.), §5.8.2).
Self-adjointness of the cutoff multipliers #
Self-adjointness of the cutoff multiplier on L²(Ω). Both pairings are the integral of the
triple product ∫_Ω η · g · w.
One-neighbourhood shift margin #
One-neighbourhood shift margin. If the cutoff η is ≡ 1 on a neighbourhood of a
compact set K, then there is a positive margin δ such that η is locally constant ≡ 1
near every point within δ of K. This restates, for use outside
EllipticPdes.Regularity.Interior.NormBound, the localisation fact that shifting a support
point of one tower cutoff by less than the margin lands where the next cutoff is identically
1 (Evans, Partial Differential Equations (2nd ed.), §6.3.1).
Uniform graph-norm bound on the discrete family #
Membership of a cut-off directional derivative in H₀¹(Ω) #
Cutoff of a directional derivative is admissible (Evans, Partial Differential
Equations (2nd ed.), §6.3.1, Theorem 2, step 3). For a weak solution u ∈ H₀¹(Ω) of
L u = f with W^{1,∞} principal coefficients and a cutoff tower T for V ⋐ Ω, the product
ξ · ∂_ℓ u of the middle tower cutoff with a directional derivative of u is again an element
of H₀¹(Ω): there is W ∈ H₀¹(Ω) whose function coordinate is ξ · ∂_ℓ u. Since H₀¹(Ω)
sits inside the weak-gradient graph space, the gradient coordinates of W are then the weak
derivatives of ξ · ∂_ℓ u, which hasWeakDeriv_extendL2_of_mem_H01 reads off.
This is the admissibility step the H^k bootstrap needs and that Evans does not: his interior
H² theorem asks only u ∈ H¹(U), so he differentiates the equation without cutting off,
whereas EllipticPdes.Regularity.interior_H2_estimate quantifies its solution over H₀¹(Ω) and
∂_ℓ u has no boundary condition.
The proof takes a weak limit of the admissible discrete family ξ · Dₗ^h u, whose members lie
in H₀¹(Ω) by cutoffMul_diffQuotG_mem_H01 and which is bounded in the graph norm by
exists_cutoffMul_diffQuotG_norm_bound. The limit stays in H₀¹(Ω) because a closed subspace
of a Hilbert space equals its double orthogonal complement, and its function coordinate is
pinned by the weak L² convergence Dₗ^h u ⇀ ∂_ℓ u.
Cutoff derivative is an H₀¹ function with its weak gradient (Evans, Partial
Differential Equations (2nd ed.), §6.3.1, Theorem 2, step 3). For a weak solution
u ∈ H₀¹(Ω) of L u = f with W^{1,∞} principal coefficients and a cutoff tower T for
V ⋐ Ω, the product ξ · ∂_ℓ u of the middle tower cutoff with a directional derivative of
u is an element W of H₀¹(Ω), and each gradient coordinate W_{k+1} of that element is
the weak k-derivative of ξ · ∂_ℓ u on the whole space.
This is the admissibility step that lets EllipticPdes.Regularity.interior_H2_estimate, whose
solution is quantified over H₀¹(Ω), be applied to a derivative of u, which has no boundary
condition of its own. Because ξ ≡ 1 on tsupport ζ, and ζ ≡ 1 on V, the function
coordinate agrees with ∂_ℓ u on a neighbourhood of V, so nothing is lost on the region of
interest.
Triviality of the cutoff on the base set #
Middle tower cutoff as 1 on the base set. ζ ≡ 1 on V, so V sits
inside tsupport ζ, where ξ ≡ 1.
Invisibility of the cutoff on the base set. Because ξ ≡ 1 on V, the V-restriction of
the whole-space extension of ξ · g agrees with that of g. Applied to the function coordinate
of interior_cutoffGrad_mem_H01, this says that the admissible element has ∂_ℓ u itself on
V, so nothing is lost on the region of interest.
Kept as the statement that reads interior_cutoffGrad_mem_H01, which is pinned in AxiomAudit.
Nothing else consumes it.