LocalizedFinite #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The normalized forcing class, the localized quantities, and the good cube event #
Section 5.1 attaches to each cube y + □_n two quantities: the localized error
E, comparing the rough-field solution with the comparator in the L^∞ norm,
and the localized regularity X, the normalized 1/2-Hölder seminorm of the
rough-field solution. Both are suprema over the normalized forcing class
[g]_{W^{1/2,∞}(y+□_n)} ≤ 1.
The two quantities read a solution differently, and the difference is the
source's. The L^∞ norm is an essential supremum: it is insensitive to a null
set, so it is taken of the H¹ functions themselves, with no representative and
no side condition that could drop a datum. The 1/2-Hölder seminorm is a
pointwise quantity, so it is taken of a continuous representative; the
representative is quantified by an infimum, which is the seminorm of the
unique continuous representative where one exists and ⊤ where none does. A
solution too rough to have a continuous representative therefore makes X
infinite instead of contributing nothing.
The values are ℝ≥0∞, so an unbounded family has the value ⊤ rather than
collapsing.
Main definitions #
NormalizedForceAt y n g— the normalization[g]_{W^{1/2,∞}(y+□_n)} ≤ 1.IsCubeRepresentative y n u uRep—uRepis a representative ofucontinuous ony + □_n.localizedError,localizedRegularity— the two quantities.goodCubeEvent—{E ≤ ε} ∩ {X ≤ 2 Creg}.
References #
- ABK26, the localized error and regularity quantities and the good cube event of Section 5.1.
1. The normalized forcing class #
The normalized forcing class of y + □_n: the explicit two-point form of
[g]_{W^{1/2,∞}(y+□_n)} ≤ 1.
Equations
- Algsuperdiff.Section5.Support.NormalizedForceAt y n g = Algsuperdiff.Section4.Support.HolderSeminormBoundOn (Algsuperdiff.Section5.Support.cubeSetAt y n) (1 / 2) (Real.rpow 3 (-↑n / 2)) g
Instances For
2. Continuous representatives as an explicit witness #
uRep is a representative of u continuous on y + □_n. Finiteness of
its 1/2-Hölder seminorm is deliberately not required: the source takes that
seminorm of the continuous representative, and an infinite value there is a
value of the localized regularity, not a reason to drop the datum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Representatives of almost-everywhere equal solutions agree everywhere on the cube. With the almost-everywhere uniqueness of the localized Dirichlet problem this makes every pointwise quantity below independent of the choice of solution and of representative.
3. The two localized quantities #
Continuous representatives on the open cube are unique. Two
representatives of the same H¹ witness agree at every point of the cube.
The infimum over the continuous representatives of a witness is the value
at any one of them. By uniqueness the family is a singleton where it is
nonempty, so the infimum records the seminorm of the continuous representative
where there is one and ⊤ where there is none.
The localized error E(y+□_n): the supremum, over the normalized forcing
class and over the solutions of the two problems, of
σ_n 3^{-n} ‖u_n - v‖_{L^∞(y+□_n)}.
The L^∞ norm is the essential supremum on the cube, of the H¹ functions
themselves. It does not see a null set, so it needs no representative and
carries no side condition; both inner families are nonempty by the solvability
of the two problems, and the value does not depend on which solutions are chosen
by their almost-everywhere uniqueness.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The localized regularity X(y+□_n): the supremum, over the normalized
forcing class and over the rough-field solutions, of
σ_n 3^{-n/2} [u_n]_{C^{0,1/2}(y+□_n)}, the seminorm being that of the
continuous representative.
The representative is quantified by an infimum: it is unique where it exists, so
the infimum is its seminorm there, and it is ⊤ where no continuous
representative exists.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The L^∞ norm of the difference of two witnesses is the supremum norm of
the difference of their continuous representatives. This is how the localized
error, an essential supremum, is read pointwise where representatives exist.
4. The good cube event #
The good cube event 𝒢(y+□_n, ε): the localized error does not exceed
ε and the localized regularity does not exceed 2 Creg.
Equations
- One or more equations did not get rendered due to their size.
Instances For
6. Uniform bounds on the normalized class #
A uniform supremum bound for the representatives of the comparator, over the whole normalized forcing class.
Equations
- One or more equations did not get rendered due to their size.