Bounds

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

Uniform pointwise bounds along the perturbation path

The minimizer-continuity step of l.sensitivity.coarse.grained.general needs three uniform pointwise estimates, all measured against the doubled energy density of the base coefficient rather than against an L² norm:

• an a.e. uniform entry bound for an L∞ matrix field (restated here as a standalone lemma; the frozen perturbCoeffOn body carries the same argument inline, and that file is never edited);
• the two-sided comparison c |X|² ≤ X · bfA(a) X ≤ C |X|² supplied by the Chapter 2 block formalism; and
• the resulting domination of the linear and quadratic response densities by the energy density, with a free Young parameter.

Because every bound is expressed through the energy density itself, the continuity argument downstream never has to leave the doubled functional.

A standalone a.e. entry bound for L∞ matrix fields

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.lInfEntryBound {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (h : Frozen.Section24.LInfMatrixFieldOn U) : ℝ

The L∞ entry bound of a bounded matrix field: the sum of the essential suprema of all entries. This is the same quantity that the frozen perturbCoeffOn body builds inline; it is restated here so that the perturbation estimates can be proved without touching the frozen file.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.ae_abs_apply_le_lInfEntryBound {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (h : Frozen.Section24.LInfMatrixFieldOn U) (i j : Fin d) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U.carrier, |↑h x i j| ≤ lInfEntryBound h

Every entry of an L∞ matrix field is a.e. bounded by its entry bound.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.ae_forall_abs_apply_le_lInfEntryBound {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (h : Frozen.Section24.LInfMatrixFieldOn U) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U.carrier, ∀ (i j : Fin d), |↑h x i j| ≤ lInfEntryBound h

The a.e. uniform entry bound in the packaged form used downstream.

The Frobenius operator bound

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.vecNormSq_matVecMul_le_frobenius {d : ℕ} (A : HCPolySupport.Mat d) (η : HCPolySupport.Vec d) : HCPolySupport.vecNormSq (HCPolySupport.matVecMul A η) ≤ (∑ i : Fin d, ∑ j : Fin d, A i j ^ 2) * HCPolySupport.vecNormSq η

The Frobenius bound for the image of a matrix.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.vecNormSq_matVecMul_le_of_abs_apply_le {d : ℕ} {A : HCPolySupport.Mat d} {b : ℝ} (hb : ∀ (i j : Fin d), |A i j| ≤ b) (w : HCPolySupport.Vec d) : HCPolySupport.vecNormSq (HCPolySupport.matVecMul A w) ≤ ↑d * ↑d * b ^ 2 * HCPolySupport.vecNormSq w

An entrywise bound gives a uniform bound on the image of a matrix.

Comparison of the doubled quadratic form with the Euclidean norm

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockVecDot_self_eq {d : ℕ} (Z : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot Z Z = HCPolySupport.vecNormSq Z.1 + HCPolySupport.vecNormSq Z.2

Block self-pairing is the sum of the two component norms.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.vecNormSq_fst_le_blockVecDot_self {d : ℕ} (Z : HCPolySupport.BlockVec d) : HCPolySupport.vecNormSq Z.1 ≤ HCPolySupport.blockVecDot Z Z

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.vecNormSq_snd_le_blockVecDot_self {d : ℕ} (Z : HCPolySupport.BlockVec d) : HCPolySupport.vecNormSq Z.2 ≤ HCPolySupport.blockVecDot Z Z

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockVecDot_self_nonneg {d : ℕ} (Z : HCPolySupport.BlockVec d) : 0 ≤ HCPolySupport.blockVecDot Z Z

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Path.blockCoercivityConst (lam Lam : ℝ) : ℝ

The reciprocal coercivity constant of the doubled matrix.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Path.blockCoercivityConst lam Lam = (1 + 2 * Lam ^ 2) / lam

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockCoercivityConst_pos {lam Lam : ℝ} (hlam : 0 < lam) : 0 < blockCoercivityConst lam Lam

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockVecDot_self_le_blockQuadForm {d : ℕ} {lam Lam : ℝ} {A : HCPolySupport.Mat d} (hA : HCPolySupport.IsEllipticMatrix lam Lam A) (Z : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot Z Z ≤ blockCoercivityConst lam Lam * HCPolySupport.blockVecDot Z (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) Z)

The Euclidean square norm of a block vector is controlled by its doubled quadratic form.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockQuadForm_nonneg {d : ℕ} {lam Lam : ℝ} {A : HCPolySupport.Mat d} (hA : HCPolySupport.IsEllipticMatrix lam Lam A) (Z : HCPolySupport.BlockVec d) : 0 ≤ HCPolySupport.blockVecDot Z (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) Z)

The doubled quadratic form is nonnegative under ellipticity.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockVecDot_image_self_le_blockQuadForm {d : ℕ} {lam Lam : ℝ} {A : HCPolySupport.Mat d} (hA : HCPolySupport.IsEllipticMatrix lam Lam A) (Z : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) Z) (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) Z) ≤ HCPolySupport.blockMatrixOfCoeffNormSqBound lam Lam * blockCoercivityConst lam Lam * HCPolySupport.blockVecDot Z (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) Z)

The block image of a block vector is controlled by its doubled quadratic form.