LocalizationSelectionVariation

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

Provider: the first variation of the field-slope localization minimizer

Source displays in ABK26:

• e.Pz.def and e.Fz.def;
• e.lower.bound.basic.split, whose quadratic expansion is the second line of the display and whose cross-term collapse is the third line, the cross summand itself sitting;

This module joins the existence layer of LocalizationSelectionExistence.lean to the cell algebra of LocalizationBasicSplit.lean: it turns the minimality of the field-slope minimizers into the Euler--Lagrange property that the cell algebra consumes.

What is proved

• isDoubledTestField_add -- the doubled test fields form an additive class (the two halves are Whitney/ZeroExtension.lean's closure lemmas).
• isDoubledAmbientField_of_isDoubledMuAdmissibleField -- a competitor over an ambient slope field is ambient.
• isDoubledResponseField_of_isDoubledMuMinimizerField -- the first variation: a field-slope minimizer is a doubled response field. This is what makes LocalizationBasicSplit's cross-term collapse (volumeAverage_doubledBlockPairingIntegrand_of_isDoubledResponseField) applicable to tilde S_z, whose class is based at the field bfF_z rather than at a constant load.
• two_mul_doubledMuValue_eq_volumeAverage_of_isDoubledMuMinimizerField -- ** with its correct justification**: fint_U tilde S. bfA tilde S = fint_U bfF. bfA tilde S.
• isDoubledMuAdmissibleField_add_of_isDoubledMuAdmissible -- the predicate-level companion of X_z = S_z + tilde S_z: a constant-load admissible field plus a field-slope admissible field is admissible for the shifted slope field.

Divergences from the printed statement

• Mean-zeroness alone does not give the identity; the reason is the Euler--Lagrange equation of the minimizer. Nor does mean-zeroness alone place tilde S_z in the class: ambient membership and integrability of bfF_z come from its gradient/solenoidal structure, and the actual-carrier consumer owes that derivation. two_mul_doubledMuValue_eq_volumeAverage_of_isDoubledMuMinimizerField below uses mean-zeroness nowhere. In the pinned copy is the Hminusul factor of the inequality that follows; the justification sentence is and the identity itself is the first two lines of the display.
• The factor two. As in LocalizationBasicSplit.lean, the manuscript's fint_U X . bfA X is twice CoarseGraining's doubledMuValue; the factor is carried explicitly rather than renormalizing either object.
• . The carrier is Chapter 2's DoubledField d over Domain d; see LocalizationSelectionExistence.lean.

Sums of test fields

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledTestField_add {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 form an additive class.

The constant-slope special case

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledMuAdmissibleField_add_of_isDoubledMuAdmissible {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {P : HCPolySupport.BlockVec d} {F S T : HCPolySupport.Book.Ch02.DoubledField d} (hS : HCPolySupport.Book.Ch02.IsDoubledMuAdmissible U P S) (hT : IsDoubledMuAdmissibleField U F T) : IsDoubledMuAdmissibleField U (constantDoubledField P + F) (S + T)

The predicate-level companion of X_z = S_z + tilde S_z. A constant-load admissible field plus a field-slope admissible field is admissible for the shifted slope field. At the manuscript's carriers, S_z is admissible at the constant load P_z (e.Pz.def), tilde S_z is admissible for bfF_z (e.Fz.def), and the shifted slope field constantDoubledField P_z + bfF_z is exactly the background of the X_z display.

Ambient membership of a competitor

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledAmbientField_of_isDoubledMuAdmissibleField {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {F X : HCPolySupport.Book.Ch02.DoubledField d} (hF : HCPolySupport.Book.Ch02.IsDoubledAmbientField U F) (hX : IsDoubledMuAdmissibleField U F X) : HCPolySupport.Book.Ch02.IsDoubledAmbientField U X

A competitor over an ambient slope field is itself ambient, i.e. lies in Lpot(U) x Lsol(U). Both halves are the corresponding closure of the Chapter-1 field spaces under adding a zero-trace element.

The first variation

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledResponseField_of_isDoubledMuMinimizerField {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {a : HCPolySupport.Book.Ch02.CoeffOn U} {F X : HCPolySupport.Book.Ch02.DoubledField d} (hF : HCPolySupport.Book.Ch02.IsDoubledAmbientField U F) (hX : IsDoubledMuMinimizerField U a F X) : HCPolySupport.Book.Ch02.IsDoubledResponseField U a X

The first variation of the field-slope minimizer. A minimizer of the doubled energy over the affine class F + (L^2_{pot,0} x Lsolo)(U) is a doubled response field on U, i.e. it satisfies the Euler--Lagrange equation against every test field.

At the manuscript's carriers this is the property of tilde S_z that LocalizationBasicSplit.volumeAverage_doubledBlockPairingIntegrand_of_isDoubledResponseField consumes for the cross-term collapse of e.lower.bound.basic.split, the third line of that display it is also the correct justification of the identity.

The energy comparison

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.two_mul_doubledMuValue_eq_volumeAverage_of_isDoubledMuMinimizerField {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {a : HCPolySupport.Book.Ch02.CoeffOn U} {F X : HCPolySupport.Book.Ch02.DoubledField d} (hF : HCPolySupport.Book.Ch02.IsDoubledAmbientField U F) (hX : IsDoubledMuMinimizerField U a F X) : 2 * HCPolySupport.Book.Ch02.doubledMuValue U a X = HCPolySupport.volumeAverage U.carrier (HCPolySupport.Book.Ch02.doubledBlockPairingIntegrand U a F X)

ABK26's variation display, with the justification. For a field-slope minimizer X over the slope field F,

fint_U X . bfA_m X = fint_U F . bfA_m X .

The manuscript justifies this by "since bfF_z has mean zero in z+cu_n"; mean-zeroness is used nowhere below. The identity is the Euler--Lagrange equation of X tested against the test field X - F. Mean-zeroness alone does not place tilde S_z in the class; membership needs the gradient/solenoidal structure and integrability of bfF_z, which the actual-carrier consumer must derive.