IncrementGauge

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

Subadditivity of the local cube derivative gauges

The two derivative gauges of Algsuperdiff.Section3.Provider.Stream.ShellDerivativeControl are raw suprema over an open origin cube, so they obey the triangle inequality along the additive layer of Algsuperdiff.Section3.Provider.Stream.ShellSum.

Main results

• localCubeDerivNorm_add_le, localCubeSecondDerivNorm_add_le: the binary triangle inequality for the two open-cube gauges.
• localCubeDerivNorm_sum_le, localCubeSecondDerivNorm_sum_le: the finite triangle inequality along ShellField.sum.
• localCubeDerivNorm_translate_shellIncrement_le, localCubeSecondDerivNorm_translate_shellIncrement_le: the same for the literal stream increment k_m - k_n on a translated cube.

References

• ABK26, e.Bosc.def, e.Bosc.decomp.

The two induced matrix-derivative norms vanish at zero

theorem Algsuperdiff.Section3.Provider.Stream.matrixDerivativeNorm_zero_le {d : ℕ} : Frozen.Assumptions.ShellField.matrixDerivativeNorm 0 ≤ 0

theorem Algsuperdiff.Section3.Provider.Stream.matrixSecondDerivativeNorm_zero_le {d : ℕ} : Frozen.Assumptions.ShellField.matrixSecondDerivativeNorm 0 ≤ 0

The gauges of the zero shell field

@[simp]

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_zero_field {d : ℕ} (ell : ℤ) : localCubeDerivNorm ell (Frozen.Assumptions.ShellField.zero d) = 0

@[simp]

theorem Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm_zero_field {d : ℕ} (ell : ℤ) : localCubeSecondDerivNorm ell (Frozen.Assumptions.ShellField.zero d) = 0

Binary triangle inequalities

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_add_le {d : ℕ} (ell : ℤ) (j k : Frozen.Assumptions.ShellField d) : localCubeDerivNorm ell (j.add k) ≤ localCubeDerivNorm ell j + localCubeDerivNorm ell k

||grad (j + k)||_{L∞(cu_ell)} <= ||grad j|| + ||grad k||.

theorem Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm_add_le {d : ℕ} (ell : ℤ) (j k : Frozen.Assumptions.ShellField d) : localCubeSecondDerivNorm ell (j.add k) ≤ localCubeSecondDerivNorm ell j + localCubeSecondDerivNorm ell k

||grad² (j + k)||_{L∞(cu_ell)} <= ||grad² j|| + ||grad² k||.

Finite triangle inequalities

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_sum_le {d : ℕ} (ell : ℤ) {ι : Type u_1} (s : Finset ι) (f : ι → Frozen.Assumptions.ShellField d) : localCubeDerivNorm ell (Frozen.Assumptions.ShellField.sum s f) ≤ ∑ i ∈ s, localCubeDerivNorm ell (f i)

||grad (sum_i j_i)||_{L∞(cu_ell)} <= sum_i ||grad j_i||_{L∞(cu_ell)}.

theorem Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm_sum_le {d : ℕ} (ell : ℤ) {ι : Type u_1} (s : Finset ι) (f : ι → Frozen.Assumptions.ShellField d) : localCubeSecondDerivNorm ell (Frozen.Assumptions.ShellField.sum s f) ≤ ∑ i ∈ s, localCubeSecondDerivNorm ell (f i)

||grad² (sum_i j_i)||_{L∞(cu_ell)} <= sum_i ||grad² j_i||_{L∞(cu_ell)}.

The literal stream increment

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_translate_shellIncrement_le {d : ℕ} (ell : ℤ) (z : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) (n m : ℤ) : localCubeDerivNorm ell (Frozen.Assumptions.ShellField.translate z (shellIncrement omega n m)) ≤ ∑ k ∈ Finset.Ioc n m, localCubeDerivNorm ell (Frozen.Assumptions.ShellField.translate z (omega k))

The literal-increment first-derivative triangle inequality ||grad (k_m - k_n)||_{L∞(z + cu_ell)} <= sum_{k in (n,m]} ||grad j_k||.

theorem Algsuperdiff.Section3.Provider.Stream.localCubeSecondDerivNorm_translate_shellIncrement_le {d : ℕ} (ell : ℤ) (z : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) (n m : ℤ) : localCubeSecondDerivNorm ell (Frozen.Assumptions.ShellField.translate z (shellIncrement omega n m)) ≤ ∑ k ∈ Finset.Ioc n m, localCubeSecondDerivNorm ell (Frozen.Assumptions.ShellField.translate z (omega k))

The literal-increment second-derivative triangle inequality.