Documentation

LeanPool.RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.SupportedH1

RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.SupportedH1 #

Supported Euclidean H¹ subspaces for a general measure.

This file defines the H¹ subspace of functions whose L² component is (a.e.) supported in a measurable set K, modeled as membership in the closed range of the extension-by-zero map Lp (μ.restrict K) →ₗᵢ Lp μ.

These definitions match the volume-specialized h1On construction used by RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Rellich, but are stated for an arbitrary measure μ. Compactness results are proven elsewhere.

Main definitions #

source
@[implicit_reducible]
def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableSpaceSupportedH1 {E : Type u_1} [NormedAddCommGroup E] :
MeasurableSpace E

Borel σ-algebra on the model space E.

Equations
Instances For
    source
    theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instBorelSpaceSupportedH1 {E : Type u_1} [NormedAddCommGroup E] :
    BorelSpace E
    source
    theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instOpensMeasurableSpaceSupportedH1 {E : Type u_1} [NormedAddCommGroup E] :
    OpensMeasurableSpace E
    source
    theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instFactOneLeTwoSobolevEuclideanSupportedH1 :
    Fact (1 ≤ 2)

    Range characterization for extension-by-zero #

    source
    theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.mem_range_extendByZeroₗᵢ_toLp_of_tsupport_subset {E : Type u_1} [NormedAddCommGroup E] (μ : MeasureTheory.Measure E) {K : Set E} (hKm : MeasurableSet K) {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (hf : MeasureTheory.MemLp f 2 μ) (hK : tsupport f ⊆ K) :
    MeasureTheory.MemLp.toLp f hf ∈ (MeasureTheory.Lp.extendByZeroₗᵢ hKm).range

    If a function is supported in K, then its Lp class belongs to the range of extendByZeroₗᵢ from the restricted measure μ.restrict K.

    source
    noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1OnMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] {K : Set E} (hKm : MeasurableSet K) :
    Submodule ℝ ↥(h1 μ)

    The subspace of H¹(μ) whose L² component is (a.e.) supported in K.

    We model “supported in K” as belonging to the closed range of the extension-by-zero map Lp(μ.restrict K) →ₗᵢ Lp(μ).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1OnToL2Measure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] {K : Set E} (hKm : MeasurableSet K) :
      ↥(h1OnMeasure μ hKm) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 μ)

      The inclusion h1OnMeasure μ K → L²(μ) as a continuous linear map.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For