FreshShellCorrectorEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The fresh-shell corrector energy is the (J4) constant #
ABK26, assumption a.j.nondeg and the first equality of e.perturb.assumption,
at the fresh shell k = 0.
Algsuperdiff/Section3/Provider/Corrector/CorrectorLimitNode.lean proves the
corrector limit e.corrector.limit at the fresh shell, on the continuous-path
carrier C(Vec d, Mat d); its limit value is the energy E[|∇w|²] = ∫ ‖valuePathCorrectorRepr M he‖² of the canonical Helmholtz corrector of that
carrier. The frozen assumption (J4)
(Algsuperdiff/Frozen/Assumptions/ShellLawJ4.lean) states the corrector energy
on CoarseGraining's regular-field carrier RegCoeffField d, as
‖ShellField.zeroShellPotentialCorrector …‖² = c⋆ log 3.
Algsuperdiff/Section3/Provider/Corrector/ValuePathTransport.lean states
explicitly that its canonical corrector is not identified with
ShellField.zeroShellPotentialCorrector: only the forcing, its covariance and
its forcing energy are shown to agree there. This file supplies the missing
identification — of the corrector energies — and therefore evaluates the
corrector limit at the literal constant c⋆ log 3.
How the identification is made #
The two carriers are related by the forgetful map
regOfPath : C(Vec d, Mat d) → RegCoeffField d
— a continuous matrix path is an entrywise measurable, locally integrable
coefficient field — which is measurable, equivariant for the two real
translation actions, satisfies regOfPath ∘ valuePath = forgetShell, and hence
pushes the transported zero-shell law forward to CoarseGraining's zero-shell
law. The generic comparison of
Algsuperdiff/Section3/Provider/Corrector/StationaryCarrierTransport.lean then
gives, for the Koopman isometry T of regOfPath and its Hilbert adjoint,
P_path (T F) = T (P_reg F),
whence the two projected energies agree. No identification of the two carrier
σ-algebras, no surjectivity of T, and no cyclic-subspace or
covariance-isomorphism argument is used: the adjoint replaces all of them.
Main results #
norm_valuePathPotentialCorrector_eq— the two canonical corrector energies agree.integral_normSq_valuePathCorrectorRepr_eq— the path-carrier corrector energy equalsc⋆ log 3, withc⋆ = Disorder.cstar Mthe selected (J4) constant.
Disclosure. This file realizes the fresh-shell (k = 0) instance of the
first equality of e.perturb.assumption, with its |e|² factor, and without
the shell sum Σ_{k = m-h+1}^m, the σ_{m-h}^{-2} normalization and the
3^{2γk} dilation factor; those three are not proved here. Its inputs are the frozen assumptions
(J1),
(J2), (J4) through ABKModel, the proved corrector limit of
CorrectorLimitNode.lean, and Mathlib. No draft theorem, in particular not
Frozen.External.calderon_zygmund, is used.
The forgetful map from continuous paths to CoarseGraining regular fields #
A continuous matrix-valued path, read as an CoarseGraining regular coefficient field. Continuity supplies both carrier obligations: entrywise measurability and entrywise local integrability.
Equations
- Algsuperdiff.Section3.Provider.Corrector.regOfPath f = { toFun := ⇑f, entry_measurable := ⋯, entry_locInt := ⋯ }
Instances For
The two forgetful maps of the shell carrier agree: forgetting the shell packaging is reading the value path as a regular field.
Both carriers use the manuscript translation convention, so the forgetful map is equivariant.
The forgetful map is measurable for CoarseGraining's full regular-field
σ-algebra, including the compactly supported integral generators.
The forgetful map pushes the transported zero-shell law forward to CoarseGraining's zero-shell law: both are pushforwards of one and the same shell-zero law.
The transported forcing is the path-carrier forcing #
The Koopman transport of the CoarseGraining forcing is the path-carrier forcing.
The two corrector energies agree #
The canonical fresh-shell corrector energies of the two carriers agree.
The L² norm square of the path-carrier corrector is the expectation of the
squared Euclidean norm of its strongly measurable representative.
The fresh-shell corrector energy is c⋆ log 3 — the first equality of
e.perturb.assumption at the fresh shell k = 0, at a unit direction, read
through assumption a.j.nondeg.