SolutionScaling #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Homogeneity of the localized regularity #
The localized regularity X(y+□_n) is a supremum over the normalized forcing
class [g]_{C^{0,1/2}(y+□_n)} ≤ 3^{-n/2}, so by itself it says nothing about a
solution whose datum is not normalized. The localized Dirichlet problem is
homogeneous of degree one in the pair (solution, datum), so a datum with a
finite Hölder seminorm is brought into the class by the scalar factor
3^{-n/2} [g]^{-1}, and the bound for the normalized datum transfers with the
reciprocal factor.
This module proves that homogeneity and the resulting general bound.
Main results #
holderSeminormOn_const_smul— the Hölder seminorm is homogeneous.isDirichletSolutionAt_const_smul,isCubeRepresentative_const_smul— the problem and its continuous representatives are homogeneous.isDivFormWeakSolutionOn_congr_ae,isDirichletSolutionAt_congr_eqOn— the weak equation only sees the forcing field on the cube, up to a null set.localizedRegularity_apply_general— the bound for an arbitrary datum of finite Hölder seminorm.holderSeminormOn_le_localizedRegularity— the same, evaluated at a named continuous representative.exists_isCubeRepresentative_of_localizedRegularity_ne_top— a finite localized regularity produces a continuous representative of every solution with a datum of finite Hölder seminorm.
References #
- ABK26, the localized regularity of Section 5.1 and its use in the iteration of Proposition 5.1.
1. The Hölder seminorm is homogeneous #
The Hölder seminorm scales. For a nonnegative factor the seminorm of
t f is t times the seminorm of f, the identity holding in ℝ≥0∞ also when
the seminorm is infinite and when t = 0.
The scalar case of the previous statement, in multiplicative notation.
The Hölder seminorm of the zero field vanishes.
2. The localized Dirichlet problem is homogeneous #
Representatives scale.
The localized Dirichlet problem is homogeneous of degree one.
3. The equation only sees the forcing field on the cube #
The weak equation is insensitive to a null set of the forcing field.
The Dirichlet problem is insensitive to a null set of the forcing field.
The Dirichlet problem only sees the forcing field on the cube.
The zero function solves the homogeneous problem.
4. A datum of vanishing Hölder seminorm forces a vanishing solution #
A datum constant on the cube produces the zero solution. A vanishing
Hölder seminorm on y + □_n says exactly that the forcing field is constant
there, and a constant field pairs to zero against every zero-trace gradient, so
the solution is almost everywhere zero and the zero function is one of its
continuous representatives.
5. The infimum over representatives scales #
The infimum defining the localized regularity scales. Multiplying the
solution by a positive factor multiplies the infimum by the same factor,
including when no continuous representative exists and the infimum is ⊤.
6. The general bound #
The inner infimum of the localized regularity is bounded by it, for every normalized datum and every solution.
The localized regularity bounds every solution, normalized or not.
For a datum g of finite 1/2-Hölder seminorm on y + □_n and any solution
u of the rough-field problem with that datum,
σ_n 3^{-n/2} [u]_{C^{0,1/2}(y+□_n)}
≤ X(y+□_n) · 3^{n/2} [g]_{C^{0,1/2}(y+□_n)} ,
the left side being the infimum over continuous representatives that the
localized regularity is built from. The proof is the homogeneity of the
problem: the datum 3^{-n/2}[g]^{-1} g is normalized and the solution scales
with it.
The general bound, read at a named continuous representative.
A finite localized regularity produces a continuous representative. The
infimum defining the localized regularity is ⊤ when the solution has no
continuous representative, so a finite value forces one to exist for every datum
of finite Hölder seminorm.