Material Spatial

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Construction.MaterialSpatial.streamVel_component0_iterated_eq {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) : ((iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => streamVel (fun (x : ℝ) (z : Homogenization.Vec 2) => f z) 0 y 0) x) fun (k : Fin n) => Homogenization.basisVec (J k)) = -(iteratedFDeriv ℝ (n + 1) f x) (Fin.snoc (fun (k : Fin n) => Homogenization.basisVec (J k)) (Homogenization.basisVec 1))

theorem AVenhance.Infra.Construction.MaterialSpatial.streamVel_component1_iterated_eq {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) : ((iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => streamVel (fun (x : ℝ) (z : Homogenization.Vec 2) => f z) 0 y 1) x) fun (k : Fin n) => Homogenization.basisVec (J k)) = (iteratedFDeriv ℝ (n + 1) f x) (Fin.snoc (fun (k : Fin n) => Homogenization.basisVec (J k)) (Homogenization.basisVec 0))

theorem AVenhance.Infra.Construction.MaterialSpatial.basisVec_snoc {n : ℕ} (J : Fin n → Fin 2) (j : Fin 2) : Fin.snoc (fun (i : Fin n) => Homogenization.basisVec (J i)) (Homogenization.basisVec j) = fun (k : Fin (n + 1)) => Homogenization.basisVec (Fin.snoc J j k)

theorem AVenhance.Infra.Construction.MaterialSpatial.material_potential_normalization {β : ℝ} {I : Ingredients β} (m p N : ℕ) (hp : 2 ≤ p) (hpN : p ≤ N) : have e := epsilon β I.Λ m; have R := 2 ^ 8 * e⁻¹; have B := 2 ^ 5 * a β I.Λ m * e ^ 2 * ((↑p + 2) ^ 2 / (↑p + 1) ^ 3); have K := 2 ^ (8 * N + 6) * ↑N.factorial; B / ((↑p + 1) ^ 2 / ↑p.factorial * R⁻¹ ^ p) ≤ K * e ^ (β - ↑p)

theorem AVenhance.Infra.Construction.MaterialSpatial.iteratedFDeriv_component {f : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) (i : Fin 2) : ((iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => f y i) x) fun (k : Fin n) => Homogenization.basisVec (J k)) = (iteratedFDeriv ℝ n f x) (fun (k : Fin n) => Homogenization.basisVec (J k)) i

theorem AVenhance.Infra.Construction.MaterialSpatial.iteratedFDeriv_gradient_scalar_eq {g : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (q : ℕ) (x : Homogenization.Vec 2) (J : Fin q → Fin 2) (j : Fin 2) : ((iteratedFDeriv ℝ q (fun (y : Homogenization.Vec 2) => (fderiv ℝ g y) (Homogenization.basisVec j)) x) fun (k : Fin q) => Homogenization.basisVec (J k)) = (iteratedFDeriv ℝ (q + 1) g x) (Fin.snoc (fun (k : Fin q) => Homogenization.basisVec (J k)) (Homogenization.basisVec j))

theorem AVenhance.Infra.Construction.MaterialSpatial.fderiv_component_apply {f : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) (i j : Fin 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => f y i) x) (Homogenization.basisVec j) = (fderiv ℝ f x) (Homogenization.basisVec j) i

theorem AVenhance.Infra.Construction.MaterialSpatial.material_scale_identity_shift2 {β e : ℝ} (he : 0 < e) (n : ℕ) : e ^ (β - (↑n + 2)) = e ^ (β - 2) * e⁻¹ ^ n

theorem AVenhance.Infra.Construction.MaterialSpatial.material_scale_identity {β e : ℝ} (he : 0 < e) (n : ℕ) : e ^ (β - (↑n + 1)) = e ^ (β - 1) * e⁻¹ ^ n