DirichletClosure #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: zero-trace potential representatives on triadic cubes #
PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization U
= ∀ F : VectorL2 U, F ∈ (ofSubmoduleClosures U).potentialZeroTrace →
IsPotentialZeroTraceOn U F
is the statement that the closure used to build the canonical zero-trace
potential subspace adds no abstract elements, so that every closed L²
zero-trace potential class really is the gradient of an H¹₀ function.
It does, and the two ingredients are both already in CoarseGraining:
hasPotentialZeroTraceClosureRealization_of_isOpenBoundedConvexDomain
(Homogenization/Sobolev/PotentialSolenoidalL2Realization.lean), proved from
the closed-range gradient projection on the H¹₀ graph; and
This file records the composition and the unconditional Dirichlet existence it
yields on cu_K, which is what the corrector-limit nodes B3/B7 consume.
Note that HasPotentialZeroTraceClosureRealization is stated for the open
cube; the half-open realization cubeSet Q carries the same restricted
Lebesgue measure
(Homogenization.volume_restrict_cubeSet_eq_volume_restrict_openCubeSet) but a
syntactically different VectorL2 carrier, and CoarseGraining transports
solutions across the two realizations separately.
An open triadic cube is nonempty: its centre lies in it.
Decision D-2, resolved affirmatively. Every open triadic cube satisfies CoarseGraining's zero-trace potential closure realization hypothesis, so no separate obligation has to be carried through the corrector-limit development.
Unconditional existence of a zero-trace Dirichlet weak solution of
-div (a ∇v) = div g on an open triadic cube. With a the identity
coefficient field and g := -f this is the cube problem w_D^{(K)} of
ABK26.