Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Determinant bounds for Hessian estimates

theorem ViscositySolns.Matrix.PosSemidef.det_le_pow_of_le_smul_one {n : ℕ} {lambda : ℝ} (hlambda : 0 ≤ lambda) {A : Hessian n} (hA : Matrix.PosSemidef A) (hAle : A ≤ lambda • 1) : Matrix.det A ≤ lambda ^ n

Determinant bound for positive semidefinite matrices bounded above by a scalar multiple of the identity.

In quantified mathematical form, if A is a positive semidefinite real n × n matrix, if 0 ≤ lambda, and if A ≤ lambda I in the Loewner order, then det A ≤ lambda^n.

theorem ViscositySolns.hessian_abs_det_le_pow_of_neg_smul_one_le_of_le_zero {n : ℕ} {lambda : ℝ} (hlambda : 0 ≤ lambda) {A : Hessian n} (hA : Matrix.IsHermitian A) (hlower : -(lambda • 1) ≤ A) (hupper : A ≤ 0) : |Matrix.det A| ≤ lambda ^ n

Determinant bound for Hermitian matrices whose eigenvalues lie between -lambda and 0.

In quantified mathematical form, if A is Hermitian, 0 ≤ lambda, -lambda I ≤ A, and A ≤ 0, then |det A| ≤ lambda^n.

theorem ViscositySolns.hessian_ofReal_abs_det_le_of_neg_smul_one_le_of_le_zero {n : ℕ} {lambda : ℝ} (hlambda : 0 ≤ lambda) {A : Hessian n} (hA : Matrix.IsHermitian A) (hlower : -(lambda • 1) ≤ A) (hupper : A ≤ 0) : ENNReal.ofReal |Matrix.det A| ≤ ENNReal.ofReal (max (lambda ^ n) 1)

The determinant bound in the ℝ≥0∞ form used by the Jacobian estimate.

In quantified mathematical form, if A is Hermitian, 0 ≤ lambda, -lambda I ≤ A, and A ≤ 0, then ofReal |det A| ≤ ofReal (max (lambda^n) 1).

The maximum with 1 gives a positive finite constant for the later division step, while still dominating the determinant bound supplied by the preceding theorem.

theorem ViscositySolns.ofReal_abs_det_le_of_forall_hessian_bounds {n : ℕ} {S : Set (Point n)} {H : Point n → Hessian n} {lambda : ℝ} (hlambda : 0 ≤ lambda) (hHerm : ∀ x ∈ S, Matrix.IsHermitian (H x)) (hlower : ∀ x ∈ S, -(lambda • 1) ≤ H x) (hupper : ∀ x ∈ S, H x ≤ 0) (x : Point n) : x ∈ S → ENNReal.ofReal |Matrix.det (H x)| ≤ ENNReal.ofReal (max (lambda ^ n) 1)

Pointwise determinant bound from Loewner-order Hessian bounds.

In quantified mathematical form, let S ⊆ R^n and let H x be a real symmetric matrix for every x ∈ S. If 0 ≤ lambda and, for every x ∈ S, -lambda I ≤ H x ≤ 0, then for every x ∈ S, ofReal |det (H x)| ≤ ofReal (max (lambda^n) 1).