RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.H2

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

This is a “graph-closure” Sobolev-style construction analogous to Euclidean.H1: we take C² compactly supported functions, map them to their L² classes together with their gradient and Hessian, and define H² as the topological closure of the range inside an ambient L² product.

No Rellich/elliptic regularity theorems are proved here; this file is purely definitional/API.

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.C2c {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.C2c = { carrier := {f : E → ℝ | ContDiff ℝ 2 f ∧ HasCompactSupport f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.C2c_le_C1c {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : C2c ≤ C1c

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.C2cToC1cLinear {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : ↥C2c →ₗ[ℝ] ↥C1c

The coercion map C²_c →ₗ C¹_c.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.C2cToC1cLinear = Submodule.inclusion ⋯

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

The pointwise Hessian (as an E →L E-valued function), defined as fderiv of grad.

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.hess f x = fderiv ℝ (RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.grad f) x

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

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

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

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

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.hess_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f g : E → ℝ} (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g) : hess (f + g) = hess f + hess g

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.hess_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (c : ℝ) {f : E → ℝ} (hf : ContDiff ℝ 2 f) : hess (c • f) = c • hess f

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

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

Equations

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

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

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

Equations

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

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

Linear map C²_c → L² (via the inclusion C²_c ⊆ C¹_c).

Equations

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

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

Linear map C²_c → L²(E) for gradients (via the inclusion C²_c ⊆ C¹_c).

Equations

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

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

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

Equations

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

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

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

Equations

• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h2 μ = (RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.graph2 μ).range.topologicalClosure

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

The Euclidean H² submodule is closed by construction.

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

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

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h2ToL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : ↥(h2 μ) →L[ℝ] RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.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.h2ToL2Grad {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : ↥(h2 μ) →L[ℝ] RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.L2E✝ μ

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

Equations

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

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

The continuous Hessian map H² → L²(E →L E).

Equations

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