TUpgrade Consumers Jets

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.TUpgradeConsumersJets.fin_cast_of_heq {a b : ℕ} {j : Fin a} {k : Fin b} (hab : a = b) (h : j ≍ k) : Fin.cast hab j = k

theorem AVenhance.Infra.Section4.iterate_positive_temperature_jets_of_word_bound {u : ℝ → Homogenization.Vec 2 → ℝ} {κ S P D ρ A : ℝ} (hu : ∀ t ∈ Set.Icc 0 1, ContDiff ℝ (↑⊤) (u t)) (hS : 0 ≤ S) (hP : 0 ≤ P) (hD : 0 ≤ D) (hρ : 0 < ρ) (hPA : P ≤ A) (hDA : D ≤ A) (hb : ∀ (v w : List (Fin 2)), v.length = w.length → 1 ≤ v.length → ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → √(l2NormSq (iterateSpatialWord v (u t))) + √κ * √(spaceTimeGradNormSq fun (s : ℝ) => spaceGrad (iterateSpatialWord w (u s))) ≤ S * P * ↑v.length.factorial * (D / ρ) ^ v.length) : Section5.RelativeError.PositiveTemperatureJets A ρ S u

Convert the positive ordered-word part of the upgrade to the exact Frechet-jet carrier used by RelativeLeaves.