Even reflection across a hyperplane preserves weak differentiability #

Let H = normalHalfSpace a = {x | a < x.fst} in the Euclidean product ℝ × E, and let ρ (t, y) = (2a - t, y) be the reflection in its boundary hyperplane {a} × E. If w is weakly differentiable on H with weak gradient G, and w and G are locally integrable up to the boundary (we extend them by zero off H), then the even reflection

x ↦ w x + w (ρ x)

is weakly differentiable on the whole space, with weak gradient x ↦ G x + R (G (ρ x)), where R (s, z) = (-s, z) is the linear part of ρ. No boundary condition on w is needed: the reflection is what makes the two one-sided traces match. This is the analytic content of the extension operator W^{1,p}(H) → W^{1,p}(ℝ × E) constructed in TauCeti.Analysis.Sobolev.Trace.Extension.

The proof follows H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Lemma 9.2. A test function φ on the whole space is tested against the even reflection; after the change of variables x ↦ ρ x this becomes the pairing of w on H with χ = φ ± φ ∘ ρ, where the sign is + for directions tangent to the boundary and - for the normal direction. Such a χ is not supported inside H, so it is multiplied by cutoffs η_n (x.fst) vanishing near the boundary. In tangential directions the cutoff commutes with differentiation. In the normal direction χ vanishes on the boundary, so |χ| ≤ M (x.fst - a) there, which exactly compensates the size O(n) of η_n' on its support of width O(1/n). Dominated convergence then passes to the limit.

Main declarations #

TauCeti.normalLinearReflection: the linear reflection (t, y) ↦ (-t, y), which is Mathlib's Submodule.reflection in the hyperplane {0} × E.
TauCeti.normalReflection: the affine reflection (t, y) ↦ (2a - t, y) in {a} × E, with its measure preservation and derivative.
TauCeti.gradient_normalReflection_of_forall_eq_neg: the gradient of a function odd under the normal reflection ρ satisfies ∇h (ρ x) = -R (∇h x), where R is the linear part of ρ.
TauCeti.integrableOn_of_integrableOn_inter_normalHalfSpace and TauCeti.setIntegral_eq_two_smul_setIntegral_inter_normalHalfSpace: a reflection-invariant function on a reflection-invariant set is integrable there as soon as it is integrable on the half in H, and its integral is twice the integral over that half.
TauCeti.normalCutoff: the smooth cutoff σ(c (x.fst - a) - 1) of the normal coordinate, supported a positive distance inside the half-space, with the common bound TauCeti.exists_normalCutoff_bound on it and its gradient.
TauCeti.tendsto_integral_normalCutoff_mul and TauCeti.tendsto_integral_mul_fderiv_normalCutoff_apply: the two limits behind integration by parts up to the boundary. Multiplying by the cutoffs does not change integrals over the half-space in the limit, and the error from differentiating them vanishes against a function that is zero on the boundary.
TauCeti.HasWeakFDerivOn.add_comp_normalReflection: the even reflection of a weakly differentiable function on the half-space is weakly differentiable on the whole space.
TauCeti.HasWeakLineDerivOn.top_of_normalHalfSpace: in a direction tangent to the boundary, the extension by zero of a weakly differentiable function on the half-space is weakly differentiable on the whole space.
TauCeti.HasWeakFDerivOn.hasWeakLineDerivOn_sub_comp_normalReflection: in a direction tangent to the boundary, the odd reflection is weakly differentiable on the whole space.
TauCeti.HasWeakFDerivOn.comp_normalReflection: precomposition with the reflection on the whole space.

References #

H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Lemma 9.2.

Even reflection across a hyperplane preserves weak differentiability #

Main declarations #

References #

The reflection in the boundary hyperplane #

Cutoffs vanishing near the boundary hyperplane #

Integration by parts up to the boundary #