Iterates TAnalytic Assembly #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_T_positive_analytic_of_increment_bounds
{β : ℝ}
(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))
{N L η : ℝ}
(hκ : 0 < κprev)
(hN : 0 ≤ N)
(hL : 0 ≤ L)
(hη : 0 ≤ η)
(hsmall : η ≤ 1 / 4)
(hbase : iterateCoordinateEnergyProfile θprev κprev N L 0)
(hV :
∀ (i : ℕ),
1 ≤ i →
i ≤ Nstar β →
∀ (v w : List (Fin 2)),
v.length = w.length →
∀ (s : ℝ),
0 ≤ s →
s ≤ 1 →
√(l2NormSq (iterateSpatialWord v (iterateIncrement T i s))) + √κprev * √(spaceTimeGradNormSq fun (t : ℝ) =>
spaceGrad (iterateSpatialWord w (iterateIncrement T i t))) ≤ N * iterateAmplitude η i * iterateAnalyticWeight v.length i L)
(v w : List (Fin 2))
(hvw : v.length = w.length)
(hv : 1 ≤ v.length)
{s : ℝ}
(hs : 0 ≤ s)
(hs1 : s ≤ 1)
:
The analytic T upgrade at positive scalar order, with abstract amplitude. This is a finite-sum helper; actual PDE l.V supplies its increment estimates.
theorem
AVenhance.Infra.Section4.iterate_T_zero_gradient_relative_of_increment_bounds
{β : ℝ}
(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))
{N η : ℝ}
(hN : 0 ≤ N)
(hη : 0 ≤ η)
(hsmall : η ≤ 1)
(hzero : √κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (θprev t)) ≤ N)
(hV :
∀ (i : ℕ),
1 ≤ i →
i ≤ Nstar β →
√κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateIncrement T i t)) ≤ N * iterateAmplitude η i * ↑(2 * i).factorial)
:
Zeroth T order is exclusively a gradient estimate; no scalar supremum is present in either its hypotheses or its conclusion.