StreamForcingDeriv

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

Differentiability and derivative size of the fresh-shell forcing

The forcing of the two corrector problems e.def.w is streamForcing sigmaInv omega n m e = sigmaInv * (k_m - k_n) e (FreshShellL8). The nested-recentring display of OscillationNestedAssembly consumes a forcing G through exactly two properties:

• ∀ i, Differentiable ℝ (fun y => G y i), and
• ∀ x ∈ (the coarse cube), ∀ i, ‖fderiv ℝ (fun y => G y i) x‖ ≤ M.

This module supplies both at G = ± streamForcing, and converts the second one into the derivative gauges in which ABK26's e.W.1.inf.bound is stated.

Why differentiability is elementary here

Since the passage from the matrix A to the real number sigmaInv * (A e)_i is a continuous linear map of A, the forcing coordinate is a finite sum of compositions of continuous linear maps with differentiable maps.

The gauge conversion, with every factor visible

Two conversion factors meet here and neither is absorbed silently.

• The ambient carrier Vec d = Fin d -> ℝ is sup-normed, so the operator norm ‖fderiv ℝ (fun y => G y i) x‖ is measured against ‖v‖_∞. The shell derivative gauge ShellField.matrixDerivativeNorm is measured against the Euclidean length Book.Ch02.vecNorm v. Converting the input costs the factor sqrt d (vecNorm_le_sqrt_dim_mul_norm); it is written explicitly in every statement below.
• Converting the output costs nothing: the single coordinate |(A e)_i| ≤ ‖A e‖_∞ ≤ |A e|_2 (norm_le_vecNorm), so the factor is 1.

The net conversion is thus M = sigmaInv * sqrt d * |e|_2 * ∑_{k ∈ (n,m]} ‖∇j_k‖_{L∞(z + cu_ell)}, the last factor being the bare sum of local cube derivative gauges. Pricing that bare sum against the weighted summand 3^k ‖∇j_k‖_{L∞(cu_l)} + 3^{2k} ‖∇²j_k‖_{L∞(cu_l)} of e.W.1.inf.bound (Provider.Stream.largeCubeDerivGauge) costs a further factor 3^{-(n+1)}, the reciprocal of the smallest weight in the range; that step belongs to the consumer and is not taken here.

Contents

• differentiable_streamForcing_coord, differentiable_neg_streamForcing_coord -- coordinatewise differentiability of the forcing and of its negative.
• norm_fderiv_streamForcing_coord_le, norm_fderiv_neg_streamForcing_coord_le -- the pointwise differential bound in the exact induced shell-derivative gauge.
• matrixDerivativeNorm_sum_deriv_le_sum_localCubeDerivNorm_translate -- the same gauge read on a translated cube z + cu_ell.

References

• ABK26, e.def.w.
• ABK26, e.nablaw.oscillations, whose forcing term is the eventual consumer.
• ABK26, e.W.1.inf.bound.

The coordinate functional of the forcing

def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.streamForcingCoordLinear {d : ℕ} (sigmaInv : ℝ) (e : HCPolySupport.Vec d) (i : Fin d) : HCPolySupport.Mat d →ₗ[ℝ] ℝ

The map A ↦ sigmaInv * (A e)_i, which is linear in the matrix A.

Equations

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

def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.streamForcingCoordCLM {d : ℕ} (sigmaInv : ℝ) (e : HCPolySupport.Vec d) (i : Fin d) : HCPolySupport.Mat d →L[ℝ] ℝ

The same map as a continuous linear functional. The bound used to manufacture continuity is the crude entrywise one; the sharp bound is proved separately in norm_fderiv_streamForcing_coord_le.

Equations

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

(1) Coordinatewise differentiability of the forcing

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.differentiable_streamForcing_coord {d : ℕ} (sigmaInv : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (i : Fin d) : Differentiable ℝ fun (y : HCPolySupport.Vec d) => streamForcing sigmaInv omega n m e y i

Coordinatewise differentiability of the fresh-shell forcing. Each coordinate of sigmaInv (k_m - k_n) e is differentiable on all of Vec d.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.differentiable_neg_streamForcing_coord {d : ℕ} (sigmaInv : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (i : Fin d) : Differentiable ℝ fun (y : HCPolySupport.Vec d) => (-streamForcing sigmaInv omega n m e y) i

The same for the negated forcing, which is the sign convention in which the CoarseGraining weak-solution predicates state - Delta w = div f.

(2) The differential bound in the exact shell-derivative gauge

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.norm_fderiv_streamForcing_coord_le {d : ℕ} (sigmaInv : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (i : Fin d) (x : HCPolySupport.Vec d) : ‖fderiv ℝ (fun (y : HCPolySupport.Vec d) => streamForcing sigmaInv omega n m e y i) x‖ ≤ |sigmaInv| * √↑d * HCPolySupport.Book.Ch02.vecNorm e * Frozen.Assumptions.ShellField.matrixDerivativeNorm (∑ k ∈ Finset.Ioc n m, (omega k).deriv x)

The pointwise differential bound. At every point, the differential of each coordinate of the forcing is bounded, in the ambient sup-operator norm, by sigmaInv times sqrt d times the Euclidean length of e times the exact induced norm of the summed shell derivatives. The factor sqrt d is the sup-to-Euclidean conversion on the input of the differential; the output conversion is free.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.norm_fderiv_neg_streamForcing_coord_le {d : ℕ} (sigmaInv : ℝ) (omega : Cutoff.ShellSeq d) (n m : ℤ) (e : HCPolySupport.Vec d) (i : Fin d) (x : HCPolySupport.Vec d) : ‖fderiv ℝ (fun (y : HCPolySupport.Vec d) => (-streamForcing sigmaInv omega n m e y) i) x‖ ≤ |sigmaInv| * √↑d * HCPolySupport.Book.Ch02.vecNorm e * Frozen.Assumptions.ShellField.matrixDerivativeNorm (∑ k ∈ Finset.Ioc n m, (omega k).deriv x)

The same bound for the negated forcing: negation does not change the size of a differential.

The shell-derivative gauge on a translated cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.matrixDerivativeNorm_sum_deriv_le_sum_localCubeDerivNorm_translate {d : ℕ} (ell : ℤ) (s : Finset ℤ) (z : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) {y : HCPolySupport.Vec d} (hy : y ∈ HCPolySupport.Book.Ch03.openCubeAtScale z ell) : Frozen.Assumptions.ShellField.matrixDerivativeNorm (∑ k ∈ s, (omega k).deriv y) ≤ ∑ k ∈ s, Stream.localCubeDerivNorm ell (Frozen.Assumptions.ShellField.translate z (omega k))

‖∇(k_m - k_n)‖_{L∞(z + cu_ell)} in the exact induced gauge. On the translated cube z + cu_ell the derivative of a finite shell sum is dominated by the sum of the local cube derivative gauges of the translated shells, which is the carrier of ABK26's e.W.1.inf.bound at base point z.