Cube Average

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def Homogenization.cubeAverage {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : ℝ

Scalar integral average over a triadic cube.

Equations

• Homogenization.cubeAverage Q f = (Homogenization.cubeVolume Q)⁻¹ * ∫ (x : Homogenization.Vec d) in Homogenization.cubeSet Q, f x

noncomputable def Homogenization.cubeAverageVec {d : ℕ} (Q : TriadicCube d) (f : Vec d → Vec d) : Vec d

Componentwise vector average over a triadic cube.

Equations

• Homogenization.cubeAverageVec Q f i = Homogenization.cubeAverage Q fun (x : Homogenization.Vec d) => f x i

noncomputable def Homogenization.cubeAverageMat {d : ℕ} (Q : TriadicCube d) (f : Vec d → Mat d) : Mat d

Entrywise matrix average over a triadic cube.

Equations

• Homogenization.cubeAverageMat Q f i j = Homogenization.cubeAverage Q fun (x : Homogenization.Vec d) => f x i j

noncomputable def Homogenization.cubeProjection {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ℝ) : Vec d → ℝ

Piecewise constant projection onto averages on depth-j triadic descendants.

Equations

• Homogenization.cubeProjection Q j f x = ∑ R ∈ Homogenization.descendantsAtDepth Q j, if x ∈ Homogenization.cubeSet R then Homogenization.cubeAverage R f else 0

noncomputable def Homogenization.cubeIncrement {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ℝ) : Vec d → ℝ

Difference between successive triadic average projections, starting with the coarse projection.

Equations

• Homogenization.cubeIncrement Q 0 f = Homogenization.cubeProjection Q 0 f
• Homogenization.cubeIncrement Q n.succ f = fun (x : Homogenization.Vec d) => Homogenization.cubeProjection Q (n + 1) f x - Homogenization.cubeProjection Q n f x