LocalizationBasicSplit #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the localization cell algebra of e.lower.bound.basic.split #
Source display in ABK26:
e.lower.bound.basic.split(label; display):
whereP . bfA_m(cu_K) P <= avsum_{z} fint_{z+cu_n} X_z . bfA_m X_z = avsum_{z} ( P_z . bfA_m(z+cu_n) P_z + 2 P_z . fint_{z+cu_n} bfA_m tilde S_z + fint_{z+cu_n} tilde S_z . bfA_m tilde S_z ) ,X_z = S_z + tilde S_z,S_zis the minimizer ofe.variational.mu.U.P(label) onz + cu_nat the constant loadP_zofe.Pz.def, andtilde S_zis the minimizer of the same energy over the affine class based at the mean-zero fieldF_zofe.Fz.def.
This module supplies the cell algebra of that display: everything that
happens inside one localization cube, with the localization cube entering only
as a free Domain. The mesh average avsum_{z in 3^n Z^d cap cu_K} and the
gluing of the cell fields into one competitor on cu_K are not treated
here; see the disclosure below.
What is proved #
isDoubledTestField_sub_constantDoubledField-- an admissible field minus its constant load is a test field.doubledMuValue_add-- the exact quadratic expansion `E(S + T) = E(S) + E(T)- fint S. bfA T` (the three summands of the middle line of the display).
volumeAverage_doubledBlockPairingIntegrand_of_isDoubledResponseField-- the cross term collapses toP . fint bfA T, which is the Euler--Lagrange equation ofTtested againstS - P.isDoubledResponseField_of_forall_le_add_isDoubledTestField-- the first variation: a field minimizing the doubled energy against all test-field perturbations is a doubled response field. This is what makes the previous item applicable totilde S_z, whose defining variational problem is based at the fieldF_zrather than at a constant, so that CoarseGraining'sDoubledMuTheory.minimizer_first_variationdoes not apply to it directly.two_mul_doubledMuValue_add_eq-- the cell form of the equality line ofe.lower.bound.basic.split.blockVecDot_coarseBlockMatrix_le_two_mul_doubledMuValue-- the cell form of the inequality line, i.e. competitor insertion intoe.variational.mu.U.P.
Divergences from the printed statement #
blockVecDot_coarseBlockMatrix_le_two_mul_doubledMuValuebelow is stated with<=, and no declaration in this module asserts the reverse.- The factor two. The manuscript's
fint_U X . bfA Xis twice CoarseGraining'sdoubledMuValue, whose integrand is1/2 X . bfA X; correspondinglymu(U,P) = 1/2 P . bfA(U) P. Every statement below carries the factor2explicitly rather than renormalizing either object. - The mesh average and the gluing are absent.
e.lower.bound.basic.splitadditionally uses thatsum_z X_z 1_{z+cu_n}is admissible oncu_Kand thatfint_{cu_K}is the mesh average of thefint_{z+cu_n}. Neither is proved here; the cell statements below are the input those two steps consume.
The constant doubled field of a load #
The constant doubled field with value P. In e.lower.bound.basic.split
this is the affine background P_z of e.Pz.def viewed as a field on the
localization cube.
Equations
- Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.constantDoubledField P = { potential := fun (x : HCPolySupport.Vec d) => P.1, flux := fun (x : HCPolySupport.Vec d) => P.2 }
Instances For
An admissible field for e.variational.mu.U.P at load P differs from the
constant field P by a test field.
Integrability of the pairing density #
The block pairing density of two vector-L² doubled fields is integrable.
The exact quadratic expansion of the doubled energy #
The exact quadratic expansion of the doubled energy: fint (S+T).bfA(S+T) = fint S.bfA S + fint T.bfA T + 2 fint S.bfA T, written with CoarseGraining's
half-normalized energy value.
The Euler--Lagrange collapse of the cross term #
The cross term of e.lower.bound.basic.split. When the second field is a
doubled response field on U, the block pairing against a mu-admissible
field collapses to the pairing against its constant load: fint_U S. bfA T = P. fint_U bfA T. This is the Euler--Lagrange equation of T tested against the
test field S - P.
Two elementary facts about the normalized average on a domain #
The first variation #
Scaling a test field by a real number gives a test field.
The first variation of the doubled energy. A vector-L² doubled field
whose energy does not decrease under any test-field perturbation satisfies the
Euler--Lagrange equation, i.e. it is a doubled response field on U.
This is what applies to the perturbation tilde S_z: its variational class is
based at the field F_z of e.Fz.def, not at a constant load, so
CoarseGraining's DoubledMuTheory.minimizer_first_variation -- which is stated
for IsDoubledMuMinimizer, i.e. for a constant base -- does not apply to it.
The inequality line of e.lower.bound.basic.split. Inserting any
admissible competitor into e.variational.mu.U.P bounds the coarse block form
from above: P . bfA(U) P <= fint_U X . bfA X.
The equality line of e.lower.bound.basic.split at one localization cube.
With S a minimizer of e.variational.mu.U.P at the constant load P and T
any doubled response field on U,
fint_U (S+T) . bfA (S+T)
= P . bfA(U) P + 2 P . fint_U bfA T + fint_U T . bfA T .
At the manuscript's carriers U = z + cu_n, P = P_z (e.Pz.def), S = S_z,
T = tilde S_z, and S + T = X_z; the response-field hypothesis on T is
discharged from minimality by
isDoubledResponseField_of_forall_le_add_isDoubledTestField.