TUpgrade Consumers Packaging

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_smallness_of_budget_enlargement {e d D : ℝ} (hd : 0 < d) (hdD : d ≤ D) (h : e ≤ (4 * D ^ 3)⁻¹) : e ≤ (4 * d ^ 3)⁻¹

Source smallness persists when the universal budget constant is enlarged.

theorem AVenhance.Infra.Section4.iterate_source_frequency_eq {e : ℝ} (he : 0 < e) (γ D : ℝ) : D * e ^ (-1 - γ / 2) = D / e ^ (1 + γ / 2)

Normalize the source frequency to the length scale in the downstream statements.

theorem AVenhance.Infra.Section4.iterate_ansatz_Tjet_of_positive_jets {β e A : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (he : 0 < e) (h : Section5.RelativeError.PositiveTemperatureJets A (e ^ (1 + gamma β / 2)) (√(l2NormSq θ₀)) u) (i : Fin 2) (s : ℝ) : s ∈ Set.Icc 0 1 → √(l2NormSq fun (x : Homogenization.Vec 2) => spaceGrad (u s) x i) ≤ A ^ 2 * √(l2NormSq θ₀) * e ^ (-(1 + gamma β / 2))

First-gradient shape of section_four_ansatz_bound.hTjet from the exact positive-temperature jet carrier.