Coarse-graining support: Support.Sobolev.Foundations.CoerciveH1

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

Coercive H¹ Scaffolding

This file packages the first reusable coercive layer above the witness-based H1Function API.

The key objects are:

• a gauge-fixed mean-zero carrier H1MeanZeroFunction U;
• typed L²(U) and L²(U; ℝ^d) realizations of u and ∇u;
• a bundled coercive estimate on the mean-zero carrier.

The future bounded-open-convex Poincare theorem should produce H1CoerciveEstimate U data, and the future Hodge proof should consume that coercive layer rather than the raw witness structures directly.

structure HCPolySupport.H1MeanZeroFunction {d : ℕ} (U : Set (Vec d)) : Type

Mean-zero H¹(U) functions, represented by a chosen H¹ witness together with the zero-average condition.

• toH1Function : H1Function U

  The H¹ function underlying the mean-zero Sobolev function.

• meanZero : MeanZeroOn U self.toH1Function.toFun

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instCoeH1Function {d : ℕ} {U : Set (Vec d)} : Coe (H1MeanZeroFunction U) (H1Function U)

Equations

• HCPolySupport.H1MeanZeroFunction.instCoeH1Function = { coe := fun (u : HCPolySupport.H1MeanZeroFunction U) => u.toH1Function }

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instCoeFunForallVecReal {d : ℕ} {U : Set (Vec d)} : CoeFun (H1MeanZeroFunction U) fun (x : H1MeanZeroFunction U) => Vec d → ℝ

Equations

• HCPolySupport.H1MeanZeroFunction.instCoeFunForallVecReal = { coe := fun (u : HCPolySupport.H1MeanZeroFunction U) => u.toH1Function.toFun }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.coe_mk {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (hmean : MeanZeroOn U u.toFun) : { toH1Function := u, meanZero := hmean }.toH1Function = u

theorem HCPolySupport.H1MeanZeroFunction.ext {d : ℕ} {U : Set (Vec d)} {u v : H1MeanZeroFunction U} (htoH1 : u.toH1Function = v.toH1Function) : u = v

theorem HCPolySupport.H1MeanZeroFunction.ext_iff {d : ℕ} {U : Set (Vec d)} {u v : H1MeanZeroFunction U} : u = v ↔ u.toH1Function = v.toH1Function

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instZero {d : ℕ} {U : Set (Vec d)} : Zero (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instZero = { zero := { toH1Function := 0, meanZero := ⋯ } }

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instAdd {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : Add (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instAdd = { add := fun (u v : HCPolySupport.H1MeanZeroFunction U) => { toH1Function := u.toH1Function + v.toH1Function, meanZero := ⋯ } }

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instSMulReal {d : ℕ} {U : Set (Vec d)} : SMul ℝ (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instSMulReal = { smul := fun (c : ℝ) (u : HCPolySupport.H1MeanZeroFunction U) => { toH1Function := c • u.toH1Function, meanZero := ⋯ } }

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instNeg {d : ℕ} {U : Set (Vec d)} : Neg (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instNeg = { neg := fun (u : HCPolySupport.H1MeanZeroFunction U) => -1 • u }

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instSub {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : Sub (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instSub = { sub := fun (u v : HCPolySupport.H1MeanZeroFunction U) => u + -v }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.toH1Function_zero {d : ℕ} {U : Set (Vec d)} : toH1Function 0 = 0

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.toH1Function_add {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u v : H1MeanZeroFunction U) : (u + v).toH1Function = u.toH1Function + v.toH1Function

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.toH1Function_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1MeanZeroFunction U) : (c • u).toH1Function = c • u.toH1Function

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.toH1Function_neg {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : (-u).toH1Function = -u.toH1Function

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.toH1Function_sub {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u v : H1MeanZeroFunction U) : (u - v).toH1Function = u.toH1Function - v.toH1Function

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instSMulNat {d : ℕ} {U : Set (Vec d)} : SMul ℕ (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instSMulNat = { smul := fun (n : ℕ) (u : HCPolySupport.H1MeanZeroFunction U) => ↑n • u }

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instSMulInt {d : ℕ} {U : Set (Vec d)} : SMul ℤ (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instSMulInt = { smul := fun (n : ℤ) (u : HCPolySupport.H1MeanZeroFunction U) => ↑n • u }

theorem HCPolySupport.H1MeanZeroFunction.toH1Function_injective {d : ℕ} {U : Set (Vec d)} : Function.Injective fun (u : H1MeanZeroFunction U) => u.toH1Function

@[instance_reducible]

instance HCPolySupport.H1MeanZeroFunction.instAddCommGroup {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : AddCommGroup (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instAddCommGroup = Function.Injective.addCommGroup (fun (u : HCPolySupport.H1MeanZeroFunction U) => u.toH1Function) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def HCPolySupport.H1MeanZeroFunction.toH1FunctionAddMonoidHom {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : H1MeanZeroFunction U →+ H1Function U

The additive homomorphism forgetting the zero-mean condition on an H¹ function.

Equations

• HCPolySupport.H1MeanZeroFunction.toH1FunctionAddMonoidHom = { toFun := fun (u : HCPolySupport.H1MeanZeroFunction U) => u.toH1Function, map_zero' := ⋯, map_add' := ⋯ }

@[instance_reducible]

noncomputable instance HCPolySupport.H1MeanZeroFunction.instModuleReal {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : Module ℝ (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instModuleReal = Function.Injective.module ℝ HCPolySupport.H1MeanZeroFunction.toH1FunctionAddMonoidHom ⋯ ⋯

noncomputable def HCPolySupport.H1Function.toScalarL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ↥(ScalarL2 U)

The scalar L²(U) realization of an H¹ function.

Equations

• u.toScalarL2 = HCPolySupport.toScalarL2 ⋯

noncomputable def HCPolySupport.H1Function.gradToVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ↥(VectorL2 U)

The vector L²(U; ℝ^d) realization of the weak gradient.

Equations

• u.gradToVectorL2 = HCPolySupport.toVectorL2 ⋯

noncomputable def HCPolySupport.H1Function.gradToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ↥(HilbertVectorL2 U)

The Hilbert-vector L²(U; ℝ^d) realization of the weak gradient.

Equations

• u.gradToHilbertVectorL2 = HCPolySupport.toHilbertVectorL2OfVecField ⋯

noncomputable def HCPolySupport.H1Function.gradCoordToScalarL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (i : Fin d) : ↥(ScalarL2 U)

The ith scalar L²(U) realization of the weak gradient.

Equations

• u.gradCoordToScalarL2 i = HCPolySupport.toScalarL2 ⋯

noncomputable def HCPolySupport.H1Function.gradientCoordL2NormSum {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ℝ

The sum of the scalar L² norms of the gradient coordinates.

Equations

• u.gradientCoordL2NormSum = ∑ i : Fin d, ‖u.gradCoordToScalarL2 i‖

theorem HCPolySupport.H1Function.coeFn_toScalarL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ↑↑u.toScalarL2 =ᵐ[volumeMeasureOn U] u.toFun

theorem HCPolySupport.H1Function.coeFn_gradToVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ↑↑u.gradToVectorL2 =ᵐ[volumeMeasureOn U] u.grad

theorem HCPolySupport.H1Function.coeFn_gradToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ↑↑u.gradToHilbertVectorL2 =ᵐ[volumeMeasureOn U] hilbertifyVecField u.grad

theorem HCPolySupport.H1Function.coeFn_gradCoordToScalarL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (i : Fin d) : ↑↑(u.gradCoordToScalarL2 i) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => u.grad x i

theorem HCPolySupport.H1Function.toScalarL2_add {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : (u + v).toScalarL2 = u.toScalarL2 + v.toScalarL2

theorem HCPolySupport.H1Function.toScalarL2_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1Function U) : (c • u).toScalarL2 = c • u.toScalarL2

theorem HCPolySupport.H1Function.gradToVectorL2_add {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : (u + v).gradToVectorL2 = u.gradToVectorL2 + v.gradToVectorL2

theorem HCPolySupport.H1Function.gradToVectorL2_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1Function U) : (c • u).gradToVectorL2 = c • u.gradToVectorL2

theorem HCPolySupport.H1Function.gradToHilbertVectorL2_add {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : (u + v).gradToHilbertVectorL2 = u.gradToHilbertVectorL2 + v.gradToHilbertVectorL2

theorem HCPolySupport.H1Function.gradToHilbertVectorL2_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1Function U) : (c • u).gradToHilbertVectorL2 = c • u.gradToHilbertVectorL2

theorem HCPolySupport.H1Function.gradCoordToScalarL2_add {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) (i : Fin d) : (u + v).gradCoordToScalarL2 i = u.gradCoordToScalarL2 i + v.gradCoordToScalarL2 i

theorem HCPolySupport.H1Function.gradCoordToScalarL2_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1Function U) (i : Fin d) : (c • u).gradCoordToScalarL2 i = c • u.gradCoordToScalarL2 i

theorem HCPolySupport.H1Function.norm_gradCoordToScalarL2_le {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (i : Fin d) : ‖u.gradCoordToScalarL2 i‖ ≤ ‖u.gradToVectorL2‖

theorem HCPolySupport.H1Function.gradientCoordL2NormSum_nonneg {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : 0 ≤ u.gradientCoordL2NormSum

theorem HCPolySupport.H1Function.gradientCoordL2NormSum_le {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : u.gradientCoordL2NormSum ≤ ↑d * ‖u.gradToVectorL2‖

noncomputable def HCPolySupport.H1Function.toMeanZero {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : H1MeanZeroFunction U

Normalize an H¹ function to its mean-zero representative by subtracting the average.

Equations

• u.toMeanZero = { toH1Function := u.subAverage, meanZero := ⋯ }

noncomputable def HCPolySupport.H1Function.normalizeMeanZero {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : H1MeanZeroFunction U

Alias for toMeanZero, matching the existing harmonic normalization API.

Equations

• u.normalizeMeanZero = u.toMeanZero

@[simp]

theorem HCPolySupport.H1Function.toMeanZero_toH1Function {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : u.toMeanZero.toH1Function = u.subAverage

@[simp]

theorem HCPolySupport.H1Function.normalizeMeanZero_toH1Function {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : u.normalizeMeanZero.toH1Function = u.subAverage

theorem HCPolySupport.H1Function.toMeanZero_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) (x : Vec d) : u.toMeanZero.toH1Function.toFun x = u.toFun x - integralAverage U u.toFun

theorem HCPolySupport.H1Function.toMeanZero_grad {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) (x : Vec d) : u.toMeanZero.toH1Function.grad x = u.grad x

theorem HCPolySupport.H1Function.gradToVectorL2_subAverage_eq {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : u.subAverage.gradToVectorL2 = u.gradToVectorL2

noncomputable def HCPolySupport.H1Function.gradientHilbertPairing {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (u : H1Function U) : ℝ

Pair a vector L² field with the weak gradient in the Hilbert L² ambient space.

Equations

• HCPolySupport.H1Function.gradientHilbertPairing hf u = inner ℝ (HCPolySupport.toHilbertVectorL2OfVecField hf) u.gradToHilbertVectorL2

theorem HCPolySupport.H1Function.gradientHilbertPairing_eq_integral {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (u : H1Function U) : gradientHilbertPairing hf u = ∫ (x : Vec d) in U, vecDot (f x) (u.grad x)

theorem HCPolySupport.H1Function.abs_gradientHilbertPairing_le {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (u : H1Function U) : |gradientHilbertPairing hf u| ≤ ‖toHilbertVectorL2OfVecField hf‖ * ‖u.gradToHilbertVectorL2‖

theorem HCPolySupport.H1Function.norm_gradToHilbertVectorL2_le {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ‖u.gradToHilbertVectorL2‖ ≤ ↑d * ‖u.gradToVectorL2‖

theorem HCPolySupport.H1Function.norm_gradToVectorL2_le_norm_gradToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ‖u.gradToVectorL2‖ ≤ ‖u.gradToHilbertVectorL2‖

noncomputable def HCPolySupport.H1MeanZeroFunction.toScalarL2 {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : ↥(ScalarL2 U)

The scalar L²(U) realization of a mean-zero H¹ function.

Equations

• u.toScalarL2 = u.toH1Function.toScalarL2

noncomputable def HCPolySupport.H1MeanZeroFunction.gradToVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : ↥(VectorL2 U)

The vector L²(U; ℝ^d) realization of the weak gradient.

Equations

• u.gradToVectorL2 = u.toH1Function.gradToVectorL2

noncomputable def HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : ↥(HilbertVectorL2 U)

The Hilbert-vector L²(U; ℝ^d) realization of a mean-zero H¹ function's weak gradient.

Equations

• u.gradToHilbertVectorL2 = u.toH1Function.gradToHilbertVectorL2

theorem HCPolySupport.H1MeanZeroFunction.toScalarL2_add {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u v : H1MeanZeroFunction U) : (u + v).toScalarL2 = u.toScalarL2 + v.toScalarL2

theorem HCPolySupport.H1MeanZeroFunction.toScalarL2_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1MeanZeroFunction U) : (c • u).toScalarL2 = c • u.toScalarL2

theorem HCPolySupport.H1MeanZeroFunction.gradToVectorL2_add {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u v : H1MeanZeroFunction U) : (u + v).gradToVectorL2 = u.gradToVectorL2 + v.gradToVectorL2

theorem HCPolySupport.H1MeanZeroFunction.gradToVectorL2_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1MeanZeroFunction U) : (c • u).gradToVectorL2 = c • u.gradToVectorL2

theorem HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2_add {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u v : H1MeanZeroFunction U) : (u + v).gradToHilbertVectorL2 = u.gradToHilbertVectorL2 + v.gradToHilbertVectorL2

theorem HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1MeanZeroFunction U) : (c • u).gradToHilbertVectorL2 = c • u.gradToHilbertVectorL2

noncomputable def HCPolySupport.H1MeanZeroFunction.valueL2Norm {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : ℝ

The scalar L² norm of a mean-zero H¹ function.

Equations

• u.valueL2Norm = ‖u.toScalarL2‖

noncomputable def HCPolySupport.H1MeanZeroFunction.gradientL2Norm {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : ℝ

The gradient-only L² norm which is the future coercive norm on the mean-zero layer.

Equations

• u.gradientL2Norm = ‖u.gradToVectorL2‖

@[instance_reducible]

noncomputable instance HCPolySupport.H1MeanZeroFunction.instNormOfIsFiniteMeasureVecVolumeMeasureOn {d : ℕ} {U : Set (Vec d)} : Norm (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instNormOfIsFiniteMeasureVecVolumeMeasureOn = { norm := fun (u : HCPolySupport.H1MeanZeroFunction U) => u.gradientL2Norm }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.norm_eq_gradientL2Norm {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : ‖u‖ = u.gradientL2Norm

theorem HCPolySupport.H1MeanZeroFunction.seminormedSpaceCore {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : SeminormedSpace.Core ℝ (H1MeanZeroFunction U)

@[instance_reducible]

noncomputable instance HCPolySupport.H1MeanZeroFunction.instSeminormedAddCommGroupOfIsFiniteMeasureVecVolumeMeasureOn {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : SeminormedAddCommGroup (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instSeminormedAddCommGroupOfIsFiniteMeasureVecVolumeMeasureOn = SeminormedAddCommGroup.ofCore ⋯

@[instance_reducible]

noncomputable instance HCPolySupport.H1MeanZeroFunction.instNormedSpaceReal {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : NormedSpace ℝ (H1MeanZeroFunction U)

Equations

• HCPolySupport.H1MeanZeroFunction.instNormedSpaceReal = { toModule := HCPolySupport.H1MeanZeroFunction.instModuleReal, norm_smul_le := ⋯ }

noncomputable def HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2Linear {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : H1MeanZeroFunction U →ₗ[ℝ] ↥(HilbertVectorL2 U)

The gradient realization as a linear map into the Hilbert L² ambient space.

Equations

• HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2Linear = { toFun := HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2Linear_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1MeanZeroFunction U) : gradToHilbertVectorL2Linear u = u.gradToHilbertVectorL2

noncomputable def HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2CLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : H1MeanZeroFunction U →L[ℝ] ↥(HilbertVectorL2 U)

The gradient realization as a continuous linear map for the gradient-only seminorm on the mean-zero coercive layer.

Equations

• HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2CLM = HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2Linear.mkContinuous ↑d ⋯

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.gradToHilbertVectorL2CLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1MeanZeroFunction U) : gradToHilbertVectorL2CLM u = u.gradToHilbertVectorL2

noncomputable def HCPolySupport.H1MeanZeroFunction.gradientPairing {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (u : H1MeanZeroFunction U) : ℝ

The gradient pairing of a mean-zero H¹ function against an L² vector field, realized through the Hilbert L² ambient space.

Equations

• HCPolySupport.H1MeanZeroFunction.gradientPairing hf u = inner ℝ (HCPolySupport.toHilbertVectorL2OfVecField hf) u.gradToHilbertVectorL2

theorem HCPolySupport.H1MeanZeroFunction.gradientPairing_eq_integral {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (u : H1MeanZeroFunction U) : gradientPairing hf u = ∫ (x : Vec d) in U, vecDot (f x) (u.toH1Function.grad x)

theorem HCPolySupport.H1MeanZeroFunction.gradientPairing_add {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hf : MemVectorL2 U f) (u v : H1MeanZeroFunction U) : gradientPairing hf (u + v) = gradientPairing hf u + gradientPairing hf v

theorem HCPolySupport.H1MeanZeroFunction.gradientPairing_smul {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (c : ℝ) (u : H1MeanZeroFunction U) : gradientPairing hf (c • u) = c * gradientPairing hf u

noncomputable def HCPolySupport.H1MeanZeroFunction.gradientPairingLinear {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hf : MemVectorL2 U f) : H1MeanZeroFunction U →ₗ[ℝ] ℝ

The gradient pairing, packaged as a linear functional on the mean-zero coercive H¹ layer.

Equations

• HCPolySupport.H1MeanZeroFunction.gradientPairingLinear hf = { toFun := HCPolySupport.H1MeanZeroFunction.gradientPairing hf, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.gradientPairingLinear_apply {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hf : MemVectorL2 U f) (u : H1MeanZeroFunction U) : (gradientPairingLinear hf) u = gradientPairing hf u

theorem HCPolySupport.H1MeanZeroFunction.abs_gradientPairing_le {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (u : H1MeanZeroFunction U) : |gradientPairing hf u| ≤ ‖toHilbertVectorL2OfVecField hf‖ * ‖u.gradToHilbertVectorL2‖

theorem HCPolySupport.H1MeanZeroFunction.norm_gradToHilbertVectorL2_le {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : ‖u.gradToHilbertVectorL2‖ ≤ ↑d * u.gradientL2Norm

theorem HCPolySupport.H1MeanZeroFunction.gradientL2Norm_le_norm_gradToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : u.gradientL2Norm ≤ ‖u.gradToHilbertVectorL2‖

theorem HCPolySupport.H1MeanZeroFunction.abs_gradientPairing_le_gradientL2Norm {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (u : H1MeanZeroFunction U) : |gradientPairing hf u| ≤ ↑d * ‖toHilbertVectorL2OfVecField hf‖ * u.gradientL2Norm

theorem HCPolySupport.H1MeanZeroFunction.norm_gradientPairingLinear_apply_le {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hf : MemVectorL2 U f) (u : H1MeanZeroFunction U) : ‖(gradientPairingLinear hf) u‖ ≤ ↑d * ‖toHilbertVectorL2OfVecField hf‖ * u.gradientL2Norm

noncomputable def HCPolySupport.H1MeanZeroFunction.gradientPairingCLM {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hf : MemVectorL2 U f) : H1MeanZeroFunction U →L[ℝ] ℝ

The gradient pairing as a continuous linear functional for the gradient-only seminorm on the mean-zero coercive layer.

Equations

• HCPolySupport.H1MeanZeroFunction.gradientPairingCLM hf = (HCPolySupport.H1MeanZeroFunction.gradientPairingLinear hf).mkContinuous (↑d * ‖HCPolySupport.toHilbertVectorL2OfVecField hf‖) ⋯

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.gradientPairingCLM_apply {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hf : MemVectorL2 U f) (u : H1MeanZeroFunction U) : (gradientPairingCLM hf) u = gradientPairing hf u

structure HCPolySupport.H1CoerciveEstimate {d : ℕ} (U : Set (Vec d)) : Type

Bundled coercive estimate on the mean-zero H¹ layer.

• constantValue : ℝ

  The nonnegative constant bounding the L² norm of a mean-zero H¹ function by its gradient L² norm.

• constant_nonneg : 0 ≤ self.constantValue
• bound (u : H1MeanZeroFunction U) : u.valueL2Norm ≤ self.constantValue * u.gradientL2Norm

theorem HCPolySupport.H1CoerciveEstimate.bound_subAverage {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) (u : H1Function U) : u.toMeanZero.valueL2Norm ≤ hC.constantValue * ‖u.gradToVectorL2‖

noncomputable def HCPolySupport.H1MeanZeroFunction.toScalarL2Linear {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : H1MeanZeroFunction U →ₗ[ℝ] ↥(ScalarL2 U)

The value realization as a linear map into scalar L²(U).

Equations

• HCPolySupport.H1MeanZeroFunction.toScalarL2Linear = { toFun := HCPolySupport.H1MeanZeroFunction.toScalarL2, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.toScalarL2Linear_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1MeanZeroFunction U) : toScalarL2Linear u = u.toScalarL2

theorem HCPolySupport.H1MeanZeroFunction.norm_toScalarL2Linear_apply_le {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) (u : H1MeanZeroFunction U) : ‖toScalarL2Linear u‖ ≤ hC.constantValue * ‖u‖

noncomputable def HCPolySupport.H1MeanZeroFunction.toScalarL2CLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) : H1MeanZeroFunction U →L[ℝ] ↥(ScalarL2 U)

The value realization as a continuous linear map once a coercive estimate controls ‖u‖_{L²} by the gradient-only seminorm.

Equations

• HCPolySupport.H1MeanZeroFunction.toScalarL2CLM hC = HCPolySupport.H1MeanZeroFunction.toScalarL2Linear.mkContinuous hC.constantValue ⋯

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.toScalarL2CLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) (u : H1MeanZeroFunction U) : (toScalarL2CLM hC) u = u.toScalarL2

noncomputable def HCPolySupport.H1MeanZeroFunction.toHilbertProductLinear {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : H1MeanZeroFunction U →ₗ[ℝ] ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)

The mean-zero coercive layer packaged in the Hilbert product L²(U) × L²(U; ℝᵈ).

Equations

• HCPolySupport.H1MeanZeroFunction.toHilbertProductLinear = { toFun := fun (u : HCPolySupport.H1MeanZeroFunction U) => (u.toScalarL2, u.gradToHilbertVectorL2), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.toHilbertProductLinear_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1MeanZeroFunction U) : toHilbertProductLinear u = (u.toScalarL2, u.gradToHilbertVectorL2)

theorem HCPolySupport.H1MeanZeroFunction.norm_le_norm_toHilbertProductLinear_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1MeanZeroFunction U) : ‖u‖ ≤ ‖toHilbertProductLinear u‖

theorem HCPolySupport.H1MeanZeroFunction.norm_toHilbertProductLinear_apply_le {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) (u : H1MeanZeroFunction U) : ‖toHilbertProductLinear u‖ ≤ max hC.constantValue ↑d * ‖u‖

noncomputable def HCPolySupport.H1MeanZeroFunction.toHilbertProductCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) : H1MeanZeroFunction U →L[ℝ] ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)

The mean-zero coercive layer as a continuous linear map into L²(U) × L²(U; ℝᵈ) once a coercive estimate is available.

Equations

• HCPolySupport.H1MeanZeroFunction.toHilbertProductCLM hC = HCPolySupport.H1MeanZeroFunction.toHilbertProductLinear.mkContinuous (max hC.constantValue ↑d) ⋯

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.toHilbertProductCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) (u : H1MeanZeroFunction U) : (toHilbertProductCLM hC) u = (u.toScalarL2, u.gradToHilbertVectorL2)

theorem HCPolySupport.H1MeanZeroFunction.norm_le_norm_toHilbertProductCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) (u : H1MeanZeroFunction U) : ‖u‖ ≤ ‖(toHilbertProductCLM hC) u‖