Basic

Support for the Armstrong–Vicol anomalous-diffusion formalization.

@[reducible, inline]

abbrev Homogenization.Vec (d : ℕ) : Type

Real coordinate vectors indexed by the spatial dimension.

Equations

• Homogenization.Vec d = (Fin d → ℝ)

@[reducible, inline]

abbrev Homogenization.Mat (d : ℕ) : Type

Real square matrices indexed by the spatial dimension.

Equations

• Homogenization.Mat d = Matrix (Fin d) (Fin d) ℝ

@[reducible, inline]

abbrev Homogenization.BlockVec (d : ℕ) : Type

Pair of spatial vectors representing the two blocks of a doubled vector.

Equations

• Homogenization.BlockVec d = (Homogenization.Vec d × Homogenization.Vec d)

structure Homogenization.BlockMat (d : ℕ) : Type

Two-by-two block matrix with square spatial matrix blocks.

• upperLeft : Mat d

  Matrix acting from the first input block to the first output block.

• upperRight : Mat d

  Matrix acting from the second input block to the first output block.

• lowerLeft : Mat d

  Matrix acting from the first input block to the second output block.

• lowerRight : Mat d

  Matrix acting from the second input block to the second output block.

@[instance_reducible]

instance Homogenization.instInhabitedBlockMat {a✝ : ℕ} : Inhabited (BlockMat a✝)

Equations

• Homogenization.instInhabitedBlockMat = { default := Homogenization.instInhabitedBlockMat.default }

def Homogenization.vecDot {d : ℕ} (x y : Vec d) : ℝ

Euclidean coordinate dot product of real spatial vectors.

Equations

• Homogenization.vecDot x y = ∑ i : Fin d, x i * y i

def Homogenization.vecNormSq {d : ℕ} (x : Vec d) : ℝ

Squared Euclidean length of a coordinate vector.

Equations

• Homogenization.vecNormSq x = Homogenization.vecDot x x

theorem Homogenization.sq_vecDot_le_vecNormSq_mul_vecNormSq {d : ℕ} (x y : Vec d) : vecDot x y ^ 2 ≤ vecNormSq x * vecNormSq y

theorem Homogenization.vecNormSq_nonneg {d : ℕ} (x : Vec d) : 0 ≤ vecNormSq x

theorem Homogenization.sq_apply_le_vecNormSq {d : ℕ} (x : Vec d) (i : Fin d) : x i ^ 2 ≤ vecNormSq x

theorem Homogenization.abs_le_add_halves_of_sq_le_mul {u A B : ℝ} (hu_sq : u ^ 2 ≤ A * B) (hA : 0 ≤ A) (hB : 0 ≤ B) : |u| ≤ A / 2 + B / 2

A real Young inequality packaged for Cauchy-Schwarz consequences.

theorem Homogenization.abs_vecDot_le_add_halves_vecNormSq {d : ℕ} (x y : Vec d) : |vecDot x y| ≤ vecNormSq x / 2 + vecNormSq y / 2

Young's inequality for the Euclidean dot product on project vectors.

theorem Homogenization.abs_mul_mul_vecDot_le_add_halves_mul_sq_vecNormSq {d : ℕ} (a b : ℝ) (x y : Vec d) : |a * b * vecDot x y| ≤ a ^ 2 * vecNormSq x / 2 + b ^ 2 * vecNormSq y / 2

Young's inequality for scalar-weighted Euclidean dot products.

theorem Homogenization.vecNormSq_eq_zero {d : ℕ} {x : Vec d} (h : vecNormSq x = 0) : x = 0

theorem Homogenization.vecNormSq_eq_zero_iff {d : ℕ} {x : Vec d} : vecNormSq x = 0 ↔ x = 0

theorem Homogenization.vecNormSq_smul {d : ℕ} (c : ℝ) (x : Vec d) : vecNormSq (c • x) = c ^ 2 * vecNormSq x

theorem Homogenization.vecNormSq_add_le {d : ℕ} (x y : Vec d) : vecNormSq (x + y) ≤ 2 * (vecNormSq x + vecNormSq y)

theorem Homogenization.vecNormSq_four_add_le {d : ℕ} (w x y z : Vec d) : vecNormSq (w + x + y + z) ≤ 4 * (vecNormSq w + vecNormSq x + vecNormSq y + vecNormSq z)

Four-term Cauchy estimate for the squared Euclidean norm.

theorem Homogenization.vecNormSq_sub_le {d : ℕ} (x y : Vec d) : vecNormSq (x - y) ≤ 2 * (vecNormSq x + vecNormSq y)

def Homogenization.matVecMul {d : ℕ} (A : Mat d) (x : Vec d) : Vec d

Matrix-vector multiplication in coordinate form.

Equations

• Homogenization.matVecMul A x i = ∑ j : Fin d, A i j * x j

def Homogenization.matTranspose {d : ℕ} (A : Mat d) : Mat d

Transpose of a spatial matrix.

Equations

• Homogenization.matTranspose A = Matrix.transpose A

def Homogenization.blockVecDot {d : ℕ} (X Y : BlockVec d) : ℝ

Sum of the Euclidean dot products of the corresponding vector blocks.

Equations

• Homogenization.blockVecDot X Y = Homogenization.vecDot X.1 Y.1 + Homogenization.vecDot X.2 Y.2

def Homogenization.blockMatVecMul {d : ℕ} (A : BlockMat d) (X : BlockVec d) : BlockVec d

Action of a block matrix on a pair of spatial vectors.

Equations

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

@[simp]

theorem Homogenization.blockMatVecMul_fst {d : ℕ} (A : BlockMat d) (p q : Vec d) : (blockMatVecMul A (p, q)).1 = matVecMul A.upperLeft p + matVecMul A.upperRight q

@[simp]

theorem Homogenization.blockMatVecMul_snd {d : ℕ} (A : BlockMat d) (p q : Vec d) : (blockMatVecMul A (p, q)).2 = matVecMul A.lowerLeft p + matVecMul A.lowerRight q

noncomputable def Homogenization.symmPart {d : ℕ} (A : Mat d) : Mat d

Symmetric part of a spatial matrix.

Equations

• Homogenization.symmPart A i j = (A i j + A j i) / 2

noncomputable def Homogenization.skewPart {d : ℕ} (A : Mat d) : Mat d

Skew-symmetric part of a spatial matrix.

Equations

• Homogenization.skewPart A i j = (A i j - A j i) / 2

theorem Homogenization.symmPart_eq_smul_add_transpose {d : ℕ} (A : Mat d) : symmPart A = (1 / 2) • (A + matTranspose A)

theorem Homogenization.skewPart_eq_smul_sub_transpose {d : ℕ} (A : Mat d) : skewPart A = (1 / 2) • (A - matTranspose A)

@[simp]

theorem Homogenization.matTranspose_symmPart {d : ℕ} (A : Mat d) : matTranspose (symmPart A) = symmPart A

@[simp]

theorem Homogenization.matTranspose_skewPart {d : ℕ} (A : Mat d) : matTranspose (skewPart A) = -skewPart A