Continuity

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

Continuity of the linear response term along the perturbation path

The two-sided second-difference expansion of mu produces the base linear term of the perturbed minimizer on the lower side and of the base minimizer on the upper side. Turning the expansion into a derivative therefore requires

ℓ(X_t) → ℓ(X_0) as t → 0.

This module proves the quantitative version |ℓ(X_t) - ℓ(X_0)| ≤ C √|t|. The two ingredients are:

• the energy gap E_0(X_t) - mu_0 ≤ C |t|, obtained by testing each of the two minimum problems with the other minimizer and absorbing the linear terms with abs_pathLinearTerm_le; and
• uniform convexity ½ E_0(X_0 - X_t) ≤ E_0(X_t) - mu_0 together with the Young estimate for the bilinear response pairing, whose free parameter is tuned to |t|^{-1/2}.

Polarization of the linear response term

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearPairingDensity_add_eq {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (hField : HCPolySupport.CoeffField d) (X Y : HCPolySupport.Book.Ch02.DoubledField d) (x : HCPolySupport.Vec d) : pathLinearPairingDensity a hField (X - Y) X x + pathLinearPairingDensity a hField Y (X - Y) x = pathLinearDensity a hField X x - pathLinearDensity a hField Y x

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinearTerm_sub_eq {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) {X Y : HCPolySupport.Book.Ch02.DoubledField d} (hXpot : HCPolySupport.MemVectorL2 U.carrier X.potential) (hXflux : HCPolySupport.MemVectorL2 U.carrier X.flux) (hYpot : HCPolySupport.MemVectorL2 U.carrier Y.potential) (hYflux : HCPolySupport.MemVectorL2 U.carrier Y.flux) : pathLinearTerm a (↑h) X - pathLinearTerm a (↑h) Y = pathLinearPairing a (↑h) (X - Y) X + pathLinearPairing a (↑h) Y (X - Y)

Polarization of the linear response term. The difference of the linear terms of two doubled fields splits into two bilinear pairings, each of which carries the difference field in one slot.

Constants

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinConst {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) : ℝ

Domination constant of the linear response term by the doubled energy.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinConst_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) : 0 ≤ pathLinConst a h

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathSmallParam {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) : ℝ

The parameter window on which the energy gap is linear in t.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Path.pathSmallParam a h = 1 / (2 * Algsuperdiff.Section24.Sensitivity.Provider.Path.pathLinConst a h + 2)

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathSmallParam_pos {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) : 0 < pathSmallParam a h

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathSmallParam_le_one {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) : pathSmallParam a h ≤ 1

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathGapConst {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (P : HCPolySupport.BlockVec d) : ℝ

Energy-gap constant.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMu_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (P : HCPolySupport.BlockVec d) : 0 ≤ HCPolySupport.Book.Ch02.doubledMu U a P

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathGapConst_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (P : HCPolySupport.BlockVec d) : 0 ≤ pathGapConst a h P

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.pathContConst {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (P : HCPolySupport.BlockVec d) : ℝ

Continuity constant of the linear response term.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathContConst_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfMatrixFieldOn U) (P : HCPolySupport.BlockVec d) : 0 ≤ pathContConst a h P

The energy gap

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMuValue_sub_doubledMu_le {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (P : HCPolySupport.BlockVec d) {t : ℝ} (ht : |t| ≤ pathSmallParam a ↑h) {Xt : HCPolySupport.Book.Ch02.DoubledField d} (hXt : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U (Frozen.Section24.perturbCoeffOn U a h t) P Xt) : HCPolySupport.Book.Ch02.doubledMuValue U a Xt - HCPolySupport.Book.Ch02.doubledMu U a P ≤ pathGapConst a (↑h) P * |t|

Energy gap of the perturbed minimizer. Testing each minimum problem with the other minimizer and absorbing the linear terms bounds the base energy of the perturbed minimizer linearly in t.

Continuity of the linear response term

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.abs_pathLinearTerm_sub_le {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (P : HCPolySupport.BlockVec d) {t : ℝ} (ht : |t| ≤ pathSmallParam a ↑h) (ht0 : t ≠ 0) {X0 Xt : HCPolySupport.Book.Ch02.DoubledField d} (hX0 : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U a P X0) (hXt : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U (Frozen.Section24.perturbCoeffOn U a h t) P Xt) : |pathLinearTerm a (↑↑h) Xt - pathLinearTerm a (↑↑h) X0| ≤ pathContConst a (↑h) P * √|t|

Minimizer continuity. The base linear response term of the perturbed minimizer converges to that of the base minimizer, with rate √|t|.