EnergyBridge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Energy bridge: solutionEnergyNorm versus the response functional #
Source: ABK26 (e.Jenergyv.nosymm as used in the proof of l.Dh.bound):
‖σ^{1/2} ∇w‖²_{L²(□₀)} = 2 J(□₀, p, q; a), w = ½ v(·, □₀, p, q; a).
In the CoarseGraining vocabulary the left-hand side of that display, for the
unscaled maximizer v, is Ch03.solutionEnergyNorm Q a v ^ 2, i.e. the
square root of Ch02.variationEnergyValue. The public maximizer-energy
identity responseJ_eq_energy_of_isResponseMaximizer gives J = ½ · energy,
hence energy = 2 J.
Every statement here is proved at a general Chapter 2 Domain d; the triadic
cube form (the vocabulary consumed by the coarse Poincaré inequality) is a
specialization stated for an arbitrary triadic cube Q, not only the origin
cube, as required by the descendant-cube consumers.
Energy bridge at a general domain. The variational energy of a response maximizer is twice the response functional.
Energy bridge in the Chapter 3 cube vocabulary, at an arbitrary triadic
cube. The Chapter 3 solution energy norm of a response maximizer on
cubeDomain Q is √(2 J).
The energy bridge in the form used by the assembly: the Chapter 3 energy
norm of a maximizer is √2 · √J.
The Chapter 3 energy norm of a maximizer is bounded by 2 √J; this is the
form fed to the assembly, where all constants are absorbed.