Coarse-graining support: Support.Sobolev.PotentialSolenoidalL2

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

This file packages the note's spaces \Lpot(U), \Lpoto(U), \Lsol(U), \Lsolo(U) and their doubled block versions as actual closed subspaces of the ambient L² spaces.

The structures remain abstract so downstream arguments can still be phrased in terms of packaged closed subspaces. This file also provides canonical constructors obtained by taking closures of the predicate-generated Sobolev submodules that already exist in the current development.

def HCPolySupport.blockField {d : ℕ} (f g : Vec d → Vec d) : Vec d → BlockVec d

Combine two vector fields into one block-valued field.

Equations

• HCPolySupport.blockField f g x = (f x, g x)

@[simp]

theorem HCPolySupport.blockField_fst {d : ℕ} (f g : Vec d → Vec d) (x : Vec d) : (blockField f g x).1 = f x

@[simp]

theorem HCPolySupport.blockField_snd {d : ℕ} (f g : Vec d → Vec d) (x : Vec d) : (blockField f g x).2 = g x

theorem HCPolySupport.memBlockL2_blockField {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : MemBlockL2 U (blockField f g)

noncomputable def HCPolySupport.toBlockL2OfComponents {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : ↥(BlockL2 U)

Promote a pair of vector L² witnesses to the block-valued ambient type.

Equations

• HCPolySupport.toBlockL2OfComponents hf hg = HCPolySupport.toBlockL2 ⋯

theorem HCPolySupport.coeFn_toBlockL2OfComponents {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : ↑↑(toBlockL2OfComponents hf hg) =ᵐ[volumeMeasureOn U] blockField f g

def HCPolySupport.hilbertBlockField {d : ℕ} (f g : Vec d → Vec d) : Vec d → HilbertBlockVec d

Combine two vector fields into one Hilbert block-valued field.

Equations

• HCPolySupport.hilbertBlockField f g = HCPolySupport.hilbertifyBlockField (HCPolySupport.blockField f g)

theorem HCPolySupport.memHilbertBlockL2_blockField {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : MemHilbertBlockL2 U (hilbertBlockField f g)

noncomputable def HCPolySupport.toHilbertBlockL2OfComponents {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : ↥(HilbertBlockL2 U)

Promote a pair of vector L² witnesses to the Hilbert block-valued ambient type.

Equations

• HCPolySupport.toHilbertBlockL2OfComponents hf hg = HCPolySupport.toHilbertBlockL2 ⋯

theorem HCPolySupport.coeFn_toHilbertBlockL2OfComponents {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : ↑↑(toHilbertBlockL2OfComponents hf hg) =ᵐ[volumeMeasureOn U] hilbertBlockField f g

theorem HCPolySupport.memScalarL2_coord_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (i : Fin d) : MemScalarL2 U fun (x : Vec d) => f x i

theorem HCPolySupport.integrableOn_vecDot_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (f x) (g x)) U MeasureTheory.volume

theorem HCPolySupport.IsSolenoidalZeroNormalTraceOn.isSolenoidalOn {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn U g) : IsSolenoidalOn U g

theorem HCPolySupport.isSolenoidalOn_add_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf_mem : MemVectorL2 U f) (hg_mem : MemVectorL2 U g) (hf : IsSolenoidalOn U f) (hg : IsSolenoidalOn U g) : IsSolenoidalOn U (f + g)

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_add_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf_mem : MemVectorL2 U f) (hg_mem : MemVectorL2 U g) (hf : IsSolenoidalZeroNormalTraceOn U f) (hg : IsSolenoidalZeroNormalTraceOn U g) : IsSolenoidalZeroNormalTraceOn U (f + g)

theorem HCPolySupport.IsSolenoidalOn.const_isSolenoidalOn_of_isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (q : Vec d) : IsSolenoidalOn U fun (x : Vec d) => q

Constant vector fields are solenoidal against H¹₀ tests on Sobolev-regular domains.

theorem HCPolySupport.toBlockL2OfComponents_add {d : ℕ} {U : Set (Vec d)} {f1 f2 g1 g2 : Vec d → Vec d} (hf1 : MemVectorL2 U f1) (hg1 : MemVectorL2 U g1) (hf2 : MemVectorL2 U f2) (hg2 : MemVectorL2 U g2) : toBlockL2OfComponents ⋯ ⋯ = toBlockL2OfComponents hf1 hg1 + toBlockL2OfComponents hf2 hg2

theorem HCPolySupport.toBlockL2OfComponents_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : toBlockL2OfComponents ⋯ ⋯ = c • toBlockL2OfComponents hf hg

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

Packaged L² data for the note's potential and solenoidal spaces.

The four vector-valued closed subspaces model Lpot(U), Lpoto(U), Lsol(U), Lsolo(U), while the two block-valued closed subspaces model Lpot(U) × Lsol(U) and Lpoto(U) × Lsolo(U).

• potential : ClosedSubmodule ℝ ↥(VectorL2 U)

  The closed L² subspace modeling \Lpot(U).

• potentialZeroTrace : ClosedSubmodule ℝ ↥(VectorL2 U)

  The closed L² subspace modeling \Lpoto(U).

• solenoidal : ClosedSubmodule ℝ ↥(VectorL2 U)

  The closed L² subspace modeling \Lsol(U).

• solenoidalZeroNormalTrace : ClosedSubmodule ℝ ↥(VectorL2 U)

  The closed L² subspace modeling \Lsolo(U).

• blockPotentialSolenoidal : ClosedSubmodule ℝ ↥(BlockL2 U)

  The closed block subspace modeling \Lpot(U) × \Lsol(U).

• blockPotentialZeroTraceSolenoidalZeroNormalTrace : ClosedSubmodule ℝ ↥(BlockL2 U)

  The closed block subspace modeling \Lpoto(U) × \Lsolo(U).

• mem_potential {f : Vec d → Vec d} (hf : MemVectorL2 U f) : IsPotentialOn U f → toVectorL2 hf ∈ self.potential

  Predicate-level potentials land in the packaged L² subspace.

• mem_potentialZeroTrace {f : Vec d → Vec d} (hf : MemVectorL2 U f) : IsPotentialZeroTraceOn U f → toVectorL2 hf ∈ self.potentialZeroTrace

  Predicate-level zero-trace potentials land in the packaged L² subspace.

• mem_solenoidal {g : Vec d → Vec d} (hg : MemVectorL2 U g) : IsSolenoidalOn U g → toVectorL2 hg ∈ self.solenoidal

  Predicate-level solenoidal fields land in the packaged L² subspace.

• mem_solenoidalZeroNormalTrace {g : Vec d → Vec d} (hg : MemVectorL2 U g) : IsSolenoidalZeroNormalTraceOn U g → toVectorL2 hg ∈ self.solenoidalZeroNormalTrace

  Predicate-level zero-normal-trace solenoidal fields land in the packaged L² subspace.

• mem_blockPotentialSolenoidal {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : IsPotentialOn U f → IsSolenoidalOn U g → toBlockL2OfComponents hf hg ∈ self.blockPotentialSolenoidal

  Predicate-level block fields in \Lpot(U) × \Lsol(U) land in the packaged block L² subspace.

• mem_blockPotentialZeroTraceSolenoidalZeroNormalTrace {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : IsPotentialZeroTraceOn U f → IsSolenoidalZeroNormalTraceOn U g → toBlockL2OfComponents hf hg ∈ self.blockPotentialZeroTraceSolenoidalZeroNormalTrace

  Predicate-level block fields in \Lpoto(U) × \Lsolo(U) land in the packaged block L² subspace.

• potentialZeroTrace_le_potential : self.potentialZeroTrace ≤ self.potential

  The note's inclusion \Lpoto(U) ⊆ \Lpot(U).

• solenoidalZeroNormalTrace_le_solenoidal : self.solenoidalZeroNormalTrace ≤ self.solenoidal

  The note's inclusion \Lsolo(U) ⊆ \Lsol(U).

• blockPotentialZeroTraceSolenoidalZeroNormalTrace_le_blockPotentialSolenoidal : self.blockPotentialZeroTraceSolenoidalZeroNormalTrace ≤ self.blockPotentialSolenoidal

  The block-level inclusion \Lpoto(U) × \Lsolo(U) ⊆ \Lpot(U) × \Lsol(U).

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

Black-box Hilbert-valued L² packaging of the correction space \mathcal H(U) = \Lpoto(U) × \Lsolo(U) used in the doubled \mu problem.

This is the exact closed subspace that later sits inside the ambient Hilbert space L²(U; \R^{2d}).

• correctionSpace : ClosedSubmodule ℝ ↥(HilbertBlockL2 U)

  The closed Hilbert subspace modeling \Lpoto(U) × \Lsolo(U).

• mem_correctionSpace {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : IsPotentialZeroTraceOn U f → IsSolenoidalZeroNormalTraceOn U g → toHilbertBlockL2OfComponents hf hg ∈ self.correctionSpace

  Predicate-level correction pairs land in the packaged Hilbert subspace.

def HCPolySupport.PotentialSolenoidalL2Data.potentialSubmodule {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(VectorL2 U)

Predicate-generated L² submodule for \Lpot(U).

Equations

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

def HCPolySupport.PotentialSolenoidalL2Data.potentialZeroTraceSubmodule {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(VectorL2 U)

Predicate-generated L² submodule for \Lpoto(U).

Equations

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

def HCPolySupport.PotentialSolenoidalL2Data.solenoidalSubmodule {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(VectorL2 U)

Predicate-generated L² submodule for \Lsol(U).

Equations

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

def HCPolySupport.PotentialSolenoidalL2Data.solenoidalZeroNormalTraceSubmodule {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(VectorL2 U)

Predicate-generated L² submodule for \Lsolo(U).

Equations

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

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.gradientPairingVectorL2CLM {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ↥(VectorL2 U) →L[ℝ] ℝ

The continuous linear functional pairing a vector L² class with the weak gradient of u by integration over U.

Equations

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

theorem HCPolySupport.PotentialSolenoidalL2Data.isSolenoidalOn_of_mem_closure_solenoidalSubmodule {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : MemVectorL2 U g) (hmem : toVectorL2 hg ∈ (solenoidalSubmodule U).closure) : IsSolenoidalOn U g

theorem HCPolySupport.PotentialSolenoidalL2Data.isSolenoidalZeroNormalTraceOn_of_mem_closure_solenoidalZeroNormalTraceSubmodule {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : MemVectorL2 U g) (hmem : toVectorL2 hg ∈ (solenoidalZeroNormalTraceSubmodule U).closure) : IsSolenoidalZeroNormalTraceOn U g

def HCPolySupport.PotentialSolenoidalL2Data.blockPotentialSolenoidalSubmodule {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(BlockL2 U)

Predicate-generated block L² submodule for \Lpot(U) × \Lsol(U).

Equations

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

def HCPolySupport.PotentialSolenoidalL2Data.blockPotentialZeroTraceSolenoidalZeroNormalTraceSubmodule {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(BlockL2 U)

Predicate-generated block L² submodule for \Lpoto(U) × \Lsolo(U).

Equations

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

theorem HCPolySupport.PotentialSolenoidalL2Data.potentialZeroTraceSubmodule_le_potentialSubmodule {d : ℕ} {U : Set (Vec d)} : potentialZeroTraceSubmodule U ≤ potentialSubmodule U

theorem HCPolySupport.PotentialSolenoidalL2Data.solenoidalZeroNormalTraceSubmodule_le_solenoidalSubmodule {d : ℕ} {U : Set (Vec d)} : solenoidalZeroNormalTraceSubmodule U ≤ solenoidalSubmodule U

theorem HCPolySupport.PotentialSolenoidalL2Data.blockPotentialZeroTraceSolenoidal_le_blockPotentialSolenoidal {d : ℕ} {U : Set (Vec d)} : blockPotentialZeroTraceSolenoidalZeroNormalTraceSubmodule U ≤ blockPotentialSolenoidalSubmodule U

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.ofSubmoduleClosures {d : ℕ} (U : Set (Vec d)) : PotentialSolenoidalL2Data U

Canonical packaged L² data obtained by closing the predicate-generated Sobolev submodules.

Equations

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

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.ofIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (_hU : IsSobolevRegularDomain U) : PotentialSolenoidalL2Data U

Canonical packaged L² data attached to a Sobolev-regular domain.

The current implementation is obtained by closing the predicate-generated Sobolev submodules; the domain regularity hypothesis gives downstream files a stable constructor surface to consume.

Equations

• HCPolySupport.PotentialSolenoidalL2Data.ofIsSobolevRegularDomain _hU = HCPolySupport.PotentialSolenoidalL2Data.ofSubmoduleClosures U

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.ofIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : PotentialSolenoidalL2Data U

Canonical packaged L² data attached to a bounded open convex domain.

Equations

• HCPolySupport.PotentialSolenoidalL2Data.ofIsOpenBoundedConvexDomain hU = HCPolySupport.PotentialSolenoidalL2Data.ofIsSobolevRegularDomain ⋯

def HCPolySupport.PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization {d : ℕ} (U : Set (Vec d)) : Prop

Honest closed-range/realization hypothesis for the canonical zero-trace potential space. This says that the closure used in ofSubmoduleClosures has no extra abstract elements: every closed L² zero-trace potential class is represented by the gradient of an actual H¹₀ function.

Equations

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

theorem HCPolySupport.PotentialSolenoidalL2Data.isPotentialZeroTraceOn_of_mem_potentialZeroTrace_ofSubmoduleClosures {d : ℕ} {U : Set (Vec d)} (hRealize : HasPotentialZeroTraceClosureRealization U) (F : ↥(VectorL2 U)) (hF : F ∈ (ofSubmoduleClosures U).potentialZeroTrace) : IsPotentialZeroTraceOn U ↑↑F

Apply the closed-range/realization hypothesis for the canonical zero-trace potential subspace.

theorem HCPolySupport.PotentialSolenoidalL2Data.isSolenoidalOn_of_mem_solenoidal_ofSubmoduleClosures {d : ℕ} {U : Set (Vec d)} (G : ↥(VectorL2 U)) (hG : G ∈ (ofSubmoduleClosures U).solenoidal) : IsSolenoidalOn U ↑↑G

Membership in the canonical closed solenoidal subspace recovers the weak solenoidal predicate on the represented vector field.

theorem HCPolySupport.PotentialSolenoidalL2Data.isSolenoidalZeroNormalTraceOn_of_mem_closures {d : ℕ} {U : Set (Vec d)} (G : ↥(VectorL2 U)) (hG : G ∈ (ofSubmoduleClosures U).solenoidalZeroNormalTrace) : IsSolenoidalZeroNormalTraceOn U ↑↑G

Membership in the canonical closed zero-normal-trace solenoidal subspace recovers the corresponding weak predicate on the represented vector field.

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.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.

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.oneScalarL2Local {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ↥(ScalarL2 U)

The scalar L² class of the constant function one on U.

Equations

• HCPolySupport.PotentialSolenoidalL2Data.oneScalarL2Local = HCPolySupport.toScalarL2 ⋯

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

The continuous linear functional integrating a scalar L² class over U.

Equations

• HCPolySupport.PotentialSolenoidalL2Data.scalarIntegralCLMLocal = (InnerProductSpace.toDual ℝ ↥(HCPolySupport.ScalarL2 U)) HCPolySupport.PotentialSolenoidalL2Data.oneScalarL2Local

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

Members of the canonical closed zero-trace potential subspace are orthogonal to every zero-normal-trace solenoidal test field.

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.coordIntegralCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (i : Fin d) : ↥(VectorL2 U) →L[ℝ] ℝ

The continuous linear functional integrating coordinate i of a vector L² class over U.

Equations

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

theorem HCPolySupport.PotentialSolenoidalL2Data.integral_coord_eq_zero_of_mem_potentialZeroTrace_ofSubmoduleClosures {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (F : ↥(VectorL2 U)) (hF : F ∈ (ofSubmoduleClosures U).potentialZeroTrace) (i : Fin d) : ∫ (x : Vec d) in U, ↑↑F x i = 0

Members of the canonical closed zero-trace potential subspace have componentwise zero averages.

theorem HCPolySupport.PotentialSolenoidalL2Data.hilbertBlockL2ToBlockL2_toHilbertBlockL2OfComponents {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : hilbertBlockL2ToBlockL2 (toHilbertBlockL2OfComponents hf hg) = toBlockL2OfComponents hf hg

Specialization of the ambient carrier transport to block fields built from two vector components.

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.toMuCorrectionSpaceData {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : MuCorrectionSpaceData U

Transport the packaged block correction space \Lpoto(U) × \Lsolo(U) ⊆ BlockL²(U) into the Hilbert-block ambient space used by the doubled μ problem.

Equations

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

@[simp]

theorem HCPolySupport.PotentialSolenoidalL2Data.mem_toMuCorrectionSpaceData_iff {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) (X : ↥(HilbertBlockL2 U)) : X ∈ M.toMuCorrectionSpaceData.correctionSpace ↔ hilbertBlockL2ToBlockL2 X ∈ M.blockPotentialZeroTraceSolenoidalZeroNormalTrace

noncomputable def HCPolySupport.MuCorrectionSpaceData.ofSubmoduleClosures {d : ℕ} (U : Set (Vec d)) : MuCorrectionSpaceData U

Canonical Hilbert correction-space packaging obtained from the closed predicate-generated Sobolev block submodule.

Equations

• HCPolySupport.MuCorrectionSpaceData.ofSubmoduleClosures U = (HCPolySupport.PotentialSolenoidalL2Data.ofSubmoduleClosures U).toMuCorrectionSpaceData

noncomputable def HCPolySupport.MuCorrectionSpaceData.ofIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) : MuCorrectionSpaceData U

Canonical Hilbert correction-space packaging attached to a Sobolev-regular domain.

Equations

• HCPolySupport.MuCorrectionSpaceData.ofIsSobolevRegularDomain hU = (HCPolySupport.PotentialSolenoidalL2Data.ofIsSobolevRegularDomain hU).toMuCorrectionSpaceData

noncomputable def HCPolySupport.MuCorrectionSpaceData.ofIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : MuCorrectionSpaceData U

Canonical Hilbert correction-space packaging attached to a bounded open convex domain.

Equations

• HCPolySupport.MuCorrectionSpaceData.ofIsOpenBoundedConvexDomain hU = (HCPolySupport.PotentialSolenoidalL2Data.ofIsOpenBoundedConvexDomain hU).toMuCorrectionSpaceData

noncomputable def HCPolySupport.potentialSolenoidalL2DataOfSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) : PotentialSolenoidalL2Data U

Canonical packaged L² potential/solenoidal data on a Sobolev-regular domain.

Equations

• HCPolySupport.potentialSolenoidalL2DataOfSobolevRegularDomain hU = HCPolySupport.PotentialSolenoidalL2Data.ofIsSobolevRegularDomain hU

noncomputable def HCPolySupport.muCorrectionSpaceDataOfSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) : MuCorrectionSpaceData U

Canonical packaged Hilbert correction space on a Sobolev-regular domain.

Equations

• HCPolySupport.muCorrectionSpaceDataOfSobolevRegularDomain hU = HCPolySupport.MuCorrectionSpaceData.ofIsSobolevRegularDomain hU

noncomputable def HCPolySupport.potentialSolenoidalL2DataOfOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : PotentialSolenoidalL2Data U

Canonical packaged L² potential/solenoidal data on a bounded open convex domain.

Equations

• HCPolySupport.potentialSolenoidalL2DataOfOpenBoundedConvexDomain hU = HCPolySupport.PotentialSolenoidalL2Data.ofIsOpenBoundedConvexDomain hU

noncomputable def HCPolySupport.muCorrectionSpaceDataOfOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : MuCorrectionSpaceData U

Canonical packaged Hilbert correction space on a bounded open convex domain.

Equations

• HCPolySupport.muCorrectionSpaceDataOfOpenBoundedConvexDomain hU = HCPolySupport.MuCorrectionSpaceData.ofIsOpenBoundedConvexDomain hU