DivergenceContraction

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

The divergence of a matrix field is a contraction of its gradient

The perturbation step of the injection estimate feeds the field ∇ · (k_m - k_n) into a Leibniz rule, while the size bounds available on the large-scale event are bounds on the full gradient ∇(k_m - k_n). The two are related by an algebraic contraction: if k is differentiable at x with derivative D, then

  (∇ · k)_j (x) = ∑_i (D e_i)_{i j} ,

a linear function of D whose ambient norm is at most d ‖D‖. Since the contraction is linear, the same factor d transfers a two-point bound on the gradient into a two-point bound on the divergence, so the 1/2-Hölder gauge of the divergence is at most d times that of the gradient.

The second half of the file specializes both bounds to the stream increment k_m - k_n on the cube y + □_n, where the gradient bounds are those of ShellPerturbation.lean, and records the two structural facts about the increment that the iteration step consumes: its entries are C¹ and its values are antisymmetric.

Main results

• norm_matFieldDiv_le — ‖(∇ · k)(x)‖ ≤ d ‖D‖.
• norm_matFieldDiv_sub_le — the same factor on a difference of two points.
• norm_matFieldDiv_cutoff_sub_le, holderSeminormBoundOn_matFieldDiv_cutoff_sub — the two sizes of ∇ · (k_m - k_n) on y + □_n, uniform in m.
• contDiff_one_cutoff_sub_entry, matTranspose_cutoff_sub — the regularity and the antisymmetry of k_m - k_n.

References

• ABK26, the perturbation step of the injection estimate of Section 5.1.

1. The contraction and its size

noncomputable def Algsuperdiff.Section5.Provider.matEntryCLM (d : ℕ) (i j : Fin d) : HCPolySupport.Mat d →L[ℝ] ℝ

Evaluation of one entry of a matrix, as a continuous linear map.

Equations

• Algsuperdiff.Section5.Provider.matEntryCLM d i j = LinearMap.toContinuousLinearMap (Matrix.entryLinearMap ℝ ℝ i j)

theorem Algsuperdiff.Section5.Provider.matFieldDiv_eq_sum_apply {d : ℕ} {k : HCPolySupport.Vec d → HCPolySupport.Mat d} {D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d} {x : HCPolySupport.Vec d} (hk : HasFDerivAt k D x) : Support.matFieldDiv k x = fun (j : Fin d) => ∑ i : Fin d, D (HCPolySupport.basisVec i) i j

The divergence at a point is the contraction of the derivative.

theorem Algsuperdiff.Section5.Provider.norm_matFieldDiv_le {d : ℕ} {k : HCPolySupport.Vec d → HCPolySupport.Mat d} {D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d} {x : HCPolySupport.Vec d} (hk : HasFDerivAt k D x) : ‖Support.matFieldDiv k x‖ ≤ ↑d * ‖D‖

The divergence of a matrix field is at most d times its gradient.

theorem Algsuperdiff.Section5.Provider.norm_matFieldDiv_sub_le {d : ℕ} {k : HCPolySupport.Vec d → HCPolySupport.Mat d} {Dx Dz : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d} {x z : HCPolySupport.Vec d} (hx : HasFDerivAt k Dx x) (hz : HasFDerivAt k Dz z) : ‖Support.matFieldDiv k x - Support.matFieldDiv k z‖ ≤ ↑d * ‖Dx - Dz‖

The two-point form. The contraction is linear, so a two-point bound on the gradient becomes a two-point bound on the divergence at the same cost d.

2. The stream increment on the cube

theorem Algsuperdiff.Section5.Provider.norm_matFieldDiv_cutoff_sub_le {d : ℕ} {M : Section3.ABKModel d} {n m : ℤ} {y : HCPolySupport.Vec d} {theta : ℝ} {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Support.largeScaleEvent M n y theta) (htheta : 0 ≤ theta) (hnm : n ≤ m) {x : HCPolySupport.Vec d} (hx : x ∈ Support.cubeSetAt y n) : ‖Support.matFieldDiv (fun (z : HCPolySupport.Vec d) => (Section3.Cutoff.cutoff m omega).toFun z - (Section3.Cutoff.cutoff n omega).toFun z) x‖ ≤ ↑d * (√↑d * (theta * Real.rpow 3 ((M.gamma - 1) * ↑n)))

The supremum size of ∇ · (k_m - k_n) on y + □_n, uniform in m.

theorem Algsuperdiff.Section5.Provider.holderSeminormBoundOn_matFieldDiv_cutoff_sub {d : ℕ} {M : Section3.ABKModel d} {n m : ℤ} {y : HCPolySupport.Vec d} {theta : ℝ} {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Support.largeScaleEvent M n y theta) (htheta : 0 ≤ theta) (hnm : n ≤ m) : Section4.Support.HolderSeminormBoundOn (Support.cubeSetAt y n) (1 / 2) (↑d * (√2 * (↑d * (theta * Real.rpow 3 ((M.gamma - 3 / 2) * ↑n))))) (Support.matFieldDiv fun (z : HCPolySupport.Vec d) => (Section3.Cutoff.cutoff m omega).toFun z - (Section3.Cutoff.cutoff n omega).toFun z)

The 1/2-Hölder size of ∇ · (k_m - k_n) on y + □_n, uniform in m.

3. Regularity and antisymmetry of the perturbation field

theorem Algsuperdiff.Section5.Provider.contDiff_one_cutoff_sub_entry {d : ℕ} (omega : Section3.Cutoff.CutoffSample d) {n m : ℤ} (hnm : n ≤ m) (p q : Fin d) : ContDiff ℝ 1 fun (x : HCPolySupport.Vec d) => ((Section3.Cutoff.cutoff m omega).toFun x - (Section3.Cutoff.cutoff n omega).toFun x) p q

The entries of k_m - k_n are continuously differentiable.

theorem Algsuperdiff.Section5.Provider.matTranspose_cutoff_sub {d : ℕ} (omega : Section3.Cutoff.CutoffSample d) {n m : ℤ} (hnm : n ≤ m) (x : HCPolySupport.Vec d) : HCPolySupport.matTranspose ((Section3.Cutoff.cutoff m omega).toFun x - (Section3.Cutoff.cutoff n omega).toFun x) = -((Section3.Cutoff.cutoff m omega).toFun x - (Section3.Cutoff.cutoff n omega).toFun x)

The values of k_m - k_n are antisymmetric.