ScaleDecompositionSmooth

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

Differentiability of the high-frequency stream field

The nonnegative shell series has locally summable first derivatives. Uniform convergence on every origin cube gives a continuous derivative, so its sum is genuinely C¹ rather than merely pointwise differentiable.

noncomputable def Algsuperdiff.Section5.Field.streamFieldLargeDeriv {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (x : HCPolySupport.Vec d) : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d

The termwise derivative of the nonnegative-shell part.

Equations

• Algsuperdiff.Section5.Field.streamFieldLargeDeriv omega x = ∑' (r : ℕ), (↑↑omega ↑r).deriv x

theorem Algsuperdiff.Section5.Field.streamFieldLarge_contDiff_one {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) : ContDiff ℝ 1 (streamFieldLarge omega)

The nonnegative-shell part of the stream field is continuously differentiable, with derivative streamFieldLargeDeriv.

theorem Algsuperdiff.Section5.Field.fderiv_streamFieldLarge {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (x : HCPolySupport.Vec d) : fderiv ℝ (streamFieldLarge omega) x = streamFieldLargeDeriv omega x

The Fréchet derivative of the nonnegative-shell part is its termwise derivative series.