Iterates TFinite Norm #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_T_finite_norm_triangle
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => θprev z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
{K : ℕ}
(hK : K ≤ Nstar β)
(v w : List (Fin 2))
{s : ℝ}
(hs : 0 ≤ s)
:
√(l2NormSq (iterateSpatialWord v (T K s))) + √κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (T K t))) ≤ ∑ i ∈ Finset.range (K + 1),
(√(l2NormSq (iterateSpatialWord v (iterateIncrement T i s))) + √κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (iterateIncrement T i t))))
Finite telescoping gives the actual T mixed-norm triangle inequality. The scalar and gradient words may be chosen independently.
theorem
AVenhance.Infra.Section4.iterate_T_gradient_triangle
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => θprev z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
{K : ℕ}
(hK : K ≤ Nstar β)
(w : List (Fin 2))
:
√κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (T K t))) ≤ ∑ i ∈ Finset.range (K + 1),
√κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (iterateIncrement T i t)))
The T zeroth-order branch uses only integrated gradient norms.