Documentation

TauCeti.Analysis.Sobolev.GraphStep.Density

Smooth compactly supported fields are dense in vector-valued W^{1,p}(ℝⁿ) #

For a finite-dimensional target F and 1 ≤ p < ∞, every element of the first-order weak-derivative graph over Lᵖ(ℝⁿ, F) is a limit of the graph elements of smooth compactly supported fields ℝⁿ → F. A priori estimates proved for smooth compactly supported fields therefore extend to the whole Sobolev space by continuity.

The proof is coordinatewise. A scalar Sobolev function u and a vector b : F give the field x ↦ u x • b (TauCeti.WeakDerivStep.smulRightW1pL), with weak derivative v ↦ ∂ᵥ u • b. Choosing a basis bᵢ of F with coordinate functionals ℓᵢ, a field u is the sum of the fields ℓᵢ ∘ u • bᵢ built from its scalar projections TauCeti.WeakDerivStep.toW1pL. Each scalar projection is a limit of test functions (TauCeti.W1p.denseRange_ofTestFunctionₗ_top), and a test function ψ gives the smooth compactly supported field x ↦ ψ x • bᵢ.

Main declarations #

References #

L. C. Evans, Partial Differential Equations, §5.3.1; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Theorem 9.2 (the scalar case, which is applied here coordinatewise).

source
noncomputable def TauCeti.WeakDerivStep.smulRightGradientL {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (b : F) :
E →L[ℝ] E →L[ℝ] F

The derivative v ↦ ⟪g, v⟫ • b of the field x ↦ u x • b at a point where the scalar function u has gradient g.

Instances For
    source
    @[simp]
    theorem TauCeti.WeakDerivStep.smulRightGradientL_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (b : F) (g v : E) :
    ((smulRightGradientL b) g) v = inner ℝ g v • b

    Evaluation formula for smulRightGradientL.

    source
    theorem TauCeti.WeakDerivStep.hasWeakFDerivOn_smulRight {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (b : F) (u : ↥(W1p mu Omega p)) :
    HasWeakFDerivOn mu Omega ↑↑((ContinuousLinearMap.compLpL p (mu.restrict ↑Omega) (ContinuousLinearMap.toSpanSingleton ℝ b)) (W1p.value u)) ↑↑((ContinuousLinearMap.compLpL p (mu.restrict ↑Omega) (smulRightGradientL b)) (W1p.gradient u))

    The field x ↦ u x • b of a scalar Sobolev function has weak derivative v ↦ ⟪∇u x, v⟫ • b.

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

    The bounded linear map sending a scalar Sobolev function u to the F-valued Sobolev field x ↦ u x • b.

    Instances For
      source
      @[simp]
      theorem TauCeti.WeakDerivStep.prev_smulRightW1pL {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (b : F) (u : ↥(W1p mu Omega p)) :
      prev (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) ((smulRightW1pL b) u) = (ContinuousLinearMap.compLpL p (mu.restrict ↑Omega) (ContinuousLinearMap.toSpanSingleton ℝ b)) (W1p.value u)

      The value of smulRightW1pL b u is the class of x ↦ u x • b.

      source
      @[simp]
      theorem TauCeti.WeakDerivStep.weakFDeriv_smulRightW1pL {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (b : F) (u : ↥(W1p mu Omega p)) :
      weakFDeriv (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) ((smulRightW1pL b) u) = (ContinuousLinearMap.compLpL p (mu.restrict ↑Omega) (smulRightGradientL b)) (W1p.gradient u)

      The weak derivative of smulRightW1pL b u is the class of x ↦ (v ↦ ⟪∇u x, v⟫ • b).

      source
      theorem TauCeti.WeakDerivStep.prev_smulRightW1pL_ofTestFunctionₗ_ae_eq {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [CompleteSpace F] (b : F) (φ : TestFunction Omega ℝ ⊤) :
      ↑↑(prev (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) ((smulRightW1pL b) ((W1p.ofTestFunctionₗ mu Omega p) φ))) =ᵐ[mu.restrict ↑Omega] fun (x : E) => φ x • b

      The field smulRightW1pL b φ of a test function φ is represented by x ↦ φ x • b.

      source
      theorem TauCeti.WeakDerivStep.sum_smulRightW1pL_toW1pL {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [FiniteDimensional ℝ F] {ι : Type u_3} [Fintype ι] (b : Module.Basis ι ℝ F) (u : ↥(WeakDerivStep mu Omega p (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))))) :
      ∑ i : ι, (smulRightW1pL (b i)) ((toW1pL (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (LinearMap.toContinuousLinearMap (b.coord i))) u) = u

      Coordinate reconstruction. For a basis b of F, an F-valued Sobolev field is the sum of the fields ℓᵢ ∘ u • bᵢ built from its scalar coordinate projections.

      source
      theorem TauCeti.WeakDerivStep.dense_setOf_exists_contDiff_hasCompactSupport {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] [FiniteDimensional ℝ F] (hp : p ≠ ⊤) :
      Dense {u : ↥(WeakDerivStep mu ⊤ p (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F p (mu.restrict ↑⊤)))) | ∃ (φ : E → F), ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ ↑↑(prev (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F p (mu.restrict ↑⊤))) u) =ᵐ[mu.restrict ↑⊤] φ}

      Density of smooth compactly supported fields. For a finite-dimensional target and 1 ≤ p < ∞, the elements of the weak-derivative graph over Lᵖ(ℝⁿ, F) represented by a smooth compactly supported field are dense.