Documentation

TauCeti.Analysis.Sobolev.Trace.Epigraph.Extension

Sobolev extension above a graph #

For a K-Lipschitz graph function φ, reflection in flattened coordinates gives a bounded extension from W^{1,p}(normalEpigraph φ) to the whole Euclidean product, for every 1 ≤ p ≤ ∞. The extension agrees with the original function above the graph and with its reflection (t, y) ↦ (2φ(y) - t, y) below it. Restriction back to the epigraph is a left inverse, and the extension has norm at most 2 * (1 + K)².

This is the graph-domain model used in constructing extension operators by boundary charts and partitions of unity. It uses the graph-flattening Sobolev equivalence and the half-space reflection extension already constructed in this library.

References #

L. C. Evans, Partial Differential Equations, 2nd ed., §5.4, Theorem 1 (extension by flattening and reflection).

Extension from the region above the graph of a K-Lipschitz function to the whole space: flatten the graph, extend by even reflection, and unflatten. It is a bounded right inverse of restriction, with norm at most 2 * (1 + K)².

Instances For
    theorem TauCeti.W1p.value_normalEpigraphExtensionL_ae {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : C(E, ℝ)} {K : NNReal} {p : ENNReal} [Fact (1 ≤ p)] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (hφ : LipschitzWith K ⇑φ) (u : ↥(W1p MeasureTheory.volume (normalEpigraph φ) p)) :
    ↑↑(value ((normalEpigraphExtensionL hφ) u)) =ᵐ[MeasureTheory.volume] fun (x : WithLp 2 (ℝ × E)) => if φ x.snd < x.fst then ↑↑(value u) x else if x.fst < φ x.snd then ↑↑(value u) (WithLp.toLp 2 (2 * φ x.snd - x.fst, x.snd)) else 0

    The extension is the original value above the graph, its even reflection below the graph, and zero on the graph, almost everywhere with respect to volume.

    @[simp]

    Restricting the graph-domain extension back to the region above the graph recovers the original Sobolev function.

    theorem TauCeti.W1p.gradient_normalEpigraphExtensionL_ae {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : C(E, ℝ)} {K : NNReal} {p : ENNReal} [Fact (1 ≤ p)] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (hφ : LipschitzWith K ⇑φ) (u : ↥(W1p MeasureTheory.volume (normalEpigraph φ) p)) :
    have Φ := graphFlattening ⇑φ ⋯; ↑↑(gradient ((normalEpigraphExtensionL hφ) u)) =ᵐ[MeasureTheory.volume] fun (x : WithLp 2 (ℝ × E)) => if φ x.snd < x.fst then ↑↑(gradient u) x else if x.fst < φ x.snd then (ContinuousLinearMap.adjoint (fderiv ℝ (⇑Φ) x)) ((normalLinearReflection E) ((ContinuousLinearMap.adjoint (fderiv ℝ (⇑Φ.symm) ((normalReflection E 0) (Φ x)))) (↑↑(gradient u) (WithLp.toLp 2 (2 * φ x.snd - x.fst, x.snd))))) else 0

    The extension has the original weak gradient above the graph. Below the graph, the gradient at the reflected point is transformed by the adjoint derivatives of unflattening and flattening, with normal reflection between them. On the graph the formula is zero, almost everywhere with respect to volume.

    The graph-domain extension multiplies the Sobolev norm by at most 2 * (1 + K)², uniformly in the exponent p.

    The graph-domain extension has operator norm at most 2 * (1 + K)².