RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.H1

An upstream-friendly definition of a Euclidean H¹-type energy space built from L².

At the current Mathlib pin, we do not have a ready-made Sobolev-space development for domains or manifolds. For the Laplace–Beltrami compact-resolvent discharge, we mainly need:

1. a Hilbert space H¹ equipped with a continuous embedding into L²;
2. a continuous “gradient” map H¹ → L²(E); and later
3. a compactness theorem for the inclusion on bounded domains / compact manifolds (Rellich).

This file defines H¹ as the closed submodule of L² × L²(E) generated by C¹-functions with compact support and their gradients (expressed using the Riesz representation toDual).

Main definitions

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.C1c: the ℝ-submodule of C¹ compactly supported functions E → ℝ.
• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1: the (closed) H¹ submodule of L²(E) × L²(E,E).
• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1ToL2: the continuous embedding H¹ → L².
• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1ToL2Grad: the continuous gradient map H¹ → L²(E).

No analytic “Sobolev theorems” are proved here; those are tracked separately (Rellich / elliptic regularity beads).

@[instance_reducible]

def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableSpaceH1 {E : Type u_1} [NormedAddCommGroup E] : MeasurableSpace E

Borel σ-algebra on the model space E.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableSpaceH1 = borel E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instBorelSpaceH1 {E : Type u_1} [NormedAddCommGroup E] : BorelSpace E

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instOpensMeasurableSpaceH1 {E : Type u_1} [NormedAddCommGroup E] : OpensMeasurableSpace E

@[reducible, inline]

abbrev RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2ℝ {E : Type u_1} [NormedAddCommGroup E] (μ : MeasureTheory.Measure E) : Type u_1

The space of square-integrable real-valued functions.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2ℝ μ = ↥(MeasureTheory.Lp ℝ 2 μ)

@[reducible, inline]

abbrev RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2E {E : Type u_1} [NormedAddCommGroup E] (μ : MeasureTheory.Measure E) : Type u_1

The space of square-integrable vector-valued functions.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2E μ = ↥(MeasureTheory.Lp E 2 μ)

@[reducible, inline]

abbrev RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.H1Target {E : Type u_1} [NormedAddCommGroup E] (μ : MeasureTheory.Measure E) : Type u_1

The product space containing a function and its first derivative.

Equations

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

def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.C1c {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Submodule ℝ (E → ℝ)

C¹ real-valued functions on E with compact support, as a submodule of E → ℝ.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.C1c = { carrier := {f : E → ℝ | ContDiff ℝ 1 f ∧ HasCompactSupport f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.grad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) : E → E

The pointwise gradient (as an E-valued function), via Riesz representation.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.grad f x = (InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f x)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.continuous_grad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} (hf : ContDiff ℝ 1 f) : Continuous (grad f)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.hasCompactSupport_grad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} (hf : HasCompactSupport f) : HasCompactSupport (grad f)

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.tsupport_grad_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) : tsupport (grad f) ⊆ tsupport f

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.memLp_of_mem_C1c {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : E → ℝ} (hf : f ∈ C1c) : MeasureTheory.MemLp f 2 μ

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.memLp_grad_of_mem_C1c {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : E → ℝ} (hf : f ∈ C1c) : MeasureTheory.MemLp (grad f) 2 μ

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : ↥C1c) : L2ℝ μ

The L² class of a C¹ compactly supported function.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2 μ f = MeasureTheory.MemLp.toLp ↑f ⋯

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2Grad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : ↥C1c) : L2E μ

The L² class of the gradient of a C¹ compactly supported function.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2Grad μ f = MeasureTheory.MemLp.toLp (RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.grad ↑f) ⋯

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2Linear {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : ↥C1c →ₗ[ℝ] L2ℝ μ

Linear map sending C¹_c functions to their L² classes.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2Linear μ = { toFun := RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2 μ, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2GradLinear {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : ↥C1c →ₗ[ℝ] L2E μ

Linear map sending C¹_c functions to the L² class of their gradient.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2GradLinear μ = { toFun := RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2Grad μ, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.graph {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : ↥C1c →ₗ[ℝ] H1Target μ

The graph map f ↦ (f, ∇f) into L² × L²(E).

Equations

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

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : Submodule ℝ (H1Target μ)

The Euclidean H¹ space (as a closed submodule of L² × L²(E)).

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1 μ = (RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.graph μ).range.topologicalClosure

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.isClosed_h1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : IsClosed ↑(h1 μ)

The Euclidean H¹ submodule is closed by construction.

instance RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instCompleteSpaceh1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : CompleteSpace ↥(h1 μ)

H¹ is complete (a Hilbert space once the ambient L² spaces are).

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1ToL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : ↥(h1 μ) →L[ℝ] L2ℝ μ

The continuous embedding H¹ → L².

Equations

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

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1ToL2Grad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : ↥(h1 μ) →L[ℝ] L2E μ

The continuous gradient map H¹ → L²(E).

Equations

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