ZeroTraceSobolev

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Zero-trace Sobolev space

This file defines the Hilbert completion of the value-gradient graph of H10Function U, together with its basic component maps and realization theorem.

instance DivergenceFormProcess.Form.instFactTwoENNRealNeTop : Fact (2 ≠ ⊤)

instance DivergenceFormProcess.Form.instCountablyGeneratedVec {d : ℕ} : MeasurableSpace.CountablyGenerated (HCPolySupport.Vec d)

instance DivergenceFormProcess.Form.instSFiniteVolumeMeasureOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} : MeasureTheory.SFinite (HCPolySupport.volumeMeasureOn U)

instance DivergenceFormProcess.Form.instIsSeparableVolumeMeasureOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} : MeasureTheory.IsSeparable (HCPolySupport.volumeMeasureOn U)

instance DivergenceFormProcess.Form.instSecondCountableScalarL2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} : SecondCountableTopology ↥(HCPolySupport.ScalarL2 U)

instance DivergenceFormProcess.Form.instSecondCountableHilbertVectorL2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} : SecondCountableTopology ↥(HCPolySupport.HilbertVectorL2 U)

@[reducible, inline]

noncomputable abbrev DivergenceFormProcess.Form.zeroTraceAmbient {d : ℕ} {U : Set (HCPolySupport.Vec d)} : Type

The L² value-gradient product with its Hilbert product norm.

Equations

• DivergenceFormProcess.Form.zeroTraceAmbient = WithLp 2 (↥(HCPolySupport.ScalarL2 U) × ↥(HCPolySupport.HilbertVectorL2 U))

instance DivergenceFormProcess.Form.instSecondCountableZeroTraceAmbient {d : ℕ} {U : Set (HCPolySupport.Vec d)} : SecondCountableTopology zeroTraceAmbient

@[reducible, inline]

noncomputable abbrev DivergenceFormProcess.Form.zeroTraceAmbientEquiv {d : ℕ} {U : Set (HCPolySupport.Vec d)} : zeroTraceAmbient ≃L[ℝ] ↥(HCPolySupport.ScalarL2 U) × ↥(HCPolySupport.HilbertVectorL2 U)

The continuous linear equivalence to the ordinary value-gradient product.

Equations

• DivergenceFormProcess.Form.zeroTraceAmbientEquiv = WithLp.prodContinuousLinearEquiv 2 ℝ ↥(HCPolySupport.ScalarL2 U) ↥(HCPolySupport.HilbertVectorL2 U)

@[reducible, inline]

noncomputable abbrev DivergenceFormProcess.Form.zeroTraceClosedSubmodule {d : ℕ} {U : Set (HCPolySupport.Vec d)} : ClosedSubmodule ℝ zeroTraceAmbient

The closed value-gradient submodule defining the zero-trace Sobolev completion.

Equations

• DivergenceFormProcess.Form.zeroTraceClosedSubmodule = ClosedSubmodule.comap (↑DivergenceFormProcess.Form.zeroTraceAmbientEquiv) (HCPolySupport.h10GraphClosedSubmodule U)

noncomputable def DivergenceFormProcess.Form.ZeroTraceSobolev {d : ℕ} (U : Set (HCPolySupport.Vec d)) : Type

The Hilbert completion of the value–gradient graph generated by H10Function U. On open bounded convex domains, every element has an honest H10Function representative by ZeroTraceSobolev.exists_h10Function.

Equations

• DivergenceFormProcess.Form.ZeroTraceSobolev U = ↥↑DivergenceFormProcess.Form.zeroTraceClosedSubmodule

@[instance_reducible]

noncomputable instance DivergenceFormProcess.Form.ZeroTraceSobolev.instNormedAddCommGroup {d : ℕ} {U : Set (HCPolySupport.Vec d)} : NormedAddCommGroup (ZeroTraceSobolev U)

Equations

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

@[instance_reducible]

noncomputable instance DivergenceFormProcess.Form.ZeroTraceSobolev.instNormedSpaceReal {d : ℕ} {U : Set (HCPolySupport.Vec d)} : NormedSpace ℝ (ZeroTraceSobolev U)

Equations

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

@[instance_reducible]

noncomputable instance DivergenceFormProcess.Form.ZeroTraceSobolev.instInnerProductSpaceReal {d : ℕ} {U : Set (HCPolySupport.Vec d)} : InnerProductSpace ℝ (ZeroTraceSobolev U)

Equations

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

instance DivergenceFormProcess.Form.ZeroTraceSobolev.instCompleteSpace {d : ℕ} {U : Set (HCPolySupport.Vec d)} : CompleteSpace (ZeroTraceSobolev U)

instance DivergenceFormProcess.Form.ZeroTraceSobolev.instSecondCountableTopology {d : ℕ} {U : Set (HCPolySupport.Vec d)} : SecondCountableTopology (ZeroTraceSobolev U)

noncomputable def DivergenceFormProcess.Form.ZeroTraceSobolev.toL2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} : ZeroTraceSobolev U →L[ℝ] ↥(HCPolySupport.ScalarL2 U)

The scalar L² component of a zero-trace Sobolev element.

Equations

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

noncomputable def DivergenceFormProcess.Form.ZeroTraceSobolev.gradient {d : ℕ} {U : Set (HCPolySupport.Vec d)} : ZeroTraceSobolev U →L[ℝ] ↥(HCPolySupport.HilbertVectorL2 U)

The Hilbert-vector L² gradient of a zero-trace Sobolev element.

Equations

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

noncomputable def DivergenceFormProcess.Form.ZeroTraceSobolev.ofH10Function {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : HCPolySupport.H10Function U) : ZeroTraceSobolev U

Embed an honest zero-trace Sobolev function in its value–gradient graph completion.

Equations

• DivergenceFormProcess.Form.ZeroTraceSobolev.ofH10Function u = ⟨DivergenceFormProcess.Form.zeroTraceAmbientEquiv.symm (u.toScalarL2, u.gradToHilbertVectorL2), ⋯⟩

@[simp]

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.toL2_ofH10Function {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : HCPolySupport.H10Function U) : toL2 (ofH10Function u) = u.toScalarL2

@[simp]

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.gradient_ofH10Function {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : HCPolySupport.H10Function U) : gradient (ofH10Function u) = u.gradToHilbertVectorL2

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.ext {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u v : ZeroTraceSobolev U} (hvalue : toL2 u = toL2 v) (hgradient : gradient u = gradient v) : u = v

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.ext_iff {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u v : ZeroTraceSobolev U} : u = v ↔ toL2 u = toL2 v ∧ gradient u = gradient v

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.norm_sq_eq {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : ZeroTraceSobolev U) : ‖u‖ ^ 2 = ‖toL2 u‖ ^ 2 + ‖gradient u‖ ^ 2

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.norm_toL2_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : ZeroTraceSobolev U) : ‖toL2 u‖ ≤ ‖u‖

The scalar component has norm at most the full value--gradient norm.

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.exists_h10Function {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (z : ZeroTraceSobolev U) : ∃ (u : HCPolySupport.H10Function U), u.toScalarL2 = toL2 z ∧ u.gradToHilbertVectorL2 = gradient z

Recover an honest zero-trace Sobolev representative on the domains where the pinned CoarseGraining graph-realization theorem applies.