ShellSumConsumerTransport #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The shell-sum corrector limit at the recurrence consumer's data #
ABK26, e.def.w and e.perturb.assumption.
Algsuperdiff/Section3/Provider/Corrector/ShellSumCorrectorLimit.lean proves the
corrector limit at the shell-sum law shellSumValuePathLaw M.P n m on the
compact-open carrier, in the Helmholtz shape
(IsPotentialZeroTraceOn / IsSolenoidalOn and the Neumann pair), at the
forcing realize (valuePathForcing e).
The recurrence consumer
(Provider/Diffusivity/ApproximateRecurrence/LocalizationRecurrenceMesh.lean)
presents the same data in three different shapes:
- it forces with
Corrector.streamForcing σ⁻¹ ω.val (m−h) m e, a function of a shell sequence, not of a continuous path; - it works with
ω : CutoffSample d, the subtype of lower-tail-good sequences, undercutoffSampleLaw M, not withM.Pand not with the path law; - it states the two corrector equations in the weak-solution shape
IsZeroTraceDirichletRhsWeakSolution/IsMeanZeroNeumannRhsWeakSolution.
This module removes all three differences.
What is supplied #
toVec_realize_valuePathForcing_shellSumValuePath— the forcing identification: the realization of the path forcing at the increment path is literally the consumer'sstreamForcing, with the gaugeσ⁻¹carried by the direction. Both sides arematVecMul (finiteShellIncrement ω n m (x + ·)) e, so the proof is a normalization ofmatVecMulin the second argument.map_shellSumValuePath_cutoffSampleLaw— the law transport: the law of the increment path under the subtype lawcutoffSampleLaw Mis the shell-sum lawshellSumValuePathLaw M.P n m. The subtype inclusion is null-conull forM.P(Cutoff.map_cutoffSampleLaw_val), so the two laws coincide; no new assumption enters.tendsto_integral_cutoffSample_cubeAverage_dirichlet_neumann_shellSum— the corrector limit with the sample integral taken overCutoffSample dagainstcutoffSampleLaw M, i.e. at the consumer's carrier.tendsto_integral_cutoffSample_cubeAverage_of_weakSolutions— the same, with the two corrector equations entered in the consumer's weak-solution shape and the consumer's own forcingstreamForcing σ⁻¹ ω.val n m e.
The shape of the corrector families #
The corrector families below are indexed by the increment path, not by the
sample: wD : ℕ → C(Vec d, Mat d) → H10Function …. That is the honest reading
of e.def.w, whose right-hand side depends on the sample only through
k_m − k_{m−h}; it is also what makes the sample integral computable, since the
integrand is then a pullback along shellSumValuePath n m ∘ Subtype.val and
map_shellSumValuePath_cutoffSampleLaw applies. No uniqueness or solvability
theorem is used or needed.
The forcing identification #
The recurrence consumer's forcing is the realization of the path forcing.
Corrector.streamForcing c ω n m e is c • (k_m − k_n)(·) e, and the
realization of valuePathForcing (c • e) at the increment path is
(k_m − k_n)(· + 0) (c • e); the two agree because matVecMul is linear in its
vector argument. The gauge σ_{m−h}^{-1} of the consumer is therefore carried
by the direction, at no cost.
The realization of the path forcing is continuous in space, at every path.
This discharges the MemVectorL2 binder of the weak/Helmholtz bridge.
The subtype law transports to the shell-sum law #
The CutoffSample/ShellSeq law transport.
The law of the finite shell increment, read on the subtype of lower-tail-good
sequences under cutoffSampleLaw M, is the shell-sum law of
ShellSumCarrierLaw.lean. The only input is
Cutoff.map_cutoffSampleLaw_val, i.e. that the good set is conull for M.P.
The measure-preserving form of the law transport.
Integrals of pullbacks along the increment path are computed at the shell-sum law.
The corrector limit at the consumer's carrier #
l.corrector.limit at the shell-sum forcing, with the sample integral
taken over the consumer's carrier.
Same statement as
tendsto_integral_cubeAverage_dirichlet_neumann_shellSum, with the ambient
sample space C(Vec d, Mat d) replaced by CutoffSample d under
cutoffSampleLaw M — the carrier the recurrence consumer integrates over. The
corrector families are indexed by the increment path, which is what e.def.w
gives.
The corrector limit at the consumer's weak-solution data.
The corrector equations are entered in the shape the recurrence consumer
produces — IsZeroTraceDirichletRhsWeakSolution 1 (openCubeSet □_K) (wD K f) (−𝐟)
and its mean-zero Neumann counterpart — rather than in the Helmholtz shape; the
translation is FreshShellSumWeakBridge. At an increment path the forcing 𝐟
here is the consumer's Corrector.streamForcing c ω n m e, by
toVec_realize_valuePathForcing_shellSumValuePath, so the consumer's gauge
σ_{m−h}^{-1} enters as the scalar c and needs no separate step.