H10Witness #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The zero-trace witness for the response combination ½(∇v* + ∇v) + p #
Source: ABK26. The D_h splitting identity
quadForm_coarseMatrixDerivative_eq_split consumes a single input, namely that
the combination
∇w + ∇w* + p = ½ (∇v(·,U,p,q;a) + ∇v(·,U,p,-q;aᵗ)) + p
belongs to L²_{pot,0}(U), i.e. is a.e. the gradient of an honest H¹₀(U)
function. This module supplies that witness at an arbitrary Chapter 2 domain.
The proof is an adjoint flip carried out inside the doubled-mu formalism.
Let X be a minimizer of mu(U, (-p, q); a), which exists at every Chapter 2
domain and coefficient by doubledMuTheory. Two facts about X combine:
- admissibility.
IsDoubledMuAdmissible U (-p, q) Xsays by definition thatX.potential - (-p) ∈ L²_{pot,0}(U), and theL²_{pot,0}predicate is literally "a.e. equal to the gradient of anH¹₀function". So theH¹₀witness is already there; only its gradient has to be identified. - extraction. Writing
B xfor the lower block ofA(x) X(x), the public CoarseGraining extraction lemma givesX.potential + B =ᵃᵉ ∇vfor the primal canonical maximizer at(p, q), and its flip-flip/transpose companiondoubledMuMinimizer_neg_left_extracts_adjointMaximizerGradient(proved inProvider/Path/DhIdentification.lean) givesX.potential - B =ᵃᵉ ∇v*for the adjoint canonical maximizer ofaᵗat(p, -q). Adding the two killsBand yieldsX.potential =ᵃᵉ ½ (∇v* + ∇v).
Chapter 2 a.e. uniqueness of maximizer gradients then replaces the two canonical maximizers by arbitrary given ones, which is exactly the hypothesis shape of the splitting identity.
No convexity, ellipticity, selection, representative, or recovery-system
premise is needed beyond what Domain d and CoeffOn U already carry.
The potential block of a mu-minimizer is the half-sum of the two #
maximizer gradients
Adjoint flip for the potential block. For a doubled-mu minimizer X
at loading (-p, q), the potential block is a.e. the half-sum of the adjoint
and primal canonical response-maximizer gradients.
This is the sum of the two extraction lemmas: the lower block image B of X
enters the primal extraction with a + and the adjoint extraction with a -,
so it cancels.
The H¹₀ witness at a general Chapter 2 domain #
The zero-trace witness for the response combination.
At any Chapter 2 domain U and coefficient a, given a response maximizer v
for (a, p, q) and a maximizer vAdj for the adjoint problem (aᵗ, p, -q),
the field ½ (∇vAdj + ∇v) + p is a.e. the gradient of an H¹₀(U) function.
This is exactly the u-premise of
quadForm_coarseMatrixDerivative_eq_split.
The frozen unit-cube carrier #
The zero-trace witness at the frozen unit-cube carrier.