Iterates TDischarge

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.Infra.Section4.iterateReducedSourceConstant (β Ccut c Ck Cflow Rflow Cθ : ℝ) : ℝ

A concrete enlargement of the l.V constant discharges the coefficient smallness premises; all constants are chosen before ingredients and data.

Equations

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

theorem AVenhance.Infra.Section4.iterate_T_upgrade_of_theta_flow_material (β Ccut : ℝ) : ∃ (c : ℝ) (Ck : ℝ), 0 < c ∧ c < Ck ∧ ∀ (I : Ingredients β), I.Czeta ≤ Ccut → I.Cxi ≤ Ccut → I.Chat ≤ Ccut → ∀ {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) {m : ℕ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}, I.IsTIterates hΦ m (I.kappaAt κ m (M - m)) (I.kappaAt κ (m - 1) (M - (m - 1))) θ₀ θprev T → IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaAt κ (m - 1) (M - (m - 1))) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → 2 ≤ m → m ≤ M → κ ∈ permittedInterval β I.Λ M → (∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) → (∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t)) → ∀ (Cflow Rflow Cθ Rθ C₀ N : ℝ), 0 < N → 0 ≤ Cflow → 256 ≤ Rflow → 0 < Rθ → iterateReducedSourceConstant β Ccut c Ck Cflow Rflow Cθ ≤ C₀ → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ → epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹ → (∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (j k : Fin 2), |(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * epsilon β I.Λ (m - 1) ^ (2 * delta β)) → (∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (p : List (Fin 2)), 1 ≤ p.length → ∀ (j k : Fin 2), |iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) j k) x| ≤ Cflow * ↑p.length.factorial * (Rflow / epsilon β I.Λ (m - 1)) ^ p.length) → iterateCoordinateEnergyProfile θprev (I.kappaAt κ (m - 1) (M - (m - 1))) N (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0 → √(I.kappaAt κ (m - 1) (M - (m - 1))) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T (Nstar β) t)) ≤ N * (1 + C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * ↑(Nstar β) * ↑(2 * Nstar β).factorial) ∧ ∀ (v w : List (Fin 2)), v.length = w.length → 1 ≤ v.length → ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (iterateSpatialWord v (T (Nstar β) s))) + √(I.kappaAt κ (m - 1) (M - (m - 1))) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (T (Nstar β) t))) ≤ N * 4 ^ Nstar β * ↑(2 * Nstar β).factorial * ↑v.length.factorial * (4 * C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) ^ v.length

Actual T upgrade with stream-regularity/diffusivity-recursion and the two-error mean and Kmat inputs discharged. The positive amplitude is abstract; the theta base uses only its zeroth gradient energy and positive scalar derivative energies.