Coarse-graining support: Support.PDE.HarmonicHilbert

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

Hilbert realization of A-harmonic gradients

This file starts the Stage 6 bridge from the response-maximizer direct method to the concrete AHarmonicFunction API. The closed Hilbert subspace below models gradients F such that F ∈ Lpot(U) and a F ∈ Lsol(U).

noncomputable def HCPolySupport.AHarmonicGradientHilbert.closedSubmodule {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : ClosedSubmodule ℝ ↥(HilbertVectorL2 U)

The closed Hilbert subspace of vector L² fields whose plain representative lies in the packaged potential space and whose coefficient-weighted representative lies in the packaged solenoidal space.

Equations

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

@[reducible, inline]

noncomputable abbrev HCPolySupport.AHarmonicGradientHilbert.Space {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : Submodule ℝ ↥(HilbertVectorL2 U)

The Hilbert carrier for A-harmonic gradients.

Equations

• HCPolySupport.AHarmonicGradientHilbert.Space M hEll = ↑(HCPolySupport.AHarmonicGradientHilbert.closedSubmodule M hEll)

@[instance_reducible]

noncomputable instance HCPolySupport.AHarmonicGradientHilbert.instSeminormedAddCommGroup {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : SeminormedAddCommGroup ↥(Space M hEll)

Equations

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

@[instance_reducible]

noncomputable instance HCPolySupport.AHarmonicGradientHilbert.instNormedAddCommGroup {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : NormedAddCommGroup ↥(Space M hEll)

Equations

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

@[instance_reducible]

noncomputable instance HCPolySupport.AHarmonicGradientHilbert.instNormedSpace {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : NormedSpace ℝ ↥(Space M hEll)

Equations

• HCPolySupport.AHarmonicGradientHilbert.instNormedSpace M hEll = { toModule := (HCPolySupport.AHarmonicGradientHilbert.Space M hEll).module, norm_smul_le := ⋯ }

@[instance_reducible]

noncomputable instance HCPolySupport.AHarmonicGradientHilbert.instInnerProductSpace {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : InnerProductSpace ℝ ↥(Space M hEll)

Equations

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

instance HCPolySupport.AHarmonicGradientHilbert.instCompleteSpace {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : CompleteSpace ↥(Space M hEll)

@[reducible, inline]

abbrev HCPolySupport.AHarmonicGradientHilbert.field {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : ↥(HilbertVectorL2 U)

The ambient Hilbert-vector L² field represented by a harmonic-gradient Hilbert element.

Equations

• HCPolySupport.AHarmonicGradientHilbert.field z = ↑z

@[reducible, inline]

noncomputable abbrev HCPolySupport.AHarmonicGradientHilbert.vectorField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : ↥(VectorL2 U)

The plain vector-valued L² representative of a harmonic-gradient Hilbert element.

Equations

• HCPolySupport.AHarmonicGradientHilbert.vectorField z = HCPolySupport.hilbertVectorL2ToVectorL2 (HCPolySupport.AHarmonicGradientHilbert.field z)

@[reducible, inline]

noncomputable abbrev HCPolySupport.AHarmonicGradientHilbert.coeffField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : ↥(HilbertVectorL2 U)

The coefficient-weighted Hilbert-vector L² field associated to a harmonic-gradient Hilbert element.

Equations

• HCPolySupport.AHarmonicGradientHilbert.coeffField z = (HCPolySupport.hilbertCoeffOperator hEll) (HCPolySupport.AHarmonicGradientHilbert.field z)

@[reducible, inline]

noncomputable abbrev HCPolySupport.AHarmonicGradientHilbert.coeffVectorField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : ↥(VectorL2 U)

The plain vector-valued representative of the coefficient-weighted field.

Equations

• HCPolySupport.AHarmonicGradientHilbert.coeffVectorField z = HCPolySupport.hilbertVectorL2ToVectorL2 (HCPolySupport.AHarmonicGradientHilbert.coeffField z)

theorem HCPolySupport.AHarmonicGradientHilbert.mem_potential {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : vectorField z ∈ M.potential

theorem HCPolySupport.AHarmonicGradientHilbert.mem_solenoidal {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : coeffVectorField z ∈ M.solenoidal

noncomputable def HCPolySupport.AHarmonicGradientHilbert.ofAHarmonicFunction {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) (u : AHarmonicFunction a U) : ↥(Space M hEll)

A concrete A-harmonic function determines an element of the closed Hilbert realization of A-harmonic gradients.

Equations

• HCPolySupport.AHarmonicGradientHilbert.ofAHarmonicFunction M hEll u = ⟨u.toH1.gradToHilbertVectorL2, ⋯⟩

@[simp]

theorem HCPolySupport.AHarmonicGradientHilbert.field_ofAHarmonicFunction {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) (u : AHarmonicFunction a U) : field (ofAHarmonicFunction M hEll u) = u.toH1.gradToHilbertVectorL2

@[simp]

theorem HCPolySupport.AHarmonicGradientHilbert.vectorField_ofAHarmonicFunction {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) (u : AHarmonicFunction a U) : vectorField (ofAHarmonicFunction M hEll u) = u.toH1.gradToVectorL2

noncomputable def HCPolySupport.AHarmonicGradientHilbert.fieldCLM {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : ↥(Space M hEll) →L[ℝ] ↥(HilbertVectorL2 U)

The inclusion of the closed harmonic-gradient space into ambient Hilbert-vector L².

Equations

• HCPolySupport.AHarmonicGradientHilbert.fieldCLM M hEll = (↑(HCPolySupport.AHarmonicGradientHilbert.closedSubmodule M hEll)).subtypeL

@[simp]

theorem HCPolySupport.AHarmonicGradientHilbert.fieldCLM_apply {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) (z : ↥(Space M hEll)) : (fieldCLM M hEll) z = field z

theorem HCPolySupport.AHarmonicGradientHilbert.field_eq_toHilbertVectorL2OfVecField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : field z = toHilbertVectorL2OfVecField ⋯

@[reducible, inline]

noncomputable abbrev HCPolySupport.AHarmonicGradientHilbert.symmCoeffField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : ↥(HilbertVectorL2 U)

The symmetric coefficient-weighted field associated to a harmonic-gradient Hilbert element.

Equations

• HCPolySupport.AHarmonicGradientHilbert.symmCoeffField z = (HCPolySupport.hilbertSymmCoeffOperator hEll) (HCPolySupport.AHarmonicGradientHilbert.field z)

noncomputable def HCPolySupport.AHarmonicGradientHilbert.symmCoeffFieldCLM {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : ↥(Space M hEll) →L[ℝ] ↥(HilbertVectorL2 U)

The continuous symmetric-coefficient field map on the closed harmonic-gradient space.

Equations

• HCPolySupport.AHarmonicGradientHilbert.symmCoeffFieldCLM M hEll = HCPolySupport.hilbertSymmCoeffOperator hEll ∘SL HCPolySupport.AHarmonicGradientHilbert.fieldCLM M hEll

noncomputable def HCPolySupport.AHarmonicGradientHilbert.symmCoeffBilin {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (M : PotentialSolenoidalL2Data U) (hEll : IsEllipticFieldOn lam Lam U a) : ↥(Space M hEll) →L[ℝ] ↥(Space M hEll) →L[ℝ] ℝ

The symmetric energy bilinear form on the closed A-harmonic-gradient Hilbert space.

Equations

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

@[simp]

theorem HCPolySupport.AHarmonicGradientHilbert.symmCoeffBilin_apply {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z w : ↥(Space M hEll)) : ((symmCoeffBilin M hEll) z) w = inner ℝ ((hilbertSymmCoeffOperator hEll) (field z)) (field w)

theorem HCPolySupport.AHarmonicGradientHilbert.symmCoeffBilin_apply_eq_integral {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z w : ↥(Space M hEll)) : ((symmCoeffBilin M hEll) z) w = ∫ (x : Vec d) in U, vecDot (matVecMul (symmPart (a x)) (↑↑(vectorField z) x)) (↑↑(vectorField w) x)

theorem HCPolySupport.AHarmonicGradientHilbert.symmCoeffBilin_apply_eq_integral_comm {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z w : ↥(Space M hEll)) : ((symmCoeffBilin M hEll) z) w = ∫ (x : Vec d) in U, vecDot (↑↑(vectorField w) x) (matVecMul (symmPart (a x)) (↑↑(vectorField z) x))

theorem HCPolySupport.AHarmonicGradientHilbert.symmCoeffBilin_symm {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z w : ↥(Space M hEll)) : ((symmCoeffBilin M hEll) z) w = ((symmCoeffBilin M hEll) w) z

theorem HCPolySupport.AHarmonicGradientHilbert.symmCoeffBilin_self_ge_lam_mul_norm_sq {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : lam * ‖z‖ ^ 2 ≤ ((symmCoeffBilin M hEll) z) z

theorem HCPolySupport.AHarmonicGradientHilbert.isCoercive_symmCoeffBilin {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : IsCoercive (symmCoeffBilin M hEll)

noncomputable def HCPolySupport.AHarmonicGradientHilbert.vectorPairingCLM {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : MemVectorL2 U g) : ↥(VectorL2 U) →L[ℝ] ℝ

The continuous linear functional on vector L² fields given by the integral of their dot product with g over U.

Equations

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

theorem HCPolySupport.AHarmonicGradientHilbert.vectorPairingCLM_apply_eq_integral {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : MemVectorL2 U g) (F : ↥(VectorL2 U)) : (vectorPairingCLM hg) F = ∫ (x : Vec d) in U, vecDot (g x) (↑↑F x)

theorem HCPolySupport.AHarmonicGradientHilbert.integral_vecDot_eq_zero_of_mem_potential_closure {d : ℕ} {U : Set (Vec d)} (F : ↥(VectorL2 U)) (hF : F ∈ (PotentialSolenoidalL2Data.ofSubmoduleClosures U).potential) {g : Vec d → Vec d} (hg : MemVectorL2 U g) (hsol : IsSolenoidalZeroNormalTraceOn U g) : ∫ (x : Vec d) in U, vecDot (g x) (↑↑F x) = 0

theorem HCPolySupport.AHarmonicGradientHilbert.integral_vecDot_eq_zero_of_mem_solenoidal_closure {d : ℕ} {U : Set (Vec d)} (G : ↥(VectorL2 U)) (hG : G ∈ (PotentialSolenoidalL2Data.ofSubmoduleClosures U).solenoidal) (φ : H10Function U) : ∫ (x : Vec d) in U, vecDot (↑↑G x) (φ.grad x) = 0

theorem HCPolySupport.AHarmonicGradientHilbert.isPotentialOn_vectorField_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {hEll : IsEllipticFieldOn lam Lam U a} (hHodge : HodgeConverseCriterion U) (z : ↥(Space (PotentialSolenoidalL2Data.ofSubmoduleClosures U) hEll)) : IsPotentialOn U ↑↑(vectorField z)

theorem HCPolySupport.AHarmonicGradientHilbert.isSolenoidalOn_coeffVectorField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space (PotentialSolenoidalL2Data.ofSubmoduleClosures U) hEll)) : IsSolenoidalOn U ↑↑(coeffVectorField z)

theorem HCPolySupport.AHarmonicGradientHilbert.ae_coeffVectorField_eq_matVecMul_vectorField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {M : PotentialSolenoidalL2Data U} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space M hEll)) : ↑↑(coeffVectorField z) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => matVecMul (a x) (↑↑(vectorField z) x)

theorem HCPolySupport.AHarmonicGradientHilbert.isSolenoidalOn_matVecMul_vectorField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {hEll : IsEllipticFieldOn lam Lam U a} (z : ↥(Space (PotentialSolenoidalL2Data.ofSubmoduleClosures U) hEll)) : IsSolenoidalOn U fun (x : Vec d) => matVecMul (a x) (↑↑(vectorField z) x)

theorem HCPolySupport.AHarmonicGradientHilbert.isAHarmonicGradient_vectorField_of_hodgeConverseCriterion {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {hEll : IsEllipticFieldOn lam Lam U a} (hHodge : HodgeConverseCriterion U) (z : ↥(Space (PotentialSolenoidalL2Data.ofSubmoduleClosures U) hEll)) : IsAHarmonicGradient a U ↑↑(vectorField z)

noncomputable def HCPolySupport.AHarmonicGradientHilbert.toAHarmonicFunction {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {hEll : IsEllipticFieldOn lam Lam U a} (hHodge : HodgeConverseCriterion U) (z : ↥(Space (PotentialSolenoidalL2Data.ofSubmoduleClosures U) hEll)) : AHarmonicFunction a U

Recover a concrete AHarmonicFunction from a Hilbert element in the closed A-harmonic gradient space, using the Hodge converse to recover the potential representative.

Equations

• HCPolySupport.AHarmonicGradientHilbert.toAHarmonicFunction hHodge z = { toH1 := Classical.choose ⋯, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicGradientHilbert.grad_toAHarmonicFunction {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {hEll : IsEllipticFieldOn lam Lam U a} (hHodge : HodgeConverseCriterion U) (z : ↥(Space (PotentialSolenoidalL2Data.ofSubmoduleClosures U) hEll)) : (toAHarmonicFunction ⋯ z).toH1.grad = ↑↑(vectorField z)