HomSpineFrameData #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Theorem B, §4.5: the per-datum frame from the root's own binders #
What this module is #
HomSpineCloseClause's clause body carries eight frame
binders for the Step-3c leg,
hw, hwI, hwc, hGI, hGzero, hgc, hgw, hzero
exactly as the L^∞ conversion carries them. This module produces
the first FIVE of them from the root's own data binders hsol and hcomp, and
DERIVES the eighth (hzero) from the other two. What is left is stated as one
named predicate, HasContinuousRepresentative, and is this file's reported
residue (see the module docstring's last section).
The construction, and why it is the zero extension and not u - v #
The frame items are global statements on Vec d (HasWeakGradientOn Set.univ,
Integrable … volume, HasCompactSupport). The literal difference
u.toFun - v.toFun does NOT satisfy them: an H1Function (openCubeSet Q)
constrains its representative only on Q, so u.toFun - v.toFun is arbitrary
off the cube and is in particular not compactly supported.
The object that does satisfy them is the H¹₀ ZERO EXTENSION — which is
exactly the object the manuscript names ("u - v ∈ H¹₀(□_m)"). hsol and
hcomp carry the SAME boundary datum h, so the
HomSpineCloseUnique.exists_h10Function_sub_of_hasZeroTrace produces w: H10Function (openCubeSet Q) with
∀ x, w x = u.toFun x - v.toFun x and ∀ x, ∇w x = ∇u x - ∇v x,
and CoarseGraining's H10Function.hasWeakGradientOn_univ_zeroExtension turns
the pair (w.zeroExtension, w.zeroExtensionGrad) into a GLOBAL weak-gradient
graph. The two extensions agree with u - v and ∇u - ∇v on the open cube and
vanish off it — which is simultaneously the hGzero binder ("the gradient
vanishes off □_m") and the reason the a.e.-on-□_m conclusion is unchanged.
hzero is DERIVED, not assumed #
faceZero_of_continuousRepresentative: if W vanishes off the open cube and
g is a continuous representative of W, then g vanishes on
cubeFaceSet Q. The complement of the CLOSED cube is open and W vanishes on
it pointwise, so g vanishes there a.e., hence — being continuous, and Lebesgue
measure being open-positive — everywhere on it; g⁻¹{0} is closed and contains
that complement, so it contains its closure, which contains every face point
(cubeFaceSet_subset_closure_compl).
THE RESIDUE (reported, not closed) #
HasContinuousRepresentative W — the existence of a continuous g with W =ᵐ[volume] g. It is NOT derivable from w ∈ H¹₀(□_m) alone (for d ≥ 2 an
H¹₀ function need not have a continuous representative), and it is not
derivable from the root's data binders. Mathematically it comes from the SAME
"fractional Sobolev–Poincaré" step the print invokes in the paper: the negative
gauge on ∇w makes every mollification w ⋆ ψ Hölder-(1-s) at one constant
(the holderSeminormBoundOn_convolution_of_uniformBoxGauge), and a uniformly
Hölder family with L¹ convergence is uniformly Cauchy. That compactness step
is not formalized in this tree.
1. The cube's measure-theoretic frame #
A triadic cube has finite Lebesgue measure: it is bounded and Vec d is a
proper space carrying a measure finite on compacts.
The open realization sits inside the half-open one.
Anything supported in a triadic cube has compact support: the closure of a
bounded set in Vec d is compact.
On a cube, L² control gives L¹ control of the zero extension.
2. The frame of an H¹₀ function #
The value zero extension is integrable.
The value zero extension has compact support.
Every coordinate of the gradient zero extension is integrable.
The gradient zero extension vanishes off the (half-open) cube — the
hGzero binder of the L^∞ conversion.
3. The face geometry, and hzero #
The closed realization of a triadic cube is closed.
Every face point is a limit of exterior points. A point of
cubeFaceSet Q has, in some coordinate, the exact value of a face, so pushing
that one coordinate outwards leaves the closed cube at arbitrarily small
sup-distance.
hzero is DERIVED.
If W vanishes off the open cube and g is a continuous representative of
W, then g vanishes on the faces of the cube. This is the eighth frame
binder of the L^∞ conversion, obtained from the other two
representative binders and the zero extension itself; nothing about the
Dirichlet problem is used.
4. The frame, from the root's own data binders #
The residue. A scalar has a continuous representative if some
continuous function agrees with it a.e. For W = u - v on □_m this is NOT
implied by u - v ∈ H¹₀(□_m); see the module docstring.
Equations
- Algsuperdiff.Section4.Provider.Homogenization.HasContinuousRepresentative W = ∃ (g : HCPolySupport.Vec d → ℝ), Continuous g ∧ W =ᵐ[MeasureTheory.volume] g
Instances For
THE PER-DATUM FRAME.
From the root's own two data binders hsol and hcomp — solutions of the two
Dirichlet problems at the SAME boundary datum h and the SAME forcing g —
the H¹₀ zero extension of u - v and its gradient carry every frame item of
the L^∞ conversion except the continuous representative:
- the two agree with
u - vand∇u - ∇von the open cube; - the value extension vanishes off the open cube;
- the pair is a GLOBAL weak-gradient graph, the value is integrable and compactly supported, each gradient coordinate is integrable;
- the gradient vanishes off the cube (
hGzero).
Nothing beyond hsol.1/hcomp.1 (the zero-trace conjuncts) is consumed.