Iterates Discharge Bounds

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.Infra.Section4.iterateRatioConstant (β Ck : ℝ) : ℝ

Uniform ratio coefficient, covering the interior diffusivity-recursion estimate and the terminal step.

Equations

• AVenhance.Infra.Section4.iterateRatioConstant β Ck = max 1 (max Ck (AVenhance.Infra.Section3.kappaPrimeEndpointExpratConstant β))

noncomputable def AVenhance.Infra.Section4.iterateDischargeThreshold (β Ccut Ck : ℝ) : ℝ

The coefficient smallness threshold is fixed before choosing ingredients.

Equations

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

noncomputable def AVenhance.Infra.Section4.iterateKmatConstant (β Ccut : ℝ) : ℝ

The zeroth Kmat entry coefficient after one-step enhancement.

Equations

• AVenhance.Infra.Section4.iterateKmatConstant β Ccut = 160 / 9 * (1 + ↑(AVenhance.Nstar β) * Ccut)

theorem AVenhance.Infra.Section4.iterate_chain_upgrade_inputs {β Ccut Ck C₀ κ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ Ccut) (hh : I.Chat ≤ Ccut) {m M : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) (hκ : 0 < κ) (hPerm : κ ∈ permittedInterval β I.Λ M) (hCk : 0 ≤ Ck) (hC₀ : 1 ≤ C₀) (hthreshold : iterateDischargeThreshold β Ccut Ck ≤ C₀) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹) (hA5 : ∀ (j : ℕ), 2 ≤ j → j < M → epsilon β I.Λ j ^ 2 / (I.kappaAt κ j (M - j) * tau β I.Λ j) ≤ Ck * epsilon β I.Λ (j - 1) ^ (4 * delta β)) : (∀ (t : ℝ) (j k : Fin 2), |I.Kmat (I.kappaAt κ m (M - m)) m t j k| ≤ iterateKmatConstant β Ccut * I.kappaAt κ (m - 1) (M - (m - 1))) ∧ epsilon β I.Λ m ^ 2 ≤ I.kappaAt κ m (M - m) * tau β I.Λ m / 2 ∧ iterateMeanErrorBound I (I.kappaAt κ m (M - m)) m ≤ I.kappaAt κ (m - 1) (M - (m - 1)) * iterateMeanScaleConstant β Ccut (iterateRatioConstant β Ck) * epsilon β I.Λ (m - 1) ^ (2 * delta β)

Package the three cheap inputs of the actual T upgrade. The diffusivity-recursion ratio premise is stated explicitly here.