ShellDerivativeControl

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

Derivative-level local cube controls for shell fields

Algsuperdiff.Section3.Cutoff.localCubeControl measures the exact value supremum ‖j‖_{L∞(cu_ell)} of a shell field on the open origin cube of scale ell. ABK26's stream estimates additionally need the two derivative suprema ‖∇j‖_{L∞(cu_ell)} and ‖∇²j‖_{L∞(cu_ell)}. This module supplies them in exactly the norms fixed by the frozen J2 observable (ShellField.unitCubeDerivNorm and ShellField.unitCubeSecondDerivNorm), together with their sharp characterizations, monotonicity in the cube scale, and the exact triadic scaling identities.

The two gauges are raw suprema: localCubeDerivNorm ell j is literally ‖∇j‖_{L∞(cu_ell)} and localCubeSecondDerivNorm ell j is literally ‖∇²j‖_{L∞(cu_ell)}, with no scale normalization folded in. The chain-rule factors of the frozen spatialScale action are divided out explicitly in the definitions. Consequently the amplitudes in the triadic scaling identities are the manuscript's 3^{(γ-1)k} and 3^{(γ-2)k} rather than 3^{γk}.

Note that cubeScaleFactor (originCube d ell) is by definition (3 : ℝ) ^ ell, so the definitions below use exactly the cube-scale convention of Algsuperdiff.Section3.Cutoff.localCubeControl.

Main definitions

• localCubeDerivNorm: ‖∇j‖_{L∞(cu_ell)}.
• localCubeSecondDerivNorm: ‖∇²j‖_{L∞(cu_ell)}.

Main results

• matrixDerivativeNorm_deriv_le_localCubeDerivNorm, localCubeDerivNorm_le_of_forall and their second-derivative analogues: each gauge is the least nonnegative pointwise bound on its open cube.
• localCubeDerivNorm_triadicScale, localCubeSecondDerivNorm_triadicScale: the exact scaling identities, mirroring Algsuperdiff.Section3.Cutoff.localCubeControl_triadicScale.

References

• ABK26, e.jk.O, e.nabla.jk.O.
• ABK26, e.kn.reg.ass.with.gamma.

Exact positive homogeneity of the J2 matrix norms

theorem Algsuperdiff.Section3.Provider.Stream.matrixDerivativeNorm_le_iff {d : ℕ} (D : Frozen.Assumptions.ShellField.MatrixDerivative d) (C : ℝ) : Frozen.Assumptions.ShellField.matrixDerivativeNorm D ≤ C ↔ 0 ≤ C ∧ ∀ (v : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm v ≤ 1 → HCPolySupport.Book.Ch02.matrixOperatorNorm (D v) ≤ C

Sharp characterization of the exact induced first-derivative norm: it is the least nonnegative bound on the Euclidean unit ball.

theorem Algsuperdiff.Section3.Provider.Stream.matrixDerivativeNorm_smul_of_nonneg {d : ℕ} {c : ℝ} (hc : 0 ≤ c) (D : Frozen.Assumptions.ShellField.MatrixDerivative d) : Frozen.Assumptions.ShellField.matrixDerivativeNorm (c • D) = c * Frozen.Assumptions.ShellField.matrixDerivativeNorm D

The exact induced first-derivative norm is positively homogeneous.

theorem Algsuperdiff.Section3.Provider.Stream.matrixSecondDerivativeNorm_smul_of_nonneg {d : ℕ} {c : ℝ} (hc : 0 ≤ c) (H : Frozen.Assumptions.ShellField.MatrixSecondDerivative d) : Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm (c • H) = c * Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm H

The exact twice-induced second-derivative norm is positively homogeneous.

The open-unit-cube supremum toolkit

theorem Algsuperdiff.Section3.Provider.Stream.matrixDerivativeNorm_deriv_le_unitCubeDerivNorm {d : ℕ} (j : Frozen.Assumptions.ShellField d) {y : HCPolySupport.Vec d} (hy : y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0)) : Frozen.Assumptions.ShellField.matrixDerivativeNorm (j.deriv y) ≤ j.unitCubeDerivNorm

The J2 first-derivative unit-cube norm dominates the exact induced derivative norm at every point of the literal open unit cube.

theorem Algsuperdiff.Section3.Provider.Stream.unitCubeDerivNorm_le_iff {d : ℕ} (j : Frozen.Assumptions.ShellField d) (C : ℝ) : j.unitCubeDerivNorm ≤ C ↔ 0 ≤ C ∧ ∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0), Frozen.Assumptions.ShellField.matrixDerivativeNorm (j.deriv y) ≤ C

Sharp characterization of the J2 first-derivative unit-cube norm.

theorem Algsuperdiff.Section3.Provider.Stream.matrixSecondDerivativeNorm_secondDeriv_le_unitCubeSecondDerivNorm {d : ℕ} (j : Frozen.Assumptions.ShellField d) {y : HCPolySupport.Vec d} (hy : y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0)) : Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm (j.secondDeriv y) ≤ j.unitCubeSecondDerivNorm

The J2 second-derivative unit-cube norm dominates the exact twice-induced derivative norm at every point of the literal open unit cube.

theorem Algsuperdiff.Section3.Provider.Stream.unitCubeSecondDerivNorm_le_iff' {d : ℕ} (j : Frozen.Assumptions.ShellField d) (C : ℝ) : j.unitCubeSecondDerivNorm ≤ C ↔ 0 ≤ C ∧ ∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d 0), Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm (j.secondDeriv y) ≤ C

Sharp characterization of the J2 second-derivative unit-cube norm, stated on unbundled cube points.

Amplitude scaling of the unit-cube derivative norms

theorem Algsuperdiff.Section3.Provider.Stream.unitCubeDerivNorm_scale_of_nonneg {d : ℕ} {c : ℝ} (hc : 0 ≤ c) (j : Frozen.Assumptions.ShellField d) : (Frozen.Assumptions.ShellField.scale c j).unitCubeDerivNorm = c * j.unitCubeDerivNorm

Amplitude scaling acts on the J2 first-derivative unit-cube norm by the exact factor.

theorem Algsuperdiff.Section3.Provider.Stream.unitCubeSecondDerivNorm_scale_of_nonneg {d : ℕ} {c : ℝ} (hc : 0 ≤ c) (j : Frozen.Assumptions.ShellField d) : (Frozen.Assumptions.ShellField.scale c j).unitCubeSecondDerivNorm = c * j.unitCubeSecondDerivNorm

Amplitude scaling acts on the J2 second-derivative unit-cube norm by the exact factor.

Local cube derivative gauges

noncomputable def Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) : ℝ

The exact L∞ norm of the shell's first derivative on the open origin cube of scale ell: the manuscript's ‖∇j‖_{L∞(cu_ell)}. The chain-rule factor of the frozen spatialScale action is divided out, so this is the raw supremum with no scale normalization.

Equations

• Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm ell j = (3 ^ ell)⁻¹ * (Algsuperdiff.Frozen.Assumptions.ShellField.spatialScale (3 ^ ell) j).unitCubeDerivNorm

noncomputable def Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) : ℝ

The exact L∞ norm of the shell's second derivative on the open origin cube of scale ell: the manuscript's ‖∇²j‖_{L∞(cu_ell)}.

Equations

• Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm ell j = (3 ^ ell)⁻¹ ^ 2 * (Algsuperdiff.Frozen.Assumptions.ShellField.spatialScale (3 ^ ell) j).unitCubeSecondDerivNorm

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_nonneg {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) : 0 ≤ localCubeDerivNorm ell j

theorem Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm_nonneg {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) : 0 ≤ localCubeSecondDerivNorm ell j

theorem Algsuperdiff.Section3.Provider.Stream.measurable_localCubeDerivNorm {d : ℕ} (ell : ℤ) : Measurable (localCubeDerivNorm ell)

theorem Algsuperdiff.Section3.Provider.Stream.measurable_localCubeSecondDerivNorm {d : ℕ} (ell : ℤ) : Measurable (localCubeSecondDerivNorm ell)

@[simp]

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_zero {d : ℕ} (j : Frozen.Assumptions.ShellField d) : localCubeDerivNorm 0 j = j.unitCubeDerivNorm

@[simp]

theorem Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm_zero {d : ℕ} (j : Frozen.Assumptions.ShellField d) : localCubeSecondDerivNorm 0 j = j.unitCubeSecondDerivNorm

theorem Algsuperdiff.Section3.Provider.Stream.matrixDerivativeNorm_deriv_le_localCubeDerivNorm {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) : Frozen.Assumptions.ShellField.matrixDerivativeNorm (j.deriv x) ≤ localCubeDerivNorm ell j

The first-derivative gauge dominates the exact induced derivative norm at every point of the open origin cube of scale ell.

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_le_of_forall {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) {C : ℝ} (hC : 0 ≤ C) (h : ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell), Frozen.Assumptions.ShellField.matrixDerivativeNorm (j.deriv x) ≤ C) : localCubeDerivNorm ell j ≤ C

Minimality of the first-derivative gauge.

theorem Algsuperdiff.Section3.Provider.Stream.matrixSecondDerivativeNorm_secondDeriv_le_localCubeSecondDerivNorm {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) : Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm (j.secondDeriv x) ≤ localCubeSecondDerivNorm ell j

The second-derivative gauge dominates the exact twice-induced derivative norm at every point of the open origin cube of scale ell.

theorem Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm_le_of_forall {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) {C : ℝ} (hC : 0 ≤ C) (h : ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell), Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm (j.secondDeriv x) ≤ C) : localCubeSecondDerivNorm ell j ≤ C

Minimality of the second-derivative gauge.

Monotonicity in the cube scale

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_mono {d : ℕ} {ell ell' : ℤ} (h : ell ≤ ell') (j : Frozen.Assumptions.ShellField d) : localCubeDerivNorm ell j ≤ localCubeDerivNorm ell' j

The first-derivative gauge is monotone in the cube scale, since larger scales mean larger cubes.

theorem Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm_mono {d : ℕ} {ell ell' : ℤ} (h : ell ≤ ell') (j : Frozen.Assumptions.ShellField d) : localCubeSecondDerivNorm ell j ≤ localCubeSecondDerivNorm ell' j

The second-derivative gauge is monotone in the cube scale.

Exact triadic scaling

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_triadicScale {d : ℕ} (gamma : ℝ) (ell k : ℤ) (j : Frozen.Assumptions.ShellField d) : localCubeDerivNorm ell (Frozen.Assumptions.ShellField.triadicScale gamma k j) = Real.rpow 3 ((gamma - 1) * ↑k) * localCubeDerivNorm (ell - k) j

The exact first-derivative scaling identity: the triadically scaled shell 3^{γk} j(3^{-k}·) has first-derivative gauge 3^{(γ-1)k} times the gauge of the original shell at the shifted cube scale ell - k. This is the derivative analogue of Algsuperdiff.Section3.Cutoff.localCubeControl_triadicScale; the extra factor 3^{-k} is the chain rule.

theorem Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm_triadicScale {d : ℕ} (gamma : ℝ) (ell k : ℤ) (j : Frozen.Assumptions.ShellField d) : localCubeSecondDerivNorm ell (Frozen.Assumptions.ShellField.triadicScale gamma k j) = Real.rpow 3 ((gamma - 2) * ↑k) * localCubeSecondDerivNorm (ell - k) j

The exact second-derivative scaling identity, with the two chain-rule factors producing the exponent γ - 2.