Coarse-graining support: Support.Ambient.CoefficientField

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

@[reducible, inline]

abbrev HCPolySupport.CoeffField (d : ℕ) : Type

Real matrix-valued fields on the d-dimensional coordinate space.

Equations

• HCPolySupport.CoeffField d = (HCPolySupport.Vec d → HCPolySupport.Mat d)

def HCPolySupport.IsEllipticMatrix {d : ℕ} (lam Lam : ℝ) (A : Mat d) : Prop

Positive ordered bounds lam ≤ Lam, with quadratic lower bounds lam for A and Lam⁻¹ for its matrix inverse.

Equations

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

theorem HCPolySupport.IsEllipticMatrix.mono {d : ℕ} {lam Lam lam' Lam' : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (hlam'_pos : 0 < lam') (hlam'_le : lam' ≤ lam) (hLam_le : Lam ≤ Lam') : IsEllipticMatrix lam' Lam' A

theorem HCPolySupport.isUnit_det_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) : IsUnit (Matrix.det A)

theorem HCPolySupport.vecNormSq_matVecMul_le_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : vecNormSq (matVecMul A ξ) ≤ Lam ^ 2 * vecNormSq ξ

theorem HCPolySupport.abs_apply_le_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (i j : Fin d) : |A i j| ≤ Lam

theorem HCPolySupport.isEllipticMatrix_transpose {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) : IsEllipticMatrix lam Lam (matTranspose A)

theorem HCPolySupport.vecNormSq_matVecMul_symmPart_le_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : vecNormSq (matVecMul (symmPart A) ξ) ≤ Lam ^ 2 * vecNormSq ξ

theorem HCPolySupport.vecNormSq_matVecMul_skewPart_le_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : vecNormSq (matVecMul (skewPart A) ξ) ≤ Lam ^ 2 * vecNormSq ξ

theorem HCPolySupport.vecDot_matVecMul_comm_of_isSymm {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) (ξ η : Vec d) : vecDot ξ (matVecMul A η) = vecDot η (matVecMul A ξ)

theorem HCPolySupport.isSymm_nonsingInv {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) : Matrix.IsSymm A⁻¹

theorem HCPolySupport.vecDot_matVecMul_symmPart {d : ℕ} (A : Mat d) (ξ : Vec d) : vecDot ξ (matVecMul (symmPart A) ξ) = vecDot ξ (matVecMul A ξ)

theorem HCPolySupport.sq_le_mul_of_quadratic_nonneg {a b c : ℝ} (hc : 0 ≤ c) (hquad : ∀ (t : ℝ), 0 ≤ a - 2 * t * b + t ^ 2 * c) : b ^ 2 ≤ a * c

theorem HCPolySupport.sq_vecDot_matVecMul_le_of_isSymm_of_nonneg {d : ℕ} {A : Mat d} (hA : Matrix.IsSymm A) (hA_nonneg : ∀ (ξ : Vec d), 0 ≤ vecDot ξ (matVecMul A ξ)) (ξ η : Vec d) : vecDot ξ (matVecMul A η) ^ 2 ≤ vecDot ξ (matVecMul A ξ) * vecDot η (matVecMul A η)

theorem HCPolySupport.sq_vecDot_matVecMul_symmPart_le_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ η : Vec d) : vecDot ξ (matVecMul (symmPart A) η) ^ 2 ≤ vecDot ξ (matVecMul (symmPart A) ξ) * vecDot η (matVecMul (symmPart A) η)

theorem HCPolySupport.lowerBound_symmPart_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : lam * vecNormSq ξ ≤ vecDot ξ (matVecMul (symmPart A) ξ)

theorem HCPolySupport.upperBound_symmPart_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ : Vec d) : vecDot ξ (matVecMul (symmPart A) ξ) ≤ Lam * vecNormSq ξ

theorem HCPolySupport.isUnit_det_symmPart_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) : IsUnit (Matrix.det (symmPart A))

theorem HCPolySupport.abs_apply_symmPartInv_le_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (i j : Fin d) : |(symmPart A)⁻¹ i j| ≤ lam⁻¹

def HCPolySupport.IsEllipticFieldOn {d : ℕ} (lam Lam : ℝ) (U : Set (Vec d)) (a : CoeffField d) : Prop

Measurability of the zero extension from U, together with pointwise matrix ellipticity on U.

Equations

• HCPolySupport.IsEllipticFieldOn lam Lam U a = ((Measurable fun (x : HCPolySupport.Vec d) (i j : Fin d) => if x ∈ U then a x i j else 0) ∧ ∀ x ∈ U, HCPolySupport.IsEllipticMatrix lam Lam (a x))

theorem HCPolySupport.abs_apply_le_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) {x : Vec d} (hx : x ∈ U) (i j : Fin d) : |a x i j| ≤ Lam

theorem HCPolySupport.measurableSet_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) : MeasurableSet U

theorem HCPolySupport.IsEllipticFieldOn.mono {d : ℕ} {lam Lam : ℝ} {U V : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) (hV : MeasurableSet V) (hVU : V ⊆ U) : IsEllipticFieldOn lam Lam V a

theorem HCPolySupport.IsEllipticFieldOn.mono_constants {d : ℕ} {lam Lam lam' Lam' : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) (hlam'_pos : 0 < lam') (hlam'_le : lam' ≤ lam) (hLam_le : Lam ≤ Lam') : IsEllipticFieldOn lam' Lam' U a

theorem HCPolySupport.abs_apply_symmPartInv_le_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) {x : Vec d} (hx : x ∈ U) (i j : Fin d) : |(symmPart (a x))⁻¹ i j| ≤ lam⁻¹

theorem HCPolySupport.memVectorL2_matVecMul_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : MemVectorL2 U fun (x : Vec d) => matVecMul (a x) (f x)

theorem HCPolySupport.memVectorL2_matVecMul_symmPart_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : MemVectorL2 U fun (x : Vec d) => matVecMul (symmPart (a x)) (f x)

theorem HCPolySupport.memVectorL2_matVecMul_symmPartInv_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : MemVectorL2 U fun (x : Vec d) => matVecMul (symmPart (a x))⁻¹ (f x)

theorem HCPolySupport.memVectorL2_matVecMul_skewPart_of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : MemVectorL2 U fun (x : Vec d) => matVecMul (skewPart (a x)) (f x)

noncomputable def HCPolySupport.restrictCoeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : CoeffField d

The coefficient field equal to a on U and zero outside U.

Equations

• HCPolySupport.restrictCoeffField U a x = if x ∈ U then a x else 0

@[simp]

theorem HCPolySupport.restrictCoeffField_apply_of_mem {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {x : Vec d} (hx : x ∈ U) : restrictCoeffField U a x = a x

@[simp]

theorem HCPolySupport.restrictCoeffField_apply_of_not_mem {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {x : Vec d} (hx : x ∉ U) : restrictCoeffField U a x = 0

@[simp]

theorem HCPolySupport.restrictCoeffField_univ {d : ℕ} (a : CoeffField d) : restrictCoeffField Set.univ a = a

@[simp]

theorem HCPolySupport.restrictCoeffField_empty {d : ℕ} (a : CoeffField d) : restrictCoeffField ∅ a = 0

noncomputable def HCPolySupport.extendByIdCoeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : CoeffField d

Extension companion to restrictCoeffField: outside U we insert the identity matrix, matching the Chapter-2 note convention.

Equations

• HCPolySupport.extendByIdCoeffField U a x = if x ∈ U then a x else 1

@[simp]

theorem HCPolySupport.extendByIdCoeffField_apply_of_mem {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {x : Vec d} (hx : x ∈ U) : extendByIdCoeffField U a x = a x

@[simp]

theorem HCPolySupport.extendByIdCoeffField_apply_of_not_mem {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {x : Vec d} (hx : x ∉ U) : extendByIdCoeffField U a x = 1

@[simp]

theorem HCPolySupport.extendByIdCoeffField_univ {d : ℕ} (a : CoeffField d) : extendByIdCoeffField Set.univ a = a

@[simp]

theorem HCPolySupport.extendByIdCoeffField_empty {d : ℕ} (a : CoeffField d) : extendByIdCoeffField ∅ a = 1

@[simp]

theorem HCPolySupport.restrictCoeffField_extendByIdCoeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : restrictCoeffField U (extendByIdCoeffField U a) = restrictCoeffField U a

def HCPolySupport.translateCoeffField {d : ℕ} (z : Vec d) (a : CoeffField d) : CoeffField d

The translated coefficient field whose value at x is a (x + z).

Equations

• HCPolySupport.translateCoeffField z a x = a fun (i : Fin d) => x i + z i

noncomputable def HCPolySupport.symmCoeffField {d : ℕ} (a : CoeffField d) : CoeffField d

The field formed by taking the symmetric part of each coefficient matrix.

Equations

• HCPolySupport.symmCoeffField a x = HCPolySupport.symmPart (a x)

noncomputable def HCPolySupport.skewCoeffField {d : ℕ} (a : CoeffField d) : CoeffField d

The field formed by taking the skew-symmetric part of each coefficient matrix.

Equations

• HCPolySupport.skewCoeffField a x = HCPolySupport.skewPart (a x)