Scalar projections of weak-derivative graph spaces

Applying a continuous linear functional to an F-valued Sobolev field gives a scalar Sobolev function. TauCeti.WeakDerivStep.toW1pL bundles this operation as a bounded linear map into W1p, using the Riesz correspondence to turn the projected derivative into a gradient. Its value is the projected field, and its gradient pairs with a direction as the functional applied to the original weak derivative.

For finite-dimensional F, applying a scalar embedding W^{1,p}(Ω) → L^{p⋆}(Ω) to every coordinate in a basis embeds the selected field into L^{p⋆}(Ω; F) (TauCeti.WeakDerivStep.exists_lpEmbeddingL_of_ae_eq).

The preceding space and its field-selection map remain arbitrary. This permits coordinatewise use of scalar Sobolev estimates without introducing a separate vector-valued Sobolev carrier. The construction uses WeakDerivStep and W1p.mk, whose weak derivatives are distributional.

Reference

L. C. Evans, Partial Differential Equations, second edition, Chapter 5, §5.2.

noncomputable def TauCeti.scalarGradientL {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ℓ : F →L[ℝ] ℝ) : (E →L[ℝ] F) →L[ℝ] E

Turn an F-valued derivative into the gradient of its scalar projection by ℓ, using the Riesz correspondence.

@[simp]

theorem TauCeti.inner_scalarGradientL_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ℓ : F →L[ℝ] ℝ) (D : E →L[ℝ] F) (h : E) : inner ℝ ((scalarGradientL ℓ) D) h = ℓ (D h)

Pairing a scalar-projected gradient with a direction evaluates the projected derivative.

theorem TauCeti.norm_scalarGradientL_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ℓ : F →L[ℝ] ℝ) : ‖scalarGradientL ℓ‖ ≤ ‖ℓ‖

Scalar projection of a derivative has operator norm at most the norm of the functional.

theorem TauCeti.WeakDerivStep.hasWeakFDerivOn_compLpL_base_prev {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (ℓ : F →L[ℝ] ℝ) (u : ↥(WeakDerivStep mu Omega p base)) : HasWeakFDerivOn mu Omega ↑↑((ContinuousLinearMap.compLpL p (mu.restrict ↑Omega) ℓ) (base (prev base u))) fun (x : E) => (innerSL ℝ) (↑↑((ContinuousLinearMap.compLpL p (mu.restrict ↑Omega) (scalarGradientL ℓ)) (weakFDeriv base u)) x)

The scalar-projected field has the Riesz representative of its projected weak derivative as weak gradient.

noncomputable def TauCeti.WeakDerivStep.toW1pL {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (ℓ : F →L[ℝ] ℝ) : ↥(WeakDerivStep mu Omega p base) →L[ℝ] ↥(W1p mu Omega p)

Apply a continuous linear functional to the field selected by base, obtaining a scalar Sobolev function. Its operator norm is at most ‖ℓ‖ * (‖base‖ + 1).

@[simp]

theorem TauCeti.WeakDerivStep.value_toW1pL {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (ℓ : F →L[ℝ] ℝ) (u : ↥(WeakDerivStep mu Omega p base)) : W1p.value ((toW1pL base ℓ) u) = (ContinuousLinearMap.compLpL p (mu.restrict ↑Omega) ℓ) (base (prev base u))

Scalar projection commutes with the value map: its Lᵖ class is obtained by applying ℓ to the field selected by base.

@[simp]

theorem TauCeti.WeakDerivStep.gradient_toW1pL {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (ℓ : F →L[ℝ] ℝ) (u : ↥(WeakDerivStep mu Omega p base)) : W1p.gradient ((toW1pL base ℓ) u) = (ContinuousLinearMap.compLpL p (mu.restrict ↑Omega) (scalarGradientL ℓ)) (weakFDeriv base u)

The gradient of a scalar projection is the Riesz representative of ℓ ∘ Du.

theorem TauCeti.WeakDerivStep.inner_gradient_toW1pL_ae {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (ℓ : F →L[ℝ] ℝ) (u : ↥(WeakDerivStep mu Omega p base)) : ∀ᵐ (x : E) ∂mu.restrict ↑Omega, ∀ (h : E), inner ℝ (↑↑(W1p.gradient ((toW1pL base ℓ) u)) x) h = ℓ ((↑↑(weakFDeriv base u) x) h)

Pairing the projected gradient with a direction applies ℓ to the original weak derivative in that direction, almost everywhere.

theorem TauCeti.WeakDerivStep.norm_toW1pL_le {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (ℓ : F →L[ℝ] ℝ) : ‖toW1pL base ℓ‖ ≤ ‖ℓ‖ * (‖base‖ + 1)

The scalar projection has an explicit operator-norm bound.

theorem TauCeti.WeakDerivStep.exists_lpEmbeddingL_of_ae_eq {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [FiniteDimensional ℝ F] {pstar : ENNReal} [Fact (1 ≤ pstar)] (S : ↥(W1p mu Omega p) →L[ℝ] ↥(MeasureTheory.Lp ℝ pstar (mu.restrict ↑Omega))) (hS : ∀ (u : ↥(W1p mu Omega p)), ↑↑(S u) =ᵐ[mu.restrict ↑Omega] ↑↑(W1p.value u)) (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) : ∃ (V : ↥(WeakDerivStep mu Omega p base) →L[ℝ] ↥(MeasureTheory.Lp F pstar (mu.restrict ↑Omega))), ∀ (u : ↥(WeakDerivStep mu Omega p base)), ↑↑(V u) =ᵐ[mu.restrict ↑Omega] ↑↑(base (prev base u))

Coordinatewise lifting of a scalar embedding. If a bounded linear map S : W^{1,p}(Ω) → L^{p⋆}(Ω) represents the values and F is finite-dimensional, then the field selected by base lies in L^{p⋆}(Ω; F), continuously in the graph norm. In a basis of F, each coordinate of the field is a scalar Sobolev function (TauCeti.WeakDerivStep.toW1pL), to which S applies.