Coarse-graining support: Support.Sobolev.Foundations.H1Graph.CoerciveHilbert

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

@[reducible, inline]

noncomputable abbrev HCPolySupport.H1CoerciveHilbertAmbient {d : ℕ} {U : Set (Vec d)} : Type

The canonical complete Hilbert carrier for the mean-zero coercive H¹ layer: the closed mean-zero weak-gradient graph inside L²(U) × L²(U; HilbertVec d).

Equations

• HCPolySupport.H1CoerciveHilbertAmbient = WithLp 2 (↥(HCPolySupport.ScalarL2 U) × ↥(HCPolySupport.HilbertVectorL2 U))

@[reducible, inline]

noncomputable abbrev HCPolySupport.h1CoerciveHilbertAmbientEquiv {d : ℕ} {U : Set (Vec d)} : H1CoerciveHilbertAmbient ≃L[ℝ] ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)

The continuous linear equivalence between the ℓ² product ambient space and the ordinary product of value and gradient L² spaces.

Equations

• HCPolySupport.h1CoerciveHilbertAmbientEquiv = WithLp.prodContinuousLinearEquiv 2 ℝ ↥(HCPolySupport.ScalarL2 U) ↥(HCPolySupport.HilbertVectorL2 U)

@[reducible, inline]

noncomputable abbrev HCPolySupport.h1CoerciveHilbertClosedSubmodule {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ClosedSubmodule ℝ H1CoerciveHilbertAmbient

The closed mean-zero weak H¹ graph transported into the ℓ² product of value and gradient L² spaces.

Equations

• HCPolySupport.h1CoerciveHilbertClosedSubmodule = ClosedSubmodule.comap (↑HCPolySupport.h1CoerciveHilbertAmbientEquiv) HCPolySupport.h1MeanZeroGraphClosedSubmodule

@[reducible, inline]

noncomputable abbrev HCPolySupport.h1CoerciveHilbertSubmodule {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : Submodule ℝ H1CoerciveHilbertAmbient

The real submodule underlying the closed mean-zero weak H¹ graph in the ℓ² product ambient space.

Equations

• HCPolySupport.h1CoerciveHilbertSubmodule = ↑HCPolySupport.h1CoerciveHilbertClosedSubmodule

@[reducible, inline]

noncomputable abbrev HCPolySupport.H1CoerciveHilbertSpace {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : Type

The Hilbert-space carrier of the closed mean-zero weak H¹ graph.

Equations

• HCPolySupport.H1CoerciveHilbertSpace = ↥HCPolySupport.h1CoerciveHilbertSubmodule

@[instance_reducible]

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

Equations

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

@[instance_reducible]

noncomputable instance HCPolySupport.H1CoerciveHilbert.instNormedAddCommGroupH1CoerciveHilbertSpace {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : NormedAddCommGroup H1CoerciveHilbertSpace

Equations

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

@[instance_reducible]

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

Equations

• HCPolySupport.H1CoerciveHilbert.instNormedSpaceRealH1CoerciveHilbertSpace = { toModule := HCPolySupport.h1CoerciveHilbertSubmodule.module, norm_smul_le := ⋯ }

@[instance_reducible]

noncomputable instance HCPolySupport.H1CoerciveHilbert.instInnerProductSpaceRealH1CoerciveHilbertSpace {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : InnerProductSpace ℝ H1CoerciveHilbertSpace

Equations

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

instance HCPolySupport.H1CoerciveHilbert.instCompleteSpaceH1CoerciveHilbertSpace {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : CompleteSpace H1CoerciveHilbertSpace

@[reducible, inline]

abbrev HCPolySupport.H1CoerciveHilbert.value {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z : H1CoerciveHilbertSpace) : ↥(ScalarL2 U)

The scalar L²(U) value component of a point in the coercive Hilbert graph.

Equations

• HCPolySupport.H1CoerciveHilbert.value z = WithLp.fst ↑z

@[reducible, inline]

abbrev HCPolySupport.H1CoerciveHilbert.gradient {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z : H1CoerciveHilbertSpace) : ↥(HilbertVectorL2 U)

The Hilbert-vector L²(U) gradient component of a point in the coercive Hilbert graph.

Equations

• HCPolySupport.H1CoerciveHilbert.gradient z = WithLp.snd ↑z

noncomputable def HCPolySupport.H1CoerciveHilbert.valueCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : H1CoerciveHilbertSpace →L[ℝ] ↥(ScalarL2 U)

The scalar-value projection from the coercive Hilbert graph.

Equations

• HCPolySupport.H1CoerciveHilbert.valueCLM = WithLp.fstL 2 ℝ ↥(HCPolySupport.ScalarL2 U) ↥(HCPolySupport.HilbertVectorL2 U) ∘SL HCPolySupport.h1CoerciveHilbertSubmodule.subtypeL

@[simp]

theorem HCPolySupport.H1CoerciveHilbert.valueCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z : H1CoerciveHilbertSpace) : valueCLM z = value z

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

The gradient projection from the coercive Hilbert graph.

Equations

• HCPolySupport.H1CoerciveHilbert.gradientCLM = WithLp.sndL 2 ℝ ↥(HCPolySupport.ScalarL2 U) ↥(HCPolySupport.HilbertVectorL2 U) ∘SL HCPolySupport.h1CoerciveHilbertSubmodule.subtypeL

@[simp]

theorem HCPolySupport.H1CoerciveHilbert.gradientCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z : H1CoerciveHilbertSpace) : gradientCLM z = gradient z

noncomputable def HCPolySupport.H1CoerciveHilbert.gradientBilin {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : H1CoerciveHilbertSpace →L[ℝ] H1CoerciveHilbertSpace →L[ℝ] ℝ

The gradient-energy bilinear form on the coercive Hilbert graph.

Equations

• HCPolySupport.H1CoerciveHilbert.gradientBilin = ⋯.toContinuousLinearMap.bilinearComp HCPolySupport.H1CoerciveHilbert.gradientCLM HCPolySupport.H1CoerciveHilbert.gradientCLM

@[simp]

theorem HCPolySupport.H1CoerciveHilbert.gradientBilin_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z w : H1CoerciveHilbertSpace) : (gradientBilin z) w = inner ℝ (gradient z) (gradient w)

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

The forcing functional z ↦ ⟪f, ∇z⟫ on the coercive Hilbert graph.

Equations

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

@[simp]

theorem HCPolySupport.H1CoerciveHilbert.forcingFunctionalCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : MemVectorL2 U f) (z : H1CoerciveHilbertSpace) : (forcingFunctionalCLM hf) z = inner ℝ (toHilbertVectorL2OfVecField hf) (gradient z)

noncomputable def HCPolySupport.H1CoerciveHilbert.scalarForcingFunctionalCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {F : Vec d → ℝ} (hF : MemScalarL2 U F) : H1CoerciveHilbertSpace →L[ℝ] ℝ

The scalar forcing functional z ↦ ⟪F, z⟫ on the coercive Hilbert graph.

Equations

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

@[simp]

theorem HCPolySupport.H1CoerciveHilbert.scalarForcingFunctionalCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {F : Vec d → ℝ} (hF : MemScalarL2 U F) (z : H1CoerciveHilbertSpace) : (scalarForcingFunctionalCLM hF) z = inner ℝ (toScalarL2 hF) (value z)

noncomputable def HCPolySupport.H1CoerciveHilbert.forcingRieszMap {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : (H1CoerciveHilbertSpace →L[ℝ] ℝ) → H1CoerciveHilbertSpace

The Riesz representative of the forcing functional on the coercive Hilbert graph.

Equations

• HCPolySupport.H1CoerciveHilbert.forcingRieszMap ℓ = (InnerProductSpace.toDual ℝ HCPolySupport.H1CoerciveHilbertSpace).symm ℓ

theorem HCPolySupport.H1CoerciveHilbert.inner_forcingRieszMap_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (ℓ : H1CoerciveHilbertSpace →L[ℝ] ℝ) (z : H1CoerciveHilbertSpace) : inner ℝ (forcingRieszMap ℓ) z = ℓ z

noncomputable def HCPolySupport.H1CoerciveHilbert.forcingRieszRep {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : MemVectorL2 U f) : H1CoerciveHilbertSpace

The Riesz representative of the forcing functional on the coercive Hilbert graph.

Equations

• HCPolySupport.H1CoerciveHilbert.forcingRieszRep hf = HCPolySupport.H1CoerciveHilbert.forcingRieszMap (HCPolySupport.H1CoerciveHilbert.forcingFunctionalCLM hf)

theorem HCPolySupport.H1CoerciveHilbert.inner_forcingRieszRep_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : MemVectorL2 U f) (z : H1CoerciveHilbertSpace) : inner ℝ (forcingRieszRep hf) z = (forcingFunctionalCLM hf) z

noncomputable def HCPolySupport.H1CoerciveHilbert.toH1MeanZeroFunction {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z : H1CoerciveHilbertSpace) : H1MeanZeroFunction U

Recover the mean-zero H¹ witness represented by a point of the coercive Hilbert graph.

Equations

• HCPolySupport.H1CoerciveHilbert.toH1MeanZeroFunction z = { toH1Function := HCPolySupport.toH1FunctionOfMemH1Graph (HCPolySupport.h1CoerciveHilbertAmbientEquiv ↑z) ⋯, meanZero := ⋯ }

@[simp]

theorem HCPolySupport.H1CoerciveHilbert.toH1MeanZeroFunction_toScalarL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z : H1CoerciveHilbertSpace) : (toH1MeanZeroFunction z).toScalarL2 = value z

@[simp]

theorem HCPolySupport.H1CoerciveHilbert.toH1MeanZeroFunction_gradToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z : H1CoerciveHilbertSpace) : (toH1MeanZeroFunction z).gradToHilbertVectorL2 = gradient z

theorem HCPolySupport.H1CoerciveHilbert.norm_value_le_constant_mul_norm_gradient {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) (z : H1CoerciveHilbertSpace) : ‖value z‖ ≤ hC.constantValue * ‖gradient z‖

theorem HCPolySupport.H1CoerciveHilbert.norm_le_max_constant_one_mul_norm_gradient {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) (z : H1CoerciveHilbertSpace) : ‖z‖ ≤ (hC.constantValue + 1) * ‖gradient z‖

theorem HCPolySupport.H1CoerciveHilbert.isCoercive_gradientBilin {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hC : H1CoerciveEstimate U) : IsCoercive gradientBilin

noncomputable def HCPolySupport.H1CoerciveHilbert.gradientProblemSolution {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) : H1CoerciveHilbertSpace

The unique coercive-Hilbert graph element solving the weak gradient problem with forcing f.

Equations

• HCPolySupport.H1CoerciveHilbert.gradientProblemSolution hf hC = ⋯.continuousLinearEquivOfBilin.symm (HCPolySupport.H1CoerciveHilbert.forcingRieszRep hf)

theorem HCPolySupport.H1CoerciveHilbert.gradientBilin_gradientProblemSolution_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) (z : H1CoerciveHilbertSpace) : (gradientBilin (gradientProblemSolution hf hC)) z = (forcingFunctionalCLM hf) z

noncomputable def HCPolySupport.H1CoerciveHilbert.scalarRhsProblemSolution {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {F : Vec d → ℝ} (hF : MemScalarL2 U F) (hC : H1CoerciveEstimate U) : H1CoerciveHilbertSpace

The unique coercive-Hilbert graph element solving the scalar right-hand-side problem with forcing F.

Equations

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

theorem HCPolySupport.H1CoerciveHilbert.gradientBilin_scalarRhsProblemSolution_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {F : Vec d → ℝ} (hF : MemScalarL2 U F) (hC : H1CoerciveEstimate U) (z : H1CoerciveHilbertSpace) : (gradientBilin (scalarRhsProblemSolution hF hC)) z = (scalarForcingFunctionalCLM hF) z

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

The element of the mean-zero H¹ Hilbert graph given by the L² value and gradient of u.

Equations

• u.toH1CoerciveHilbertSpace = ⟨HCPolySupport.h1CoerciveHilbertAmbientEquiv.symm (u.toScalarL2, u.gradToHilbertVectorL2), ⋯⟩

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.H1CoerciveHilbert_value_toH1CoerciveHilbertSpace {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1MeanZeroFunction U) : H1CoerciveHilbert.value u.toH1CoerciveHilbertSpace = u.toScalarL2

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.H1CoerciveHilbert_gradient_toH1CoerciveHilbertSpace {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1MeanZeroFunction U) : H1CoerciveHilbert.gradient u.toH1CoerciveHilbertSpace = u.gradToHilbertVectorL2

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

theorem HCPolySupport.H1MeanZeroFunction.H1CoerciveHilbert_scalarForcingFunctionalCLM_apply_toH1CoerciveHilbertSpace {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {F : Vec d → ℝ} (hF : MemScalarL2 U F) (u : H1MeanZeroFunction U) : (H1CoerciveHilbert.scalarForcingFunctionalCLM hF) u.toH1CoerciveHilbertSpace = inner ℝ (HCPolySupport.toScalarL2 hF) u.toScalarL2

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

The mean-zero H¹ weak solution represented by the coercive Hilbert graph solution of the gradient problem.

Equations

• HCPolySupport.H1MeanZeroFunction.gradientProblemSolution hf hC = HCPolySupport.H1CoerciveHilbert.toH1MeanZeroFunction (HCPolySupport.H1CoerciveHilbert.gradientProblemSolution hf hC)

theorem HCPolySupport.H1MeanZeroFunction.gradientProblemSolution_firstVariation {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) (u : H1MeanZeroFunction U) : inner ℝ (gradientProblemSolution hf hC).gradToHilbertVectorL2 u.gradToHilbertVectorL2 = gradientPairing hf u

theorem HCPolySupport.H1MeanZeroFunction.gradientProblemSolution_firstVariation_eq_integral {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) (u : H1MeanZeroFunction U) : ∫ (x : Vec d) in U, vecDot ((gradientProblemSolution hf hC).toH1Function.grad x) (u.toH1Function.grad x) = ∫ (x : Vec d) in U, vecDot (f x) (u.toH1Function.grad x)

noncomputable def HCPolySupport.H1MeanZeroFunction.scalarRhsProblemSolution {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {F : Vec d → ℝ} (hF : MemScalarL2 U F) (hC : H1CoerciveEstimate U) : H1MeanZeroFunction U

The mean-zero H¹ weak solution represented by the coercive Hilbert graph solution of the scalar right-hand-side problem.

Equations

• HCPolySupport.H1MeanZeroFunction.scalarRhsProblemSolution hF hC = HCPolySupport.H1CoerciveHilbert.toH1MeanZeroFunction (HCPolySupport.H1CoerciveHilbert.scalarRhsProblemSolution hF hC)

theorem HCPolySupport.H1MeanZeroFunction.scalarRhsProblemSolution_firstVariation {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {F : Vec d → ℝ} (hF : MemScalarL2 U F) (hC : H1CoerciveEstimate U) (u : H1MeanZeroFunction U) : inner ℝ (scalarRhsProblemSolution hF hC).gradToHilbertVectorL2 u.gradToHilbertVectorL2 = inner ℝ (HCPolySupport.toScalarL2 hF) u.toScalarL2

theorem HCPolySupport.H1MeanZeroFunction.scalarRhsProblemSolution_firstVariation_eq_integral {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {F : Vec d → ℝ} (hF : MemScalarL2 U F) (hC : H1CoerciveEstimate U) (u : H1MeanZeroFunction U) : ∫ (x : Vec d) in U, vecDot ((scalarRhsProblemSolution hF hC).toH1Function.grad x) (u.toH1Function.grad x) = ∫ (x : Vec d) in U, F x * u.toH1Function.toFun x

theorem HCPolySupport.H1Function.gradientProblemSolution_firstVariation_eq_integral {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) (u : H1Function U) : ∫ (x : Vec d) in U, vecDot ((H1MeanZeroFunction.gradientProblemSolution hf hC).toH1Function.grad x) (u.grad x) = ∫ (x : Vec d) in U, vecDot (f x) (u.grad x)