Iterates Coordinate Profile

Support for the Armstrong–Vicol anomalous-diffusion formalization.

def AVenhance.Infra.Section4.iterateCoordinateEnergyProfile (u : ℝ → Homogenization.Vec 2 → ℝ) (κ N L : ℝ) (i : ℕ) : Prop

Scalar coordinate energies at every order, with the common prefactor outside the increment amplitude. The homogeneous base has only positive-order scalar energies; its order-zero input is the integrated gradient.

Equations

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

theorem AVenhance.Infra.Section4.iterate_coordinate_profile_of_word_norm {u : ℝ → Homogenization.Vec 2 → ℝ} {κ N L : ℝ} {i : ℕ} (hκ : 0 < κ) (hnorm : ∀ (w : List (Fin 2)) (s : ℝ), 0 ≤ s → s ≤ 1 → (√(l2NormSq (iterateSpatialWord w (u s))) + √κ * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t)))) ^ 2 ≤ N ^ 2 * iterateAnalyticWeight w.length i L ^ 2) : iterateCoordinateEnergyProfile u κ N L i

A proved squared norm estimate supplies the two energies used by the next increment equation.