Regularity #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.coarseCoeff_matrix_mul_contDiff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{n : WithTop ℕ∞}
{K F : E → CoarseMatrix}
(hK : ContDiff ℝ n K)
(hF : ContDiff ℝ n F)
:
Entrywise proof avoids any choice of a matrix operator norm.
theorem
AVenhance.Infra.Section4.coarseCoeffPolynomial_contDiff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{n : WithTop ℕ∞}
{K F : E → CoarseMatrix}
(a b κ : ℝ)
(hK : ContDiff ℝ n K)
(hF : ContDiff ℝ n F)
:
ContDiff ℝ n fun (x : E) => coarseCoeffPolynomial a b κ (K x) (F x)
theorem
AVenhance.Infra.Section4.coarseCoeff_matrix_mul_contDiffOn
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{n : WithTop ℕ∞}
{U : Set E}
{K F : E → CoarseMatrix}
(hK : ContDiffOn ℝ n K U)
(hF : ContDiffOn ℝ n F U)
:
ContDiffOn ℝ n (fun (x : E) => K x * F x) U
The same entrywise polynomial calculus on a closed space-time domain.
theorem
AVenhance.Infra.Section4.coarseCoeffPolynomial_contDiffOn
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{n : WithTop ℕ∞}
{U : Set E}
{K F : E → CoarseMatrix}
(a b κ : ℝ)
(hK : ContDiffOn ℝ n K U)
(hF : ContDiffOn ℝ n F U)
:
ContDiffOn ℝ n (fun (x : E) => coarseCoeffPolynomial a b κ (K x) (F x)) U
theorem
AVenhance.Infra.Section4.CoarseCoeffForm.spatial_contDiff
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hΦ : IsStreamSeq I Φ}
{m : ℕ}
{κ : ℝ}
{s : ℝ → Homogenization.Vec 2 → CoarseMatrix}
(hs : CoarseCoeffForm I hΦ m κ s)
(hm : 1 ≤ m)
(t : ℝ)
{n : WithTop ℕ∞}
(hflow : ∀ (l : ℤ), ContDiff ℝ n (I.flowGrad hΦ m l t))
:
theorem
AVenhance.Infra.Section4.CoarseCoeffForm.joint_contDiff
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hΦ : IsStreamSeq I Φ}
{m : ℕ}
{κ : ℝ}
{s : ℝ → Homogenization.Vec 2 → CoarseMatrix}
(hs : CoarseCoeffForm I hΦ m κ s)
(hm : 1 ≤ m)
(hK : ContDiff ℝ ↑⊤ fun (z : ℝ × Homogenization.Vec 2) => I.Kmat κ m z.1)
(hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : ℝ × Homogenization.Vec 2) => I.flowGrad hΦ m l z.1 z.2)
:
Joint smoothness uses a locally fixed finite window sum.