LocalizationSelectionSum

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

Provider: X_z = S_z + tilde S_z

The two minimizers it relates are

• S_z := S(., z+cu_n, -P_z, 0; a_m), the minimizer at the constant load P_z of e.Pz.def;
• tilde S_z, the minimizer over bfF_z + (L^2_{pot,0} x Lsolo)(z+cu_n) with bfF_z of e.Fz.def;

and the field they sum to is X_z, the minimizer over the class based at bfAhom_{m-h}^{-1/2}(e' + grad w_D^{(K)}, e + grad w_N^{(K)} + shom_{m-h}^{-1} h e'), which is exactly constantDoubledField P_z + bfF_z.

What is proved

• isDoubledTestField_sub -- the doubled test fields are closed under differences.
• isDoubledMuMinimizerField_add -- ****: if S minimizes the doubled energy at the constant load P and T minimizes it over the field-slope class of F, then S + T minimizes it over the field-slope class of constantDoubledField P + F.

Method

Purely variational, and it uses no positivity of bfA and no ambient-field hypothesis. For a competitor W of the sum class, W - S lies in the class of F, so E(T) <= E(W - S); the quadratic expansion (LocalizationBasicSplit.doubledMuValue_add) then reduces the claim to the vanishing of the cross pairing of S against the test field W - S - T, which is upstream's DoubledMuTheory.minimizer_first_variation for S combined with the a.e. symmetry of bfA(x). Only the first variation of S is used, not its minimality.

Divergences from the printed statement

• . The carrier is Chapter 2's DoubledField d over Domain d; see LocalizationSelectionExistence.lean.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledTestField_sub {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {Y Z : HCPolySupport.Book.Ch02.DoubledField d} (hY : HCPolySupport.Book.Ch02.IsDoubledTestField U Y) (hZ : HCPolySupport.Book.Ch02.IsDoubledTestField U Z) : HCPolySupport.Book.Ch02.IsDoubledTestField U (Y - Z)

The doubled test fields are closed under differences.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledMuMinimizerField_add {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {a : HCPolySupport.Book.Ch02.CoeffOn U} {P : HCPolySupport.BlockVec d} {F S T : HCPolySupport.Book.Ch02.DoubledField d} (hFpot : HCPolySupport.MemVectorL2 U.carrier F.potential) (hFflux : HCPolySupport.MemVectorL2 U.carrier F.flux) (hS : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U a P S) (hT : IsDoubledMuMinimizerField U a F T) : IsDoubledMuMinimizerField U a (constantDoubledField P + F) (S + T)

ABK26's selection split: X_z = S_z + tilde S_z.

If S minimizes the doubled energy of e.variational.mu.U.P at the constant load P, and T minimizes it over the field-slope class of F, then S + T minimizes it over the field-slope class of constantDoubledField P + F.

At the manuscript's carriers U = z + cu_n, P = P_z (e.Pz.def), F = bfF_z (e.Fz.def), S = S_z, T = tilde S_z, and `constantDoubledField P_z

• bfF_zis the background of theX_zdisplay, so the conclusion is precisely thatS_z + tilde S_zrealizes theargmindefiningX_z`.

Equality mode: if X_z is defined as S_z + tilde S_z, the identity is literal. If X_z is instead selected independently as the argmin of its own display, this theorem combined with a.e. uniqueness (sameAE_of_isDoubledMuMinimizerField) yields only X_z = S_z + tilde S_z almost everywhere.