VecGauge

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

Elementary gauges and matrix algebra on the ambient vector carrier

The Section 5 modules work with two sizes of a vector of Vec d = Fin d → ℝ: the ambient supremum norm ‖v‖ that the carrier itself carries, and the Euclidean size vecNorm v in which the shell derivative gauges are written. This leaf collects the two facts about that carrier that several Section 5 modules need and that would otherwise be reproved in each of them:

• the homogeneity of the Euclidean size, and its comparison vecNorm v ≤ √d ‖v‖ with the ambient one, which is where every dimensional constant of the perturbation estimates comes from;
• the compatibility of the matrix action with a finite sum of vectors.

Both are stated for the plain carrier, with no model, cube or shell data, so the module sits below every other Section 5 support file.

Main results

• vecNorm_smul — absolute homogeneity of the Euclidean size.
• vecNorm_le_sqrt_dim_mul_norm — the Euclidean size is at most √d times the ambient supremum norm.
• matVecMul_finset_sum — a fixed matrix commutes with a finite sum of vectors.

theorem Algsuperdiff.Section5.Support.vecNorm_smul {d : ℕ} (c : ℝ) (v : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm (c • v) = |c| * HCPolySupport.Book.Ch02.vecNorm v

The Euclidean vector norm is absolutely homogeneous.

theorem Algsuperdiff.Section5.Support.vecNorm_le_sqrt_dim_mul_norm {d : ℕ} (v : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm v ≤ √↑d * ‖v‖

The Euclidean vector norm is at most √d times the ambient supremum norm.

theorem Algsuperdiff.Section5.Support.matVecMul_finset_sum {d : ℕ} {iota : Type u_1} (A : HCPolySupport.Mat d) (s : Finset iota) (v : iota → HCPolySupport.Vec d) : HCPolySupport.matVecMul A (∑ j ∈ s, v j) = ∑ j ∈ s, HCPolySupport.matVecMul A (v j)

The action of a fixed matrix commutes with a finite sum of vectors.