Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.ExcessDecay.NegNormToL2

NegNormToL2 #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The negative-norm-to-L² step: the L² distance from the negative fractional norm #

ABK26's Step 1 closes with the two-step chain

  ‖u - v‖_{L²(x+□_n)} ≤ C ‖∇u - ∇v‖_{H_hat^{-1}(x+□_n)}
                       ≤ C 3^{(1 - s/2)n} ‖∇u - ∇v‖_{H_hat^{-s/2}(x+□_n)} ,

for u - v ∈ H¹₀(x+□_n), whose second inequality the graph records as an unexplained "Besov-scale comparison on a cube of side 3^n".

Finding: CoarseGraining proves the whole chain in one theorem, and the printed scale factor comes out exactly. The theorem is

  cubeBesovScaleWeight 1 Q · ‖u‖_{L²(Q)}
      ≤ C(d) · sqrt((1 - 3^{-2(1/2 - t)})⁻¹) · [∇u]_{B^{-2t}_{2,2}(Q)}

(Homogenization.Book.Ch03.cubeBesovScaleWeight_one_mul_cubeLpNorm_h10_le_grad_ negativeBesovTwo, for u ∈ H¹₀(cubeSet Q) and 0 < t < 1/2). Since cubeBesovScaleWeight 1 Q = 3^{-Q.scale} and CoarseGraining's negative seminorm carries the manuscript's own outer normalization 3^{-σ·scale}, the conclusion reads

  ‖u‖_{L²(□_n)} ≤ C(d) 3^{n} · 3^{-2tn} [∇u]_{H_hat^{-2t}(□_n)}
                = C(d) 3^{(1-2t)n} [∇u]_{H_hat^{-2t}(□_n)} ,

No separate H_hat^{-1} ← H_hat^{-s/2} comparison is needed: the two printed inequalities are one theorem.

This module contributes the two bounded pieces:

The norm on the right is the manuscript's own substitute (recorded) #

CoarseGraining's right-hand object is the concrete block-average negative seminorm B^{-σ}_{2,2}, not the hatted H_hat^{-σ} the display prints. The manuscript itself performs exactly this substitution — records ‖·‖_{H_hat^{-s}(□)} ≤ C ‖·‖_{B^{-s}_{2,2}(□)} ≤ C ‖·‖_{B^{-s}_{2,1}(□)} — so the inequality below is the printed one with the printed norm replaced by the dominating one, i.e. a weaker statement per step. The composition with the coarse-graining leg must therefore be made at the B^{-σ}_{2,2} level, which is also the level at which CoarseGraining's coarse-graining machinery produces its bounds. Nothing here claims the hatted norm.

What is still missing (disclosed frontier) #

The frozen theorem's left-hand side is eLpNorm (u - v) 2 (normalizedVolumeMeasureOn ((x + □_n) image)), on an off-grid window, while CoarseGraining's theorem is stated at a triadic cube in the cubeSet/cubeLpNorm carriers. Two bridges therefore remain, neither of them attempted here: the normalizedVolumeMeasureOn-vs-normalizedCubeMeasure identification on the open/closed cube pair, and the A4 frame change (this leg lives naturally in the frame translated by x, while the energy leg lives in the frame translated by z).

References #

1. The analytic factor at t = s/4 #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.negNormSqrtFactor_le_two {s : ℝ} (hs1 : s ≤ 1) :
√(1 - Real.rpow 3 (-2 * (1 / 2 - s / 4)))⁻¹ ≤ 2

The Besov-tail factor is bounded by 2 on the anchor's s-range.

2. The negative-norm step at the parameter choice t = s/4 #

source
noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.negNormBaseConst (d : ℕ) :
ℝ

The dimensional constant of CoarseGraining's zero-trace value estimate.

Equations
Instances For
    source
    theorem Algsuperdiff.Section4.Provider.ExcessDecay.negNormBaseConst_pos (d : ℕ) :
    0 < negNormBaseConst d
    source
    theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeLpNorm_h10_le_negativeBesov_quarter {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H10Function (HCPolySupport.cubeSet Q)) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) :
    (HCPolySupport.cubeBesovScaleWeight 1 Q * HCPolySupport.cubeLpNorm Q 2 fun (x : HCPolySupport.Vec d) => u.toFun x) ≤ 2 * negNormBaseConst d * HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q (s / 2) fun (x : HCPolySupport.Vec d) => u.grad x

    The negative-norm-to-L² step at t = s/4.

      3^{-Q.scale} ‖u‖_{L²(Q)} ≤ 2 C(d) [∇u]_{B^{-s/2}_{2,2}(Q)}      (u ∈ H¹₀(Q)) .

    This is the printed two-step chain, in one inequality, at the negative index s/2 and with the analytic tail factor discharged by negNormSqrtFactor_le_two. Nonnegativity of the right-hand seminorm is derived from the inequality itself (the left side is nonnegative and the constant is positive), so no BddAbove hypothesis is imposed.