Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.RelativeError.IteratesForcingSmooth

RelativeError item 13: smoothness and periodicity of the iterate forcing TForcing #

The forcing βˆ‡Β·((𝐊_m βˆ’ ΞΊ_{m-1} I + 𝐬_{m-1}) βˆ‡T^{(i-1)}) is jointly C^∞ on [0,∞) Γ— ℝ² and β„€Β²-periodic in x, whenever T^{(i-1)} is C^∞ on [0,∞) Γ— ℝ² (resp. periodic).

Slices of jointly smooth functions on the closed half-space #

source
theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_slice_eq_fderivWithin {F : ℝ Γ— Homogenization.Vec 2 β†’ ℝ} {s : Set (ℝ Γ— Homogenization.Vec 2)} (t : ℝ) (x : Homogenization.Vec 2) (hs : βˆ€ (y : Homogenization.Vec 2), (t, y) ∈ s) (hF : DifferentiableWithinAt ℝ F s (t, x)) (j : Fin 2) :
spaceGrad (fun (y : Homogenization.Vec 2) => F (t, y)) x j = (fderivWithin ℝ F s (t, x)) (0, Homogenization.basisVec j)

The spatial gradient of a slice, as a partial derivative of the joint map within s.

source
theorem AVenhance.Infra.Section5.RelativeError.slice_contDiff_of_contDiffOn {T : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hT : ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 Γ—Λ’ Set.univ)) {t : ℝ} (ht : 0 ≀ t) :
ContDiff ℝ (β†‘βŠ€) (T t)

A function C^∞ on [0,∞) Γ— ℝ² is C^∞ on each slice at a nonnegative time.

source
theorem AVenhance.Infra.Section5.RelativeError.contDiffOn_spaceGrad_slice {F : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hF : ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => F p.1 p.2) (Set.Ici 0 Γ—Λ’ Set.univ)) (j : Fin 2) :
ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => spaceGrad (F p.1) p.2 j) (Set.Ici 0 Γ—Λ’ Set.univ)

Each component of the spatial gradient of a C^∞-on-[0,∞) Γ— ℝ² function is again C^∞ on [0,∞) Γ— ℝ², jointly in (t,x).

Matrix-valued smoothness helpers #

source
theorem AVenhance.Infra.Section5.RelativeError.contDiff_matrix_of_entries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop β„•βˆž} {f : E β†’ Matrix (Fin 2) (Fin 2) ℝ} (h : βˆ€ (i j : Fin 2), ContDiff ℝ n fun (x : E) => f x i j) :
ContDiff ℝ n f
source
theorem AVenhance.Infra.Section5.RelativeError.contDiff_matrix_entry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop β„•βˆž} {f : E β†’ Matrix (Fin 2) (Fin 2) ℝ} (h : ContDiff ℝ n f) (i j : Fin 2) :
ContDiff ℝ n fun (x : E) => f x i j

Joint smoothness of 𝐬_{m-1} #

source
theorem AVenhance.Infra.Section5.RelativeError.Kmat_joint_contDiff {Ξ² : ℝ} (I : Ingredients Ξ²) {m : β„•} (hm : 1 ≀ m) {ΞΊ : ℝ} (hΞΊ : 0 < ΞΊ) :
ContDiff ℝ β†‘βŠ€ fun (p : ℝ Γ— Homogenization.Vec 2) => I.Kmat ΞΊ m p.1

The matrix 𝐊_m(t) is jointly C^∞ in (t,x) (constant in x).

source
theorem AVenhance.Infra.Section5.RelativeError.sMat_joint_contDiff {Ξ² : ℝ} (I : Ingredients Ξ²) {Ξ¦ : β„• β†’ ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hΞ¦ : IsStreamSeq I Ξ¦) {m : β„•} (hm : 1 ≀ m) {ΞΊm : ℝ} (hΞΊm : 0 < ΞΊm) :
ContDiff ℝ β†‘βŠ€ fun (p : ℝ Γ— Homogenization.Vec 2) => I.sMat hΞ¦ m ΞΊm p.1 p.2

The averaged coefficient 𝐬_{m-1} is jointly C^∞ in (t,x) on all of ℝ Γ— ℝ².

Smoothness of the forcing #

source
theorem AVenhance.Infra.Section5.RelativeError.TForcing_contDiffOn {Ξ² : ℝ} (I : Ingredients Ξ²) {Ξ¦ : β„• β†’ ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hΞ¦ : IsStreamSeq I Ξ¦) {m : β„•} (hm : 1 ≀ m) {ΞΊm : ℝ} (hΞΊm : 0 < ΞΊm) (ΞΊprev : ℝ) {Tprev : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hT : ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => Tprev p.1 p.2) (Set.Ici 0 Γ—Λ’ Set.univ)) :
ContDiffOn ℝ (β†‘βŠ€) (fun (p : ℝ Γ— Homogenization.Vec 2) => I.TForcing hΞ¦ m ΞΊm ΞΊprev Tprev p.1 p.2) (Set.Ici 0 Γ—Λ’ Set.univ)

The iterate forcing is jointly C^∞ on [0,∞) Γ— ℝ² if the previous iterate is.

Periodicity of the forcing #

source
theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_isZ2Periodic {f : Homogenization.Vec 2 β†’ ℝ} (hf : IsZ2Periodic f) :
IsZ2Periodic (spaceGrad f)

The spatial gradient of a β„€Β²-periodic function is β„€Β²-periodic.

source
theorem AVenhance.Infra.Section5.RelativeError.sMat_isZ2Periodic {Ξ² : ℝ} (I : Ingredients Ξ²) {Ξ¦ : β„• β†’ ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hΞ¦ : IsStreamSeq I Ξ¦) (m : β„•) (ΞΊm t : ℝ) :
IsZ2Periodic (I.sMat hΦ m κm t)

The averaged coefficient 𝐬_{m-1}(t) is β„€Β²-periodic.

source
theorem AVenhance.Infra.Section5.RelativeError.TForcing_periodic {Ξ² : ℝ} (I : Ingredients Ξ²) {Ξ¦ : β„• β†’ ℝ β†’ Homogenization.Vec 2 β†’ ℝ} (hΞ¦ : IsStreamSeq I Ξ¦) {m : β„•} (_hm : 1 ≀ m) (ΞΊm ΞΊprev : ℝ) {Tprev : ℝ β†’ Homogenization.Vec 2 β†’ ℝ} {t : ℝ} (_hTt : ContDiff ℝ 1 (Tprev t)) (hTp : IsZ2Periodic (Tprev t)) :
IsZ2Periodic (I.TForcing hΦ m κm κprev Tprev t)

The iterate forcing is β„€Β²-periodic in x whenever the previous iterate is.