HomogenizationCorrectorPointwise #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The cut-off observables of the displacement bounds, with their pointwise corrector bounds #
The stopped-moment bounds on a triadic cube consume an observable together with a bound, at
every point, on its distance to a bounded Borel function vanishing at the centre. This file
produces, for the cut-off linear and quadratic data c · (e ⬝ x) and c · (e ⬝ x)² of a smooth
cut-off c equal to one on the cube centred at the origin, the homogenization observable of the
cube with all its properties, and the pointwise corrector bounds:
- for the linear datum,
|c (e ⬝ x) − u| ≤ 3^m EB ‖e‖everywhere — on the cube by the corrector estimate read through the continuous representative, off the cube because the observable is the datum there; - for the quadratic datum, the same for the corrected observable
u − 2 sigmaBar (e ⬝ e) w, withwthe expected exit time from the cube, at every point of the compactified state space — on the cube by the corrector estimate at the forcing-2 sigmaBar (e ⬝ x) e, off the cube because the expected exit time vanishes there, and at infinity because everything vanishes.
The corrected observable solves the forced Dirichlet problem because the expected exit time is
the zero-trace solution of -∇ · a ∇w = 1, and the divergence of (e ⬝ x) e is e ⬝ e.
Main results #
isDivFormWeakSolutionOn_quadraticForcing_of_streamExitH10— the corrected observable solves the quadratic problem.exists_cutoffAffineObservable_stream— the observable of the cut-off linear datum with its pointwise corrector bound.exists_cutoffQuadraticObservable_stream— the observable of the cut-off quadratic datum with the pointwise bound on the corrected observable.
References #
- ABK26, Steps 1 and 3 of the superdiffusive displacement bounds of Section 5.4.
1. The corrected observable solves the quadratic problem #
The divergence of the field x ↦ (e ⬝ x) e is e ⬝ e.
The coordinates of the field x ↦ (e ⬝ x) e are smooth.
The corrected observable solves the quadratic problem. If u = h + w solves the
homogeneous equation on the cube with the trace of the quadratic datum, then
u − 2 sigmaBar (e ⬝ e) E, with E the zero-trace solution of -∇ · a ∇E = 1, solves the
problem with the forcing -2 sigmaBar (e ⬝ x) e.
2. The cut-off linear datum #
The observable of the cut-off linear datum, with its pointwise corrector bound. For a
smooth cut-off c equal to one on the cube centred at the origin and a uniform bound N for
c · (e ⬝ x), there is a homogenization observable of the cube with datum c · (e ⬝ x), and it
is everywhere within 3^m EB ‖e‖ of the datum, under the corrector clause of the
renormalization theorem at the sample for the scale m.
3. The cut-off quadratic datum #
The observable of the cut-off quadratic datum, with the pointwise bound on the corrected
observable. For a smooth cut-off c equal to one on the cube centred at the origin and a
uniform bound N for c · (e ⬝ x)², there is a homogenization observable u of the cube with
datum c · (e ⬝ x)², and at every point of the compactified state space the datum is within
5 (3^m)² EB ‖e‖ (∑ |e_i|) of u − 2 sigmaBar (e ⬝ e) times the expected exit time from the
cube, under the corrector clause of the renormalization theorem at the sample for the scale
m.