OffGridErrorFluxCorrected #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The shallow re-parameterization, and the development carrier #
The lower layer (fluxCorrectedNormalizedBlockResponseRepresentative) already
separates the correction cube Q from the response cube R, so the fix is a
shallow re-parameterization.
Two definitions
fluxCorrectedMaxDescendantAtRoot— the descendant maximum over the shells of an arbitrary root cube, with the correction cube and the comparator held fixed;fluxCorrectedErrorFunctionalAtRoot— the corresponding error functional,
together with the reduction
fluxCorrectedErrorFunctionalAtRoot M L k (originCube d k) (originCube d k) s
(isotropicComparatorMatrix (Annealed.sigmaBar M k))
= fluxCorrectedErrorFunctional M L k s
which holds by rfl: the generalized object is a conservative extension of the
proved one, matching it exactly at the matched index.
Main results #
isEllipticFieldOn_fluxCorrectedRegField— pointwise ellipticity on the half-open realization of a cube.ae_forall_homogenizationErrorOnCube_eq_fluxCorrectedErrorFunctionalAtRoot— the representative identification, at every root, on one event.ae_offGridErrorFunctional_le_fluxCorrectedErrorFunctionalAtRoot— the composed estimate in the development carriers.
References #
- ABK26,
e.mathcalE.stability.applied. - Repo,
fluxCorrectedNormalizedBlockResponseRepresentativeandfluxCorrectedErrorFunctionalinSection4/Support/FluxCorrectedRepresentative.lean.
1. Pointwise ellipticity of the flux-corrected field on a cube #
Pointwise ellipticity of the flux-corrected field on a triadic cube.
The proved witness is an almost everywhere statement; the countable
subadditivity consumes CoarseGraining's IsEllipticFieldOn, which is pointwise
on the set. Both clauses are available from the proved ingredients, on the
half-open realization.
2. F1': the shell root separated from the correction and comparator #
The F1' descendant maximum. The shells are taken over the descendants of an
arbitrary root cube, while the flux correction (Q, at scale m) and the
comparator a0 stay at the parent's index. Compare
fluxCorrectedMaxDescendantNormalizedBlockResponseRepresentative, which forces
root = Q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The F1' error functional. 𝓔_{s,∞,2} at the cube root, taken with the
flux correction and the comparator of the parent index.
Equations
- One or more equations did not get rendered due to their size.
Instances For
3. The representative identification, at every root #
On one probability-one event, CoarseGraining's 𝓔_{s,∞,2} of the
flux-corrected family coincides with the F1' functional at every root cube.
4. The composed estimate in the development carriers #
The composed off-grid stability estimate in the development carriers.
On one probability-one event, for every real translate w, every child cube
P and every lattice cube K with w + □_P ⊆ □_K:
𝓔_{t,∞,2}(w + □_P; ã_{L,m}, σ_m)
≤ (36dt/((t−u)(1−2u)))^{1/2} · 3^{u(K.scale − P.scale)}
· 𝓔_{u,∞,2}(□_K; ã_{L,m}, σ_m) ,
Both printed depths (K.scale − P.scale = 1, 2) are instances.