Translation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Transporting the Section 5 objects between y + □_n and □_n #
Every Section 5 object attached to the cube y + □_n is realized by moving the
sample, never the cube: the coefficient field satisfies
a_m(x, τ_y ω) = a_m(x + y, ω) exactly, the Dirichlet problem on y + □_n
becomes the Dirichlet problem on □_n for the pulled-back data, and the two
gauges of HolderGauge.lean are invariant under the same change of variables.
This module supplies those transports and the resulting statement of the
large-scale event 𝒥(y + □_n, θ) as a translate preimage.
Main definitions #
IsDirichletSolutionAt a y n u g— the zero-boundary weak solution of-∇·a∇u = ∇·gony + □_n.originPullback y n u— the same solution read on□_n,x ↦ u(x + y).largeScaleEventBase M n θ,largeScaleEvent M n y θ— the eventΣ_{k ≥ n} 3^{(2-γ)n} ‖∇ j_k‖_{W^{1,∞}(□_n)} ≤ θat the origin, and its translate toy + □_n. The weight is fixed at the cube scalen, as in the first condition of the Section 4 good event𝒢₁(m; s, T)on□_m.
References #
- ABK26, the localized Dirichlet problems and the large-scale good event of Section 5.1.
1. Transporting a Sobolev witness along an equality of domains #
cubeSetAt y n is the image of □_n under x ↦ y + x, and the ambient Sobolev
transport API is stated for translateSet. The two sets are equal but not
definitionally so, so the witnesses are moved along the equality.
Transport an H¹ witness along an equality of its domain.
Equations
- Algsuperdiff.Section5.Support.castH1 h u = h ▸ u
Instances For
Transport an H¹₀ witness along an equality of its domain.
Equations
- Algsuperdiff.Section5.Support.castH10 h u = h ▸ u
Instances For
The Dirichlet problem on y + □_n: u agrees with a zero-trace witness
and solves -∇·a∇u = ∇·g weakly on y + □_n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The solution on y + □_n, read on □_n as x ↦ u(x + y).
Equations
Instances For
The change of variables in the weak equation #
The weak equation transports exactly. The test functions on the two
domains correspond bijectively under H10Function.translate and
H10Function.untranslate, and the change of variables is measure preserving.
The zero boundary condition transports exactly.
The origin-cube reading of the Dirichlet problem on y + □_n.
3. The two gauges transport #
4. The coefficient covariance #
The cutoff coefficient of the translated sample is the coefficient field
recentred at y, in the form the origin-cube reading of the Dirichlet problem
consumes.
5. The large-scale event 𝒥 #
The large-scale event at the origin: the tail sum
Σ_{k ≥ n} 3^{(2-γ)n} ‖∇ j_k‖_{W^{1,∞}(□_n)} does not exceed θ.
The weight 3^{(2-γ)n} is fixed at the cube scale n and does not run with the
summation index k. This is the shape of the first condition of the Section 4
good event 𝒢₁(m; s, T), whose weight 3^{(2-γ)m} is likewise fixed at the
cube scale, and it is the shape the size of the summand demands: the increment
j_k obeys j_k ≃ 3^{γk} j_0(3^{-k} ·), so
‖∇ j_k‖_{W^{1,∞}(□_n)} ≃ max(3^{(γ-2)k}, 3^{-n} 3^{(γ-1)k}) and the k-th
term of the fixed-weight series is of order 3^{-(1-γ)(k-n)}. The series is
then geometric for γ < 1, and the event has positive measure at every
threshold θ above the typical value of the sum. A weight 3^{(2-γ)k} running
with k would instead make the k-th term of order max(1, 3^{k-n}), the
series divergent almost surely, and the event a null set at every finite θ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The large-scale event on y + □_n, realized by translating the sample.