Iterates Budget Constant Choice

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.Infra.Section4.iterateBudgetScaleConstant (K Ck c H : ℝ) : ℝ

A universal coefficient constant for the three primitive/material scales.

Equations

• AVenhance.Infra.Section4.iterateBudgetScaleConstant K Ck c H = 2 * K * Ck * H + 2 * K * 2 ^ 21 * H + 2 ^ 21 / c

def AVenhance.Infra.Section4.iterateBudgetCoefficientConstant (K Cflow Cmean : ℝ) : ℝ

The actual coefficient profile constant from cutoff averaging.

Equations

• AVenhance.Infra.Section4.iterateBudgetCoefficientConstant K Cflow Cmean = K + 1 + Cmean + (2 * K * Cflow + 4 * (K + 1) * Cflow * (Cflow + 1))

noncomputable def AVenhance.Infra.Section4.iterateBudgetUniversalConstant (K Ck c H Cflow Cmean : ℝ) : ℝ

One constant dominates every loss in the complete energy budgets.

Equations

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

def AVenhance.Infra.Section4.iterateSourceConstant (C Rflow Cθ : ℝ) : ℝ

A concrete source constant closes the corrected budget and both analytic-frequency conditions, and absorbs the theta frequency.

Equations

• AVenhance.Infra.Section4.iterateSourceConstant C Rflow Cθ = max 4 (max (32 * C) (max (8 * |Rflow|) (2 * Cθ)))

theorem AVenhance.Infra.Section4.iterate_budget_scale_constant_bounds {K Ck c H : ℝ} (hK : 0 ≤ K) (hCk : 0 ≤ Ck) (hc : 0 < c) (hH : 0 ≤ H) : 0 ≤ iterateBudgetScaleConstant K Ck c H ∧ 2 * K * Ck * H ≤ iterateBudgetScaleConstant K Ck c H ∧ 2 * K * 2 ^ 21 * H ≤ iterateBudgetScaleConstant K Ck c H ∧ 2 ^ 21 / c ≤ iterateBudgetScaleConstant K Ck c H

theorem AVenhance.Infra.Section4.iterate_budget_universal_constant_bounds {K Ck c H Cflow Cmean : ℝ} (hK : 0 ≤ K) (hc : 0 < c) (hH : 0 ≤ H) : have Cs := iterateBudgetScaleConstant K Ck c H; have Ccoef := iterateBudgetCoefficientConstant K Cflow Cmean; have C := iterateBudgetUniversalConstant K Ck c H Cflow Cmean; 0 ≤ C ∧ 24 * amnrMaterialMajorantConstant Ccoef Cs Cs Cs ≤ C ∧ 24 * (iterateFirstMaterialCoefficient Cs Ccoef + 384 * Cs ^ 2 + 32 * Ccoef ^ 2) ≤ C ∧ 48 * 2 ^ 19 / c ≤ C ∧ 24 * (16 * 32 ^ 2 * 4 * 256 ^ 4) / c ^ 2 ≤ C ∧ 24 * 8 * 2 * K * 2 ^ 21 * H ≤ C

theorem AVenhance.Infra.Section4.iterate_source_constant_bounds (C Rflow Cθ : ℝ) : 1 ≤ iterateSourceConstant C Rflow Cθ ∧ 32 * C ≤ iterateSourceConstant C Rflow Cθ ∧ 4 * Rflow ≤ iterateSourceConstant C Rflow Cθ ∧ 2 * Cθ ≤ iterateSourceConstant C Rflow Cθ ∧ 4 ≤ iterateSourceConstant C Rflow Cθ

theorem AVenhance.Infra.Section4.iterate_source_constant_doubled_radius (C Rflow Cθ : ℝ) : 4 * (2 * Rflow) ≤ iterateSourceConstant C Rflow Cθ

LeftJacobian's doubled flow radius is absorbed by the same chosen source constant.