LocalizationSelectionExistence

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

Provider: the field-slope doubled minimizer of the localization split

Source displays in ABK26:

• e.Pz.def, e.Fz.def;
• e.lower.bound.basic.split.

Both X_z and tilde S_z are minimizers of the doubled energy over a class whose slope datum is a field, not a constant:

X_z      = argmin { fint_{z+cu_n} (1/2) X . bfA_m X :
              X in bfAhom^{-1/2}(e'+grad w_D, e+grad w_N+shom^{-1} h e')
                     + (L^2_{pot,0} x Lsolo)(z+cu_n) }
tilde S_z = argmin { fint_{z+cu_n} (1/2) X . bfA_m X :
              X in bfF_z + (L^2_{pot,0} x Lsolo)(z+cu_n) }

The upstream repository provides the doubled variational theory only for the constant-slope class (Homogenization.Book.Ch02.IsDoubledMuAdmissible, doubledMuTheory), and upstream may not be edited. This module supplies the field-slope layer at the same carriers.

What is proved

• IsDoubledMuAdmissibleField / IsDoubledMuMinimizerField -- the field-slope admissible class and its argmin predicate, definitionally the test-field-difference class IsDoubledTestField U (X - F) used by the localization gluing modules.
• exists_isDoubledMuMinimizerField -- existence: for every Domain, every Chapter-2 coefficient a : CoeffOn U and every vector-L^2 slope field F, the argmin above exists; moreover any competitor whose energy does not exceed the minimizer's agrees with it a.e., which is the strict-convexity uniqueness.
• sameAE_of_isDoubledMuMinimizerField -- uniqueness a.e. of the field-slope minimizer, so that the manuscript's tilde S_z and X_z are well defined up to a null set.
• isDoubledMuAdmissibleField_self, isDoubledMuAdmissibleField_add and the MemVectorL2 accessors used by the downstream modules.

Method

The analytic engine is upstream's coercive affine Hilbert projection Homogenization.affineMinimizerMap on L^2(U; R^{2d}), which is already stated at an arbitrary ambient anchor; only its wrapper MuHilbertProblem.minimizerMap specializes it to a constant BlockVec d. The closed correction space L^2_{pot,0}(U) x Lsolo(U) together with pointwise representatives of its elements is upstream's PotentialSolenoidalL2RecoveryData, produced on every open bounded convex domain by exists_recoveryData_of_mu_eq_muCandidate_of_isOpenBoundedConvexDomain; the identification of the Hilbert quadratic energy with doubledMuValue is upstream's quadraticEnergy_eq_blockEnergyAverage_of_blockState. No analytic fact is reproved here.

Divergences from the printed statement

• Here the carrier is Chapter 2's DoubledField d over Domain d; the identity doubledMuValue = blockEnergyAverage . blockStateOfDoubled holds by rfl (doubledMuValue_eq_blockEnergyAverage below) and the constant-slope class is recovered definitionally.
• Pointwise vs a.e. coefficient. CoeffOn U carries only a.e. ellipticity, while the upstream recovery machinery consumes a pointwise IsEllipticFieldOn witness. The proof therefore runs on upstream's pointwise representative pointwiseCoeffOn U a and transports the conclusion along CoeffOn.AEEq, exactly as upstream's own doubledMuTheory does. No statement below mentions the representative.
• d = 0. In dimension zero every doubled energy vanishes identically and the slope field itself is a minimizer; the theorem is stated uniformly in d and discharges that case separately, again as upstream does.

The field-slope admissible class

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.IsDoubledMuAdmissibleField {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (F X : HCPolySupport.Book.Ch02.DoubledField d) : Prop

The field-slope doubled admissible class: X ∈ F + (L^2_{pot,0} × Lsolo)(U) for a slope datum F that is a field. This is the field-slope analogue of Chapter 2's IsDoubledMuAdmissible, which is the special case of a constant slope.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledMuAdmissibleField_iff_isDoubledTestField_sub {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (F X : HCPolySupport.Book.Ch02.DoubledField d) : IsDoubledMuAdmissibleField U F X ↔ HCPolySupport.Book.Ch02.IsDoubledTestField U (X - F)

The field-slope class is the difference-is-a-test-field class used by the localization gluing modules.

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.IsDoubledMuMinimizerField {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (F X : HCPolySupport.Book.Ch02.DoubledField d) : Prop

The field-slope doubled minimizer predicate, i.e. the argmin of the two displays.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.doubledMuValue_eq_blockEnergyAverage {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 X = HCPolySupport.blockEnergyAverage U.carrier a.toCoeffField (HCPolySupport.Internal.Ch02.BookCh02.blockStateOfDoubled X)

The Chapter-2 doubled energy value is the block energy average of the corresponding block state.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledMuAdmissibleField_self {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (F : HCPolySupport.Book.Ch02.DoubledField d) : IsDoubledMuAdmissibleField U F F

The slope field lies in its own class.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledMuAdmissibleField_add {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {F X Y : HCPolySupport.Book.Ch02.DoubledField d} (hX : IsDoubledMuAdmissibleField U F X) (hY : HCPolySupport.Book.Ch02.IsDoubledTestField U Y) : IsDoubledMuAdmissibleField U F (X + Y)

Adding a test field to an admissible field keeps it admissible.

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

An admissible competitor over a vector-L² slope field is itself vector-L².

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

An admissible competitor over a vector-L² slope field is itself vector-L².

The L² bookkeeping of the affine class

Existence and uniqueness of the field-slope minimizer

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_isDoubledMuMinimizerField {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) {F : HCPolySupport.Book.Ch02.DoubledField d} (hFpot : HCPolySupport.MemVectorL2 U.carrier F.potential) (hFflux : HCPolySupport.MemVectorL2 U.carrier F.flux) : ∃ (X : HCPolySupport.Book.Ch02.DoubledField d), IsDoubledMuMinimizerField U a F X ∧ ∀ (W : HCPolySupport.Book.Ch02.DoubledField d), IsDoubledMuAdmissibleField U F W → HCPolySupport.Book.Ch02.doubledMuValue U a W ≤ HCPolySupport.Book.Ch02.doubledMuValue U a X → W.SameAE X

Existence of the field-slope doubled minimizer.

For every Chapter-2 domain U, coefficient a : CoeffOn U and vector-L² slope field F, the variational problem of e.variational.mu.U.P posed over the affine class F + (L^2_{pot,0} × Lsolo)(U) attains its infimum. The second clause is the strict-convexity uniqueness: any competitor whose energy does not exceed the minimizer's agrees with it a.e. on U.

At the manuscript's carriers this produces tilde S_z (slope bfF_z of e.Fz.def) and X_z (slope bfAhom^{-1/2}(e'+grad w_D, e+grad w_N + shom^{-1} h e')), both on U = z + cu_n.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sameAE_of_isDoubledMuMinimizerField {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {a : HCPolySupport.Book.Ch02.CoeffOn U} {F X Y : HCPolySupport.Book.Ch02.DoubledField d} (hFpot : HCPolySupport.MemVectorL2 U.carrier F.potential) (hFflux : HCPolySupport.MemVectorL2 U.carrier F.flux) (hX : IsDoubledMuMinimizerField U a F X) (hY : IsDoubledMuMinimizerField U a F Y) : X.SameAE Y

Uniqueness a.e. of the field-slope minimizer. Any two minimizers of the doubled energy over the same affine class agree almost everywhere on U, so the manuscript's argmin notation denotes a well-defined object up to a null set.