TMaterial Spatial Coefficient

Support for the Armstrong–Vicol anomalous-diffusion formalization.

@[instance_reducible]

def avInfraSection5ContractsTMaterialSpatialCoefficientNormedAddCommGroup1 : NormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ)

Equip the spatial matrix space with its coordinate supremum norm.

Equations

• avInfraSection5ContractsTMaterialSpatialCoefficientNormedAddCommGroup1 = Matrix.normedAddCommGroup

@[instance_reducible]

noncomputable def avInfraSection5ContractsTMaterialSpatialCoefficientNormedSpace2 : NormedSpace ℝ (Matrix (Fin 2) (Fin 2) ℝ)

Real normed-space structure for spatial matrices with the coordinate supremum norm.

Equations

• avInfraSection5ContractsTMaterialSpatialCoefficientNormedSpace2 = Matrix.normedSpace

def AVenhance.Infra.Section5.Contracts.TMaterialSpatialCoefficient.tMaterialFlowBudget (L : ℝ) (n : ℕ) : ℝ

The all-suborder flow budget 40 n! L^n used for the quadratic Leibniz estimate.

Equations

• AVenhance.Infra.Section5.Contracts.TMaterialSpatialCoefficient.tMaterialFlowBudget L n = 40 * ↑n.factorial * L ^ n

theorem AVenhance.Infra.Section5.Contracts.TMaterialSpatialCoefficient.tMaterialFlowBudget_le {L : ℝ} (hL : 0 < L) {n : ℕ} (hn : n ≤ 2) : tMaterialFlowBudget L n ≤ 80 * L ^ n

theorem AVenhance.Infra.Section5.Contracts.TMaterialSpatialCoefficient.tMaterial_split_term_le {L : ℝ} (hL : 0 < L) {w : List (Fin 2)} (hw : w.length ≤ 2) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ Section4.iterateSpatialSplits w) : tMaterialFlowBudget L p.1.length * (tMaterialFlowBudget L p.2.length + if p.2 = [] then 1 else 0) ≤ 6480 * L ^ w.length

Every ordered Leibniz term of the quadratic budget is ≤ 6480 L^k.

theorem AVenhance.Infra.Section5.Contracts.TMaterialSpatialCoefficient.tMaterial_budget_le {L K κ ν : ℝ} (hL : 0 < L) (hK : 0 ≤ K) (hκ : |κ| ≤ ν) {w : List (Fin 2)} (hw : w.length ≤ 2) : Section4.coarseCoeffWordBudget K κ (tMaterialFlowBudget L) w ≤ (160 * K + 103680 * (K + ν)) * L ^ w.length

theorem AVenhance.Infra.Section5.Contracts.tMaterial_coefficient_spatial_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm ν Q L : ℝ} (hκm : 0 < κm) (hν : 0 ≤ ν) (hQ : 0 ≤ Q) (hL : 0 < L) (hκν : |κm| ≤ ν) (hfreq : 2 ^ 10 / epsilon β I.Λ (m - 1) ≤ L) (hK : ∀ (t : ℝ) (i j : Fin 2), |I.Kmat κm m t i j| ≤ Q * ν) (i j : Fin 2) (α : List (Fin 2)) (hα : α.length ≤ 2) (z : Section4.AmnrSpace) : |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (Section4.amnrTemperatureCoefficient I hΦ m κm ν i j) z| ≤ 200000 * (Q + 1) * ν * L ^ α.length

The actual forcing coefficient's spatial orders zero through two from Kmat size, the molecular comparison |κm| ≤ ν, and the proved active flow jets (all suborders, quadratic Leibniz budget). No time/material coefficient jet enters.