MuExpansion

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

Two-sided expansion of the doubled mu functional along the path

The doubled mu functional is an infimum over a class of doubled fields that does not depend on the coefficient, while the energy of every fixed field expands exactly quadratically along t ↦ perturbCoeffOn U a h t. Testing the infimum with the base minimizer yields the upper second-difference expansion of l.sensitivity.coarse.grained.general.

The printed suggestion to obtain the lower estimate by "applying the same argument with -h in place of h" at the same base field proves an estimate about a - h, not the required lower bound at a + h. The faithful route applies the upper estimate at the shifted base field: testing the base infimum with the shifted minimizer yields doubledMu_perturbCoeffOn_expansion_lower, whose linear term is the one attached to the shifted base.

The exact value-level expansion along the path

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMuValue_perturbCoeffOn {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t : ℝ) {X : HCPolySupport.Book.Ch02.DoubledField d} (hpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hflux : HCPolySupport.MemVectorL2 U.carrier X.flux) : HCPolySupport.Book.Ch02.doubledMuValue U (Frozen.Section24.perturbCoeffOn U a h t) X = HCPolySupport.Book.Ch02.doubledMuValue U a X + t * pathLinearTerm a (↑↑h) X + t ^ 2 * pathQuadraticTerm a (↑↑h) X

Exact expansion of the doubled energy value along the canonical path. For every doubled field with vector-L² components, E_t(X) = E_0(X) + t ℓ(X) + t² q(X) with no remainder.

Competitor bounds

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMu_le_doubledMuValue {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.IsDoubledMuAdmissible U P X) : HCPolySupport.Book.Ch02.doubledMu U a P ≤ HCPolySupport.Book.Ch02.doubledMuValue U a X

The doubled mu infimum is bounded by the value of any admissible doubled field.

The two-sided second-difference expansion

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMu_perturbCoeffOn_expansion_upper {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t : ℝ) (P : HCPolySupport.BlockVec d) {X : HCPolySupport.Book.Ch02.DoubledField d} (hX : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U a P X) : HCPolySupport.Book.Ch02.doubledMu U (Frozen.Section24.perturbCoeffOn U a h t) P - HCPolySupport.Book.Ch02.doubledMu U a P - t * pathLinearTerm a (↑↑h) X ≤ t ^ 2 * pathQuadraticTerm a (↑↑h) X

Upper second-difference expansion at the base field (source: the chain of displays from e.variational.mu.U.P to the final display of the proof of l.sensitivity.coarse.grained.general, upper half). Testing the perturbed infimum with a base minimizer X gives mu_t - mu_0 - t ℓ(X) ≤ t² q(X).

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMu_perturbCoeffOn_expansion_lower {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t : ℝ) (P : HCPolySupport.BlockVec d) {X : HCPolySupport.Book.Ch02.DoubledField d} (hX : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U (Frozen.Section24.perturbCoeffOn U a h t) P X) : t * pathLinearTerm a (↑↑h) X + t ^ 2 * pathQuadraticTerm a (↑↑h) X ≤ HCPolySupport.Book.Ch02.doubledMu U (Frozen.Section24.perturbCoeffOn U a h t) P - HCPolySupport.Book.Ch02.doubledMu U a P

Testing the base infimum with a minimizer X of the shifted problem gives t ℓ(X) + t² q(X) ≤ mu_t - mu_0, where ℓ(X), q(X) are still the base response terms.