AntisymmetricShift #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The constant antisymmetric shift: the skew-divergence primitive #
since ã_{L,n+2} and a_L differ by a constant anti-symmetric matrix,
-∇·ã_{L,n+2}∇u = -∇·a_L∇u = ∇·g in □_m .
The manuscript states the underlying invariance in prose only (: "the addition
of a constant antisymmetric matrix to the coefficient field has no effect on
the generator ∇·a(x)∇") and never writes its argument; the graph records this
as the step's whole content. This module supplies the missing argument as a
genuine theorem.
The mathematics #
For a constant matrix C and u ∈ H¹(U), φ ∈ H¹₀(U) put
T i j := ∫_U ∂_j u · ∂_i φ .
T is symmetric: with φ smooth and compactly supported in U, the
coordinate derivative ∂_i φ is again such a test function, so the weak
derivative of u in the direction j may be tested against it, giving
T i j = -∫_U u · ∂_j ∂_i φ; the right-hand side is symmetric in (i, j)
because the second derivative of a smooth function is. A skew C therefore
pairs to zero against T, i.e.
∫_U (C ∇u) · ∇φ = 0 ,
first for smooth φ and then, by the H¹₀ approximation package (the pairing
is L²-continuous in ∇φ because C ∇u ∈ L²(U)), for every φ ∈ H¹₀(U).
Subtracting C from a coefficient field consequently changes neither side of
the divergence-form weak equation.
This is the "skew-divergence integration by parts" primitive: CoarseGraining
has no such statement (swept: Homogenization/Sobolev/**,
Homogenization/Book/** for skew/antisym — only skewPart algebra and
le_antisymm), so it is proved here at Support grade, on an arbitrary set
U (no cube, no ellipticity, no finite measure).
No integrability hypothesis (and why none is needed) #
Splitting ∫ (a − C)∇u·∇φ into ∫ a∇u·∇φ − ∫ C∇u·∇φ would ordinarily need
a∇u ∈ L¹, which the weak-equation predicate does not supply. It is not
needed: the subtracted integral is zero, and Bochner integration assigns 0
to non-integrable functions, so the two cases (a∇u·∇φ integrable or not) both
close — see integral_sub_of_integrable_of_integral_eq_zero. Hence every
statement here is unconditional in the coefficient field.
Main results #
integral_vecDot_matVecMul_skew_h10— the primitive:∫_U (C∇u)·∇φ = 0for skew constantC,u ∈ H¹(U),φ ∈ H¹₀(U).integral_vecDot_matVecMul_sub_const_eq_of_skew— the tex display's first equality-∇·(a − C)∇u = -∇·a∇u, as an identity of weak operators.isDivFormWeakSolutionOn_sub_const_of_skew(and_iff,_add_const_of_skew) — the weak equation is invariant undera ↦ a − C.isDirichletSolutionOn_sub_const_of_skew— the same for the §4.3 Dirichlet carrier (the boundary clause sees onlyu − h, so it is untouched).IsWeaklyHarmonicOnis not touched: the harmonic comparison of the lemma is at the constant-coefficient Laplacian, where no shift occurs.
References #
- ABK26,
l.harmonic.approximation.good.scales. - ABK26, (the prose statement of the invariance), (the skew stream matrix).
- CoarseGraining,
Homogenization/Sobolev/Foundations/EuclideanL2.lean(euclideanCoordSecondDeriv_comm),Homogenization/Sobolev/WeakDerivatives.lean(HasWeakPartialDerivOn),Homogenization/Sobolev/Foundations/CubeNeumannW22/WeakInteriorDQ/SmoothLimit.lean(tendsto_integral_mul_of_tendsto_toScalarL2).
1. Two elementary reductions #
2. The bilinear array of an H¹ gradient against a smooth test #
3. The skew pairing, first at smooth tests #
4. The primitive: the skew pairing against every H¹₀ test #
The skew-divergence integration by parts on an arbitrary set.
For a constant skew matrix C, every u ∈ H¹(U) and every φ ∈ H¹₀(U),
∫_U (C ∇u) · ∇φ = 0 .
This is the primitive for invariance under a constant skew coefficient shift.
5. Invariance of the weak equation #
-∇·(a − C)∇u = -∇·a∇u for constant skew C — the literal first
equality of the printed display, as an identity of the two weak operators tested
against H¹₀(U). Nothing is assumed of a: if the unshifted pairing fails to
be integrable then so does the shifted one, and both Bochner integrals are 0.
The antisymmetric shift leaves the divergence-form weak equation invariant.
If -∇·a∇u = ∇·g weakly on U and C is a constant skew matrix, then
-∇·(a − C)∇u = ∇·g weakly on U. Nothing is assumed of a.
The shift by +C (C skew) is likewise invisible.
The invariance as an equivalence: the shifted and unshifted equations have exactly the same solutions.
The antisymmetric shift on the §4.3 Dirichlet carrier. The boundary clause
of IsDirichletSolutionOn constrains only u - h, so it is untouched by a
change of coefficient field; only the equation moves, by the theorem above.
This is exactly the display.
6. The energy identity of the shifted field #
A skew matrix contributes nothing to the quadratic form.
The symmetric part is untouched by a skew shift.