ShellNorms #

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

Section 4 volume-normalized shell Sobolev gauges #

ABK26's Section 4 good events (d.good.event.for.lambda) and the annular decomposition (p.mathcalE.annular.decomp) weigh the stream increments j_k in the manuscript's volume-normalized Sobolev norms ‖∇j‖_{W^{1,∞}(□_m)} and ‖j‖_{W^{2,∞}(z+□_k)}.

The manuscript defines, for |U| < ∞,

  ‖f‖_{W^{1,p}(U)} = ( ‖∇f‖_{L^p(U)}^p + |U|^{-p/d} ‖f‖_{L^p(U)}^p )^{1/p} ,

and the k-th order analogue adds one term per derivative order with the matching power of |U|^{-1/d}. At the endpoint p = ∞ the ℓ^p combination is the maximum and the normalized L^∞ norm is the plain L^∞ norm, so on the triadic cube □_m (where |□_m|^{-1/d} = 3^{-m}) the two gauges used by Section 4 are

  ‖∇j‖_{W^{1,∞}(□_m)}   = max ( ‖∇²j‖_{L^∞(□_m)} , 3^{-m} ‖∇j‖_{L^∞(□_m)} ) ,
  ‖j‖_{W^{2,∞}(z+□_k)}  = max ( ‖∇²j‖_{L^∞(z+□_k)} ,
                                 3^{-k}  ‖∇j‖_{L^∞(z+□_k)} ,
                                 3^{-2k} ‖j‖_{L^∞(z+□_k)} ) .

Both are realized on the proved shell carriers: the origin-cube L^∞ gauges are Algsuperdiff.Section3.Cutoff.localCubeControl (order 0) and Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm / localCubeSecondDerivNorm (orders 1 and 2), and the translated cube z + □_k is realized by the frozen ShellField.translate action (translate z j = j (· + z)), for which the exact supremum over z + □_k of a derivative of j is the supremum over □_k of the same derivative of translate z j. No new supremum, no fallback branch and no chosen representative is introduced.

Main definitions #

shellW1InfGradNorm m j — the tex ‖∇j‖_{W^{1,∞}(□_m)}.
shellW2InfNormAt z k j — the tex ‖j‖_{W^{2,∞}(z+□_k)}.

References #

ABK26, (the normalized Sobolev norms).
ABK26, d.good.event.for.lambda, and p.mathcalE.annular.decomp.

The first-order gauge on the origin cube #

source

noncomputable def Algsuperdiff.Section4.Support.shellW1InfGradNorm {d : ℕ} (m : ℤ) (j : Frozen.Assumptions.ShellField d) :

ℝ

The manuscript's ‖∇j‖_{W^{1,∞}(□_m)}: the p = ∞ endpoint of the volume-normalized W^{1,p} norm, applied to f = ∇j on the origin cube □_m, where |□_m|^{-1/d} = 3^{-m}.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Algsuperdiff.Section4.Support.shellW1InfGradNorm_def {d : ℕ} (m : ℤ) (j : Frozen.Assumptions.ShellField d) :

shellW1InfGradNorm m j = max (Section3.Provider.Stream.localCubeSecondDerivNorm m j) (3 ^ (-m) * Section3.Provider.Stream.localCubeDerivNorm m j)

source

theorem Algsuperdiff.Section4.Support.shellW1InfGradNorm_nonneg {d : ℕ} (m : ℤ) (j : Frozen.Assumptions.ShellField d) :

0 ≤ shellW1InfGradNorm m j

source

theorem Algsuperdiff.Section4.Support.measurable_shellW1InfGradNorm {d : ℕ} (m : ℤ) :

Measurable (shellW1InfGradNorm m)

source

theorem Algsuperdiff.Section4.Support.localCubeSecondDerivNorm_le_shellW1InfGradNorm {d : ℕ} (m : ℤ) (j : Frozen.Assumptions.ShellField d) :

Section3.Provider.Stream.localCubeSecondDerivNorm m j ≤ shellW1InfGradNorm m j

The second-derivative leg is dominated by the gauge.

source

theorem Algsuperdiff.Section4.Support.three_zpow_mul_localCubeDerivNorm_le_shellW1InfGradNorm {d : ℕ} (m : ℤ) (j : Frozen.Assumptions.ShellField d) :

3 ^ (-m) * Section3.Provider.Stream.localCubeDerivNorm m j ≤ shellW1InfGradNorm m j

The normalized first-derivative leg is dominated by the gauge.

The second-order gauge on a translated cube #

source

noncomputable def Algsuperdiff.Section4.Support.shellW2InfNormAt {d : ℕ} (z : HCPolySupport.Vec d) (k : ℤ) (j : Frozen.Assumptions.ShellField d) :

ℝ

The manuscript's ‖j‖_{W^{2,∞}(z+□_k)}: the p = ∞ endpoint of the volume-normalized second-order Sobolev norm on the translated cube z + □_k, where |z+□_k|^{-1/d} = 3^{-k}.

The translated cube is realized by the frozen translation action: ShellField.translate z j = j (· + z) carries the supremum over z + □_k of any derivative of j to the supremum over □_k of the same derivative of translate z j, which is exactly what the proved origin-cube gauges compute.

Equations