The `H¹` trace on a hyperplane #

Restriction to {a} × E extends uniquely to a bounded linear map from the weak Sobolev space H¹(ℝ × E) to L²(E). The ambient product has its Euclidean norm, represented by WithLp 2. The trace agrees with restriction on test functions, has operator norm at most one, and sends Sobolev convergence to convergence of boundary values. The construction uses the whole-space test-function density theorem and Mathlib's LinearMap.extendOfNorm.

This flat trace is the local model for boundary conditions on strips and on smooth domains. No pointwise representative of an arbitrary Sobolev function is evaluated: agreement with classical restriction is first proved on the dense space of test functions.

The proof follows L. C. Evans, Partial Differential Equations, Chapter 5, §5.5.

source

theorem TauCeti.integral_hyperplane_sq_le_integral_sq_add_norm_fderiv_sq {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {u : WithLp 2 (ℝ × E) → ℝ} (hu : ContDiff ℝ 1 u) (hsupp : HasCompactSupport u) (a : ℝ) :

∫ (y : E), u (WithLp.toLp 2 (a, y)) ^ 2 ≤ ∫ (x : WithLp 2 (ℝ × E)), u x ^ 2 + ‖fderiv ℝ u x‖ ^ 2

The squared L² norm on a hyperplane is bounded by the whole-space H¹ energy of a compactly supported C¹ function.

source

noncomputable def TauCeti.W1p.hyperplaneTrace {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] (a : ℝ) :

↥(W1p MeasureTheory.volume ⊤ 2) →L[ℝ ] ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The L² trace of a whole-space H¹ function on the hyperplane {a} × E, defined as the unique continuous extension of restriction of test functions.

Equations