CutoffFieldLimit #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Dirichlet solutions of the cutoff fields converge to those of the full field #
Three steps, on the cube y + □_n.
The shift is invisible. The cutoff coefficient a_L and its origin
normalization ã_L = a_L - k_L(0) differ by a constant skew matrix, so they have
exactly the same divergence-form weak solutions
(isDirichletSolutionAt_normalizedCoefficientCutoff_iff). This is the printed
step "the equation is unchanged if we replace a_L by a_L - (k_L - k_m)".
The coefficient distance is geometric. On the cube the entrywise distance
between ã_L and the full field a = ν I + k is at most
Field.cutoffLimitGap, which vanishes geometrically in L.
The solution map is Lipschitz in the coefficient. The energy estimate
sqrt_energy_grad_sub_le gives
‖∇u_L - ∇u‖_{L²(y+□_n)} ≤ ν⁻¹ d² ‖ã_L - a‖_{L^∞(y+□_n)} ‖∇u‖_{L²(y+□_n)} ,
and the zero-trace Poincaré inequality upgrades it to the L² distance of the
values. Both solutions carry the same forcing field g; ν is the symmetric
part of both coefficient fields.
Main results #
exists_isEllipticFieldOn_normalizedCoefficientCutoff,exists_isEllipticFieldOn_streamCoefficient— ellipticity on the cube with lower constantνfor both families.isDirichletSolutionAt_normalizedCoefficientCutoff_iff— the constant skew shift does not change the Dirichlet problem.sqrt_energy_grad_sub_normalizedCutoff_le— the energy estimate with the explicit geometric coefficient distance.exists_poincare_sub_of_isDirichletSolutionAt— theL²distance of two solutions with the same forcing, from the distance of their gradients.exists_l2_bound_cutoff_stream,tendsto_sqrt_integral_sq_sub_cutoff_atTop_zero— theL²convergenceu_L → u.
References #
- ABK26, the localized Dirichlet problems of Section 5.1, and the proof of the
homogenization theorem, where the uniform-in-
Lestimates fora_Lare passed toaby lettingL → ∞.
1. Ellipticity of the two coefficient families on the cube #
The normalized cutoff field is elliptic on y + □_n, with lower constant the
molecular diffusivity: its symmetric part is ν I and its skew part is
continuous, so compactness of the closed cube supplies the upper constant.
The full stream coefficient is elliptic on y + □_n, with the same lower
constant.
2. The constant skew shift does not change the Dirichlet problem #
The weak equation of the cutoff field and of its origin normalization are the same equation.
The constant skew shift is invisible to the Dirichlet problem. This is
the printed remark that the equation for a_L is unchanged when a_L is
replaced by a_L minus a constant skew matrix.
3. The energy estimate with the explicit geometric distance #
Continuity of the solution map in the coefficient, along the cutoff
family. For the same forcing field g, the gradient of the cutoff solution
u_L differs from that of the full-field solution u by at most
ν⁻¹ d² · gap(L) · ‖∇u‖_{L²}, with gap(L) = Field.cutoffLimitGap the explicit
geometric coefficient distance.
4. From the gradients to the values #
Two solutions of Dirichlet problems with the same forcing field differ by a zero-trace function.
The L² distance of two solutions with the same forcing field is
controlled by the L² distance of their gradients, through the zero-trace
Poincaré inequality on the cube. The constant depends only on the cube.
5. L² convergence of the cutoff solutions #
The L² bound on the distance between the cutoff solution and the
full-field solution, uniform in L up to the explicit geometric factor.
u_L → u in L²(y + □_n). The forcing field is the same at every
scale; only the coefficient field moves.