Coarse-graining support: Support.Sobolev.Fractional.EuclideanWspCompletedDualGraph

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Completed two-component graph for cube Euclidean fractional Sobolev tests

The approved inhomogeneous W^(s,p) power norm is realized as the ambient L^p norm of the graph containing a scale-weighted field component and its Gagliardo kernel. This file only introduces that ambient space, its smooth graph, and the closure of the graph; it makes no claim about a completed dual pairing.

instance HCPolySupport.instCubeEuclideanWspGraphFactOneLe (p : FiniteLpExponent) : Fact (1 ≤ p.exponent)

@[reducible, inline]

noncomputable abbrev HCPolySupport.CubeEuclideanWspGraphComponent {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) : Bool → Type

The two heterogeneous L^p components of the fractional-Sobolev graph.

Equations

• HCPolySupport.CubeEuclideanWspGraphComponent Q p false = ↥(MeasureTheory.Lp (HCPolySupport.HilbertVec d) p.exponent (HCPolySupport.normalizedCubeMeasure Q))
• HCPolySupport.CubeEuclideanWspGraphComponent Q p true = ↥(MeasureTheory.Lp (HCPolySupport.HilbertVec d) p.exponent (HCPolySupport.Gagliardo.gagliardoCubeMeasure Q))

@[instance_reducible]

noncomputable instance HCPolySupport.instCubeEuclideanWspGraphComponentNormedAddCommGroup {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) [Fact (1 ≤ p.exponent)] (b : Bool) : NormedAddCommGroup (CubeEuclideanWspGraphComponent Q p b)

Equations

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

@[instance_reducible]

noncomputable instance HCPolySupport.instCubeEuclideanWspGraphComponentNormedSpace {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) [Fact (1 ≤ p.exponent)] (b : Bool) : NormedSpace ℝ (CubeEuclideanWspGraphComponent Q p b)

Equations

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

@[reducible, inline]

noncomputable abbrev HCPolySupport.CubeEuclideanWspGraphAmbient {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) : Type

The finite two-component ambient L^p space for the full cube W^(s,p) graph.

Equations

• HCPolySupport.CubeEuclideanWspGraphAmbient Q p = PiLp p.exponent (HCPolySupport.CubeEuclideanWspGraphComponent Q p)

instance HCPolySupport.instCompleteSpaceCubeEuclideanWspGraphAmbient {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) : CompleteSpace (CubeEuclideanWspGraphAmbient Q p)

The two-component ambient graph space is complete because both of its L^p components are complete.

noncomputable def HCPolySupport.cubeEuclideanWspGraphFieldScale {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) : ℝ

The real scale applied to the field component of the full W^(s,p) graph.

Equations

• HCPolySupport.cubeEuclideanWspGraphFieldScale Q s = HCPolySupport.cubeScaleFactor Q ^ (-↑s)

noncomputable def HCPolySupport.CubeEuclideanWspSmoothTest.graphFieldComponent {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) : CubeEuclideanWspGraphComponent Q p false

The normalized Hilbert-vector Lᵖ field component of the graph associated with a smooth fractional Sobolev test.

Equations

• h.graphFieldComponent = MeasureTheory.MemLp.toLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (h.toField x)) ⋯

noncomputable def HCPolySupport.CubeEuclideanWspSmoothTest.graphKernelComponent {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) : CubeEuclideanWspGraphComponent Q p true

The Lᵖ fractional difference kernel component of the graph associated with a smooth Sobolev test.

Equations

• h.graphKernelComponent = MeasureTheory.MemLp.toLp (HCPolySupport.cubeEuclideanWspKernel s p h.toField) ⋯

theorem HCPolySupport.CubeEuclideanWspSmoothTest.graphFieldComponent_add {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h k : CubeEuclideanWspSmoothTest Q s p) : (h + k).graphFieldComponent = h.graphFieldComponent + k.graphFieldComponent

theorem HCPolySupport.CubeEuclideanWspSmoothTest.graphFieldComponent_smul {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (c : ℝ) (h : CubeEuclideanWspSmoothTest Q s p) : (c • h).graphFieldComponent = c • h.graphFieldComponent

theorem HCPolySupport.CubeEuclideanWspSmoothTest.graphKernelComponent_add {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h k : CubeEuclideanWspSmoothTest Q s p) : (h + k).graphKernelComponent = h.graphKernelComponent + k.graphKernelComponent

theorem HCPolySupport.CubeEuclideanWspSmoothTest.graphKernelComponent_smul {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (c : ℝ) (h : CubeEuclideanWspSmoothTest Q s p) : (c • h).graphKernelComponent = c • h.graphKernelComponent

noncomputable def HCPolySupport.CubeEuclideanWspSmoothTest.graphPoint {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) : CubeEuclideanWspGraphAmbient Q p

The two ambient L^p components of a smooth fractional-Sobolev test.

Equations

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

noncomputable def HCPolySupport.CubeEuclideanWspSmoothTest.graph {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : CubeEuclideanWspSmoothTest Q s p →ₗ[ℝ] CubeEuclideanWspGraphAmbient Q p

The linear smooth graph in the two-component ambient L^p space.

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.graph = { toFun := HCPolySupport.CubeEuclideanWspSmoothTest.graphPoint, map_add' := ⋯, map_smul' := ⋯ }

theorem HCPolySupport.CubeEuclideanWspSmoothTest.graph_enorm_eq_cubeEuclideanWspFullENorm {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspSmoothTest Q s p) : ‖graph h‖ₑ = cubeEuclideanWspFullENorm Q s p h.toField

The ambient L^p norm of a smooth graph point is exactly the approved full cube fractional-Sobolev norm.

noncomputable def HCPolySupport.CubeEuclideanWspSmoothTest.completedGraphSubmodule {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) : Submodule ℝ (CubeEuclideanWspGraphAmbient Q p)

The closed submodule generated by the smooth two-component graph.

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.completedGraphSubmodule Q s p = HCPolySupport.CubeEuclideanWspSmoothTest.graph.range.topologicalClosure

@[reducible, inline]

noncomputable abbrev HCPolySupport.CubeEuclideanWspSmoothTest.CubeEuclideanWspCompletedDualGraph {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) : Type

The completed graph carrier, retaining its inherited normed and complete linear-space structure.

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.CubeEuclideanWspCompletedDualGraph Q s p = ↥(HCPolySupport.CubeEuclideanWspSmoothTest.completedGraphSubmodule Q s p)

instance HCPolySupport.CubeEuclideanWspSmoothTest.instCompleteSpaceCubeEuclideanWspCompletedDualGraph {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) : CompleteSpace (CubeEuclideanWspCompletedDualGraph Q s p)

The closure of the smooth graph is a complete normed space.

noncomputable def HCPolySupport.CubeEuclideanWspSmoothTest.graphToCompleted {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : CubeEuclideanWspSmoothTest Q s p →ₗ[ℝ] CubeEuclideanWspCompletedDualGraph Q s p

The canonical linear inclusion of smooth tests into their completed graph carrier.

Equations

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

theorem HCPolySupport.CubeEuclideanWspSmoothTest.denseRange_graphToCompleted {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} : DenseRange ⇑graphToCompleted

Smooth graph points are dense in the completed graph carrier by construction.