MatrixNorms

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

Entry bounds for the frozen derivative norms

Algsuperdiff.Frozen.Section24.matrixDerivativeNorm and Algsuperdiff.Frozen.Section24.matrixSecondDerivativeNorm are suprema of Euclidean matrix norms over the vecNorm-unit ball. Two facts about them are needed to feed the W^{1,∞}-to-Lipschitz bridge from the frozen UnitCubeSkewW2Infinity carrier:

• every coordinate entry of a derivative evaluated at a basis direction is dominated by the derivative norm (abs_entry_apply_le_matrixDerivativeNorm, abs_entry_apply_apply_le_matrixSecondDerivativeNorm), and
• the derivative norm is itself dominated by a fixed multiple of the sum of the absolute values of those entries (matrixDerivativeNorm_le_sq_mul_sum, matrixSecondDerivativeNorm_le_sq_mul_sum).

The second family is what turns the entrywise L^∞ memberships stored in the frozen carrier into finiteness of the L^∞ norms appearing in UnitCubeSkewW2Infinity.w1Infinity and UnitCubeSkewW2Infinity.gradientW1Infinity, without which those real numbers carry no information.

@[instance_reducible]

noncomputable instance Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.instNormedAddCommGroupVecMatCLM {d : ℕ} : NormedAddCommGroup (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Migration cache (mathlib v4.33.1): typeclass search no longer finds the ContinuousLinearMap normed-group/space instances on the Vec/Mat abbreviations without a hint; force it once here so the rest of the file's inferInstance-driven elaboration (implicit in ‖D‖, .opNorm_le_bound, .le_opNorm, etc.) succeeds.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.instNormedAddCommGroupVecMatCLM = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.instNormedSpaceVecMatCLM {d : ℕ} : NormedSpace ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.instNormedSpaceVecMatCLM = ContinuousLinearMap.toNormedSpace

@[instance_reducible]

noncomputable instance Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.instNormedAddCommGroupVecVecMatCLM {d : ℕ} : NormedAddCommGroup (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.instNormedAddCommGroupVecVecMatCLM = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.instNormedSpaceVecVecMatCLM {d : ℕ} : NormedSpace ℝ (HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d)

The generic ContinuousLinearMap.toNormedSpace leaves 𝕜₂ as a metavariable until after its SMulCommClass argument is resolved, so ordinary instance search never reaches a concrete SMulCommClass ℝ ℝ (Vec d →L[ℝ] Mat d) goal; supply every argument explicitly (with the commuting-scalar witness spelled out) to sidestep it.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.instNormedSpaceVecVecMatCLM = ContinuousLinearMap.toNormedSpace

Elementary comparisons between the ambient and Euclidean norms

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.norm_vec_le_vecNorm {d : ℕ} (v : HCPolySupport.Vec d) : ‖v‖ ≤ HCPolySupport.Book.Ch02.vecNorm v

The ambient supremum norm on Vec d is bounded by the Euclidean norm.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.vecNorm_basisVec_le_one {d : ℕ} (k : Fin d) : HCPolySupport.Book.Ch02.vecNorm (HCPolySupport.basisVec k) ≤ 1

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.vecNorm_zero_le_one {d : ℕ} : HCPolySupport.Book.Ch02.vecNorm 0 ≤ 1

Entrywise comparisons for matrices

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.norm_mat_le_sum_abs_entries {d : ℕ} (A : HCPolySupport.Mat d) : ‖A‖ ≤ ∑ i : Fin d, ∑ j : Fin d, |A i j|

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.sum_abs_entries_le_sq_mul_norm {d : ℕ} (A : HCPolySupport.Mat d) : ∑ i : Fin d, ∑ j : Fin d, |A i j| ≤ ↑d ^ 2 * ‖A‖

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixNorm_le_sq_mul_norm {d : ℕ} (A : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.matrixNorm A ≤ ↑d ^ 2 * ‖A‖

Operator norms through the coordinate directions

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.norm_le_sum_basisVec_apply {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : HCPolySupport.Vec d →L[ℝ] F) : ‖L‖ ≤ ∑ k : Fin d, ‖L (HCPolySupport.basisVec k)‖

Vector-valued form of Homogenization.norm_clm_le_sum_basisVec_apply.

The frozen first-derivative norm

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixDerivativeNorm_range_bddAbove {d : ℕ} (D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) : BddAbove (Set.range fun (v : { v : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm v ≤ 1 }) => HCPolySupport.Book.Ch02.matrixNorm (D ↑v))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixDerivativeNorm_range_nonempty {d : ℕ} (D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) : (Set.range fun (v : { v : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm v ≤ 1 }) => HCPolySupport.Book.Ch02.matrixNorm (D ↑v)).Nonempty

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixNorm_apply_le_matrixDerivativeNorm {d : ℕ} (D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) (v : HCPolySupport.Vec d) (hv : HCPolySupport.Book.Ch02.vecNorm v ≤ 1) : HCPolySupport.Book.Ch02.matrixNorm (D v) ≤ Frozen.Section24.matrixDerivativeNorm D

The frozen first-derivative norm dominates every Euclidean matrix norm on the Euclidean unit ball.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixDerivativeNorm_nonneg {d : ℕ} (D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) : 0 ≤ Frozen.Section24.matrixDerivativeNorm D

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.abs_entry_apply_le_matrixDerivativeNorm {d : ℕ} (D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) (k i j : Fin d) : |D (HCPolySupport.basisVec k) i j| ≤ Frozen.Section24.matrixDerivativeNorm D

Every coordinate entry of a derivative in a coordinate direction is bounded by the frozen first-derivative norm.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixDerivativeNorm_le_sq_mul_norm {d : ℕ} (D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) : Frozen.Section24.matrixDerivativeNorm D ≤ ↑d ^ 2 * ‖D‖

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixDerivativeNorm_le_sq_mul_sum {d : ℕ} (D : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) : Frozen.Section24.matrixDerivativeNorm D ≤ ↑d ^ 2 * ∑ k : Fin d, ∑ i : Fin d, ∑ j : Fin d, |D (HCPolySupport.basisVec k) i j|

The frozen first-derivative norm is dominated by the coordinate entries.

The frozen second-derivative norm

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixSecondDerivativeNorm_range_bddAbove {d : ℕ} (H : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) : BddAbove (Set.range fun (v : { v : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm v ≤ 1 }) => Frozen.Section24.matrixDerivativeNorm (H ↑v))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixSecondDerivativeNorm_range_nonempty {d : ℕ} (H : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) : (Set.range fun (v : { v : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm v ≤ 1 }) => Frozen.Section24.matrixDerivativeNorm (H ↑v)).Nonempty

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixDerivativeNorm_apply_le_matrixSecondDerivativeNorm {d : ℕ} (H : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) (v : HCPolySupport.Vec d) (hv : HCPolySupport.Book.Ch02.vecNorm v ≤ 1) : Frozen.Section24.matrixDerivativeNorm (H v) ≤ Frozen.Section24.matrixSecondDerivativeNorm H

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixSecondDerivativeNorm_nonneg {d : ℕ} (H : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) : 0 ≤ Frozen.Section24.matrixSecondDerivativeNorm H

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.abs_entry_apply_apply_le_matrixSecondDerivativeNorm {d : ℕ} (H : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) (l k i j : Fin d) : |(H (HCPolySupport.basisVec l)) (HCPolySupport.basisVec k) i j| ≤ Frozen.Section24.matrixSecondDerivativeNorm H

Every coordinate entry of a second derivative in two coordinate directions is bounded by the frozen second-derivative norm.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.matrixSecondDerivativeNorm_le_sq_mul_sum {d : ℕ} (H : HCPolySupport.Vec d →L[ℝ] HCPolySupport.Vec d →L[ℝ] HCPolySupport.Mat d) : Frozen.Section24.matrixSecondDerivativeNorm H ≤ ↑d ^ 2 * ∑ l : Fin d, ∑ k : Fin d, ∑ i : Fin d, ∑ j : Fin d, |(H (HCPolySupport.basisVec l)) (HCPolySupport.basisVec k) i j|

The frozen second-derivative norm is dominated by the coordinate entries.