DhIdentification

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Identification of the linear path term with the D_h quadratic form

The linear response term of a doubled-mu minimizer at loading (-p, q) is exactly ½ (p,-q) · D_h(U; a) (p,-q): the source display ⨍ 2(∇w + ∇w*)·h(∇w - ∇w*) = ⨍ ∇v*·h∇v = P·D_h(U;a)P.

The doubled-mu minimizer encodes both scalar maximizers. The primal one is extracted by the public CoarseGraining lemma doubledMuMinimizer_neg_left_extracts_canonicalMaximizerGradient; the adjoint one is extracted here by transporting the minimizer through the exact symmetry mu(U, (P₁,P₂); aᵗ) = mu(U, (P₁,-P₂); a) realized by the flux flip, and then applying the same public extraction lemma at the transposed field.

The flux flip and the transpose symmetry of the mu problem

def Algsuperdiff.Section24.Sensitivity.Provider.Path.fluxFlip {d : ℕ} (X : HCPolySupport.Book.Ch02.DoubledField d) : HCPolySupport.Book.Ch02.DoubledField d

Flux flip of a doubled field.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Path.fluxFlip X = { potential := X.potential, flux := fun (x : HCPolySupport.Vec d) => -X.flux x }

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.fluxFlip_fluxFlip {d : ℕ} (X : HCPolySupport.Book.Ch02.DoubledField d) : fluxFlip (fluxFlip X) = X

The flux flip is an involution.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.solenoidalZeroNormalTraceFieldOn_neg {d : ℕ} {U : Set (HCPolySupport.Vec d)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U g) : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U fun (x : HCPolySupport.Vec d) => -g x

The solenoidal zero-normal-trace class is closed under negation.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.isDoubledMuAdmissible_fluxFlip {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {P : HCPolySupport.BlockVec d} {X : HCPolySupport.Book.Ch02.DoubledField d} (hX : HCPolySupport.Book.Ch02.IsDoubledMuAdmissible U P X) : HCPolySupport.Book.Ch02.IsDoubledMuAdmissible U (P.1, -P.2) (fluxFlip X)

The flux flip maps the admissible class at (P₁, P₂) onto the admissible class at (P₁, -P₂).

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMuValue_transpose_fluxFlip {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (X : HCPolySupport.Book.Ch02.DoubledField d) : HCPolySupport.Book.Ch02.doubledMuValue U a.transpose (fluxFlip X) = HCPolySupport.Book.Ch02.doubledMuValue U a X

The doubled energy value is invariant under simultaneous transpose of the coefficient and flux flip of the field: pointwise exact, no null sets.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.isDoubledMuMinimizer_transpose_fluxFlip {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {a : HCPolySupport.Book.Ch02.CoeffOn U} {P : HCPolySupport.BlockVec d} {X : HCPolySupport.Book.Ch02.DoubledField d} (hX : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U a P X) : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U a.transpose (P.1, -P.2) (fluxFlip X)

The flux flip transports mu-minimizers of the base problem to mu-minimizers of the transposed problem at the flux-flipped loading.

The adjoint extraction

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMuMinimizer_neg_left_extracts_adjointMaximizerGradient {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (p q : HCPolySupport.Vec d) {X : HCPolySupport.Book.Ch02.DoubledField d} (hX : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U a (-p, q) X) : (fun (x : HCPolySupport.Vec d) => X.potential x - (HCPolySupport.blockMatVecMul (HCPolySupport.blockCoeffField a.toCoeffField x) (X.eval x)).2) =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] fun (x : HCPolySupport.Vec d) => (HCPolySupport.Book.Ch02.canonicalMaximizer ⋯ p (-q)).toSolution.toH1.grad x

A doubled-mu minimizer at loading (-p, q) extracts the gradient of the adjoint scalar canonical response maximizer from the difference of its potential and its lower block image. Companion of the public CoarseGraining lemma doubledMuMinimizer_neg_left_extracts_canonicalMaximizerGradient, obtained by transporting the minimizer through the flux-flip/transpose symmetry.

The identification of the linear path term

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearTerm_isDoubledMuMinimizer_eq {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (p q : HCPolySupport.Vec d) {X : HCPolySupport.Book.Ch02.DoubledField d} (hX : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U a (-p, q) X) : pathLinearTerm a (↑↑h) X = 1 / 2 * HCPolySupport.blockVecDot (p, -q) (HCPolySupport.blockMatVecMul (Frozen.Section24.coarseMatrixDerivative U a ↑h) (p, -q))

The linear path term of a mu-minimizer is the D_h quadratic form. For a doubled-mu minimizer X at loading (-p, q),

ℓ(X) = ½ (p,-q) · D_h(U; a) (p,-q),

which is exactly the response-derivative slope in the frozen target responseJ_derivative. Source: the display chain ⨍ 2(∇w + ∇w*)·h(∇w - ∇w*) = ⨍ ∇v*·h∇v = P·D_h(U;a)P combined with the characterization theorem of the coarse-matrix derivative.