LocalizedSkewAlgebra

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

Pointwise algebra of an antisymmetric coefficient

The localized decay estimates split a coefficient whose symmetric part is the fixed scalar nu • I into that scalar part and an antisymmetric remainder. Three pointwise facts are used repeatedly and are collected here.

• An antisymmetric matrix contributes nothing to the quadratic form, so the elliptic energy is exactly nu times the squared gradient, with no inequality and no upper constant.
• An antisymmetric matrix flips the sign of the flux pairing.
• Since the two parts are orthogonal in the pairing, the size of the whole matrix is sqrt (nu ^ 2 + Ks ^ 2) when the antisymmetric part has size Ks, in particular at most nu + Ks.

The Young inequality for the flux cross term is then stated with the size constant of the matrix in place of the upper ellipticity constant, so that a caller may supply it at a single point rather than on the whole domain.

Main results

• DivergenceFormProcess.Decay.vecDot_matVecMul_self_eq_zero_of_skew
• DivergenceFormProcess.Decay.vecNormSq_matVecMul_le_of_symmPart_eq
• DivergenceFormProcess.Decay.localizedFlux_young

Antisymmetry

theorem DivergenceFormProcess.Decay.skew_entry_of_matTranspose {d : ℕ} {A : HCPolySupport.Mat d} (h : HCPolySupport.matTranspose A = -A) (i j : Fin d) : A j i = -A i j

Entrywise antisymmetry, read off the matrix identity.

theorem DivergenceFormProcess.Decay.vecDot_matVecMul_eq_sum {d : ℕ} (A : HCPolySupport.Mat d) (p q : HCPolySupport.Vec d) : HCPolySupport.vecDot (HCPolySupport.matVecMul A p) q = ∑ i : Fin d, ∑ j : Fin d, A i j * p j * q i

Expansion of the flux pairing as a double sum.

theorem DivergenceFormProcess.Decay.vecDot_matVecMul_eq_neg_of_skew {d : ℕ} {A : HCPolySupport.Mat d} (h : HCPolySupport.matTranspose A = -A) (p q : HCPolySupport.Vec d) : HCPolySupport.vecDot (HCPolySupport.matVecMul A p) q = -HCPolySupport.vecDot (HCPolySupport.matVecMul A q) p

An antisymmetric matrix flips the sign of the flux pairing.

theorem DivergenceFormProcess.Decay.vecDot_matVecMul_self_eq_zero_of_skew {d : ℕ} {A : HCPolySupport.Mat d} (h : HCPolySupport.matTranspose A = -A) (p : HCPolySupport.Vec d) : HCPolySupport.vecDot (HCPolySupport.matVecMul A p) p = 0

An antisymmetric matrix has vanishing quadratic form.

theorem DivergenceFormProcess.Decay.sum_sum_mul_eq_zero_of_skew_of_symm {d : ℕ} {K : HCPolySupport.Mat d} (hK : ∀ (i j : Fin d), K j i = -K i j) {T : Fin d → Fin d → ℝ} (hT : ∀ (i j : Fin d), T i j = T j i) : ∑ i : Fin d, ∑ j : Fin d, K i j * T i j = 0

An antisymmetric array pairs to zero against a symmetric one.

The size of a coefficient with scalar symmetric part

theorem DivergenceFormProcess.Decay.matVecMul_smul_one {d : ℕ} (nu : ℝ) (p : HCPolySupport.Vec d) (i : Fin d) : HCPolySupport.matVecMul (nu • 1) p i = nu * p i

The scalar matrix acts by scalar multiplication.

theorem DivergenceFormProcess.Decay.matVecMul_scalar_add_apply {d : ℕ} {nu : ℝ} {A K : HCPolySupport.Mat d} (hA : A = nu • 1 + K) (p : HCPolySupport.Vec d) (i : Fin d) : HCPolySupport.matVecMul A p i = nu * p i + HCPolySupport.matVecMul K p i

Splitting the flux of a coefficient with scalar symmetric part.

theorem DivergenceFormProcess.Decay.symmPart_scalar_add_skew {d : ℕ} {nu : ℝ} {A K : HCPolySupport.Mat d} (hA : A = nu • 1 + K) (hK : HCPolySupport.matTranspose K = -K) : HCPolySupport.symmPart A = nu • 1

The symmetric part of nu • I plus an antisymmetric matrix.

theorem DivergenceFormProcess.Decay.vecDot_matVecMul_eq_of_scalar_add_skew {d : ℕ} {nu : ℝ} {A K : HCPolySupport.Mat d} (hA : A = nu • 1 + K) (hK : HCPolySupport.matTranspose K = -K) (p : HCPolySupport.Vec d) : HCPolySupport.vecDot (HCPolySupport.matVecMul A p) p = nu * HCPolySupport.vecNormSq p

The exact quadratic form. When the symmetric part of the coefficient is the scalar nu • I, the elliptic energy is exactly nu times the squared gradient: the antisymmetric remainder contributes nothing and no upper size constant appears.

theorem DivergenceFormProcess.Decay.vecNormSq_matVecMul_le_of_scalar_add_skew {d : ℕ} {p : HCPolySupport.Vec d} {nu Ks : ℝ} {A K : HCPolySupport.Mat d} (hA : A = nu • 1 + K) (hK : HCPolySupport.matTranspose K = -K) (hKsize : HCPolySupport.vecNormSq (HCPolySupport.matVecMul K p) ≤ Ks ^ 2 * HCPolySupport.vecNormSq p) : HCPolySupport.vecNormSq (HCPolySupport.matVecMul A p) ≤ (nu ^ 2 + Ks ^ 2) * HCPolySupport.vecNormSq p

The size on the layer. The scalar and antisymmetric parts are orthogonal in the flux pairing, so the size of the whole coefficient is the Pythagorean combination of nu and the size of the antisymmetric part.

theorem DivergenceFormProcess.Decay.vecNormSq_matVecMul_le_add_of_scalar_add_skew {d : ℕ} {p : HCPolySupport.Vec d} {nu Ks : ℝ} {A K : HCPolySupport.Mat d} (hnu : 0 ≤ nu) (hKs : 0 ≤ Ks) (hA : A = nu • 1 + K) (hK : HCPolySupport.matTranspose K = -K) (hKsize : HCPolySupport.vecNormSq (HCPolySupport.matVecMul K p) ≤ Ks ^ 2 * HCPolySupport.vecNormSq p) : HCPolySupport.vecNormSq (HCPolySupport.matVecMul A p) ≤ (nu + Ks) ^ 2 * HCPolySupport.vecNormSq p

The size bound in the additive form used by the layer hypotheses.

The Young inequality with a layer size constant

theorem DivergenceFormProcess.Decay.localizedFlux_young {d : ℕ} {nu C e p : ℝ} {A : HCPolySupport.Mat d} (hnu : 0 < nu) (hC : 0 < C) (hA : ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq (HCPolySupport.matVecMul A v) ≤ C ^ 2 * HCPolySupport.vecNormSq v) (z de : HCPolySupport.Vec d) : |2 * e * p * HCPolySupport.vecDot (HCPolySupport.matVecMul A z) de| ≤ nu / 2 * (e ^ 2 * HCPolySupport.vecNormSq z) + 2 * C ^ 2 / nu * (p ^ 2 * HCPolySupport.vecNormSq de)

Young inequality for the flux cross term with the size of the coefficient in place of an upper ellipticity constant. Half of the elliptic energy at rate nu is kept and the remainder is charged to the weight gradient.