OscillationFamily #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The truncated-window oscillation family at triadic lattice centres #
This module assembles, below the frozen surface, the two-parameter oscillation
estimate of [ABK] e.oscillation.Holder.bound for the zero-boundary-datum
Dirichlet problem of the cutoff field on the cube □_m.
For a scale m, a truncation index L ≥ m, a bottom scale n admissible for
the minimal scale X and a lattice centre z = 3 ^ n v ∈ 3 ^ n ℤ^d ∩ □_m, the
family is stated on the truncated windows U_j = (z + □_j) ∩ □_m and reads, for
every n ≤ n' ≤ m' ≤ m,
3 ^ (-n') ‖u - (u)_{U_{n'}}‖_{L²(U_{n'})}
≤ Cosc · 3 ^ ((1/2)(1-α)(m-n))
( 3 ^ (-m') ‖u - (u)_{U_{m'}}‖_{L²(U_{m'})}
+ Cdata · σ_m⁻¹ 3 ^ (m/2) K_g ) ,
with K_g a C^{0,1/2} seminorm bound for the force on □_m. The exponent
1/2 is the source's β. There is no boundary-datum leg: at zero datum the
∇h term of the source's δ_j budget vanishes identically.
The minimal scale is the one the excess-decay chain builds, X = Z + k + 3 at
the Step-1 parameters, and it is returned with the same measurability and the
same exponential tail that the regularity theorem of Section 4 carries, so a
consumer may read the tail from either.
Main definitions #
oscillationDataConst— the model-free amplitude of the force leg.
Main results #
oscillationHolderBound_zeroDatum— the family, almost surely, at every truncation index, every admissible bottom scale, every lattice centre of the cube, and every intermediate pair of scales.
References #
- [ABK],
ss.proof.regularitySteps 4--6, displaye.oscillation.Holder.bound.
1. The zero boundary datum #
The zero element of H¹ has the zero value field.
At the zero datum every Hölder seminorm bound holds with constant 0.
At the zero datum the pointwise gradient cap holds with constant 0.
The zero datum is classically differentiable with the zero gradient field.
2. The amplitude of the force leg #
The model-free amplitude of the force leg. The Step-5 budget's weight
4 C_δ / (1 - 3 ^ (-(1/2 - γ))) is enlarged to the γ-free
4 C_δ / (1 - 3 ^ (-1/4)) and multiplied by the Step-4 Gagliardo constant that
converts the printed C^{0,1/2} seminorm of the force into the fractional
seminorm the excess-decay lane reads.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The force leg, in the gauge the source prints. The excess-decay lane's
own data leg is at most the amplitude times σ_m⁻¹ 3 ^ (m/2) K_g.
3. The oscillation family #
[ABK] e.oscillation.Holder.bound at zero boundary datum.
For a disorder model of strength gamma small enough and every Hölder exponent
alpha below 1 - C sqrt gamma, and for every scale m, there is a minimal
scale X -- measurable, with the exponential tail of the regularity theorem --
such that, almost surely, for every truncation index L ≥ m, every bottom scale
n ≤ m admissible for X, every lattice centre z = 3 ^ n v of the cube, every
zero-datum Dirichlet solution u on □_m with force g of C^{0,1/2}
seminorm at most K_g, and every pair of scales n ≤ n' ≤ m' ≤ m, the
normalized oscillation on the truncated window U_{n'} = (z + □_{n'}) ∩ □_m is
bounded by 3 ^ ((1/2)(1-alpha)(m-n)) times the oscillation on U_{m'} plus
the force leg σ_m⁻¹ 3 ^ (m/2) K_g.
The exponent 1/2 is the source's β; the boundary-datum leg of the source's
display vanishes at zero datum.