Local-finiteness and time differentiation for the ansatz cutoff sum.

def AVenhance.Infra.Section5.xiMKNearSupport {β : ℝ} (I : Ingredients β) (m : ℕ) (t ρ : ℝ) : Set ℤ

The indices whose cutoff may be nonzero in a fixed time neighborhood.

Equations

• AVenhance.Infra.Section5.xiMKNearSupport I m t ρ = {k : ℤ | ∃ s ∈ Set.Ioo (t - ρ) (t + ρ), I.xiMK m k s ≠ 0}

theorem AVenhance.Infra.Section5.FrozenAnsatzTime.xiMK_nonzero_time_bound {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) {s : ℝ} (hne : I.xiMK m k s ≠ 0) : |s - ↑k * tau β I.Λ m| ≤ 5 / 4 * tau β I.Λ m

theorem AVenhance.Infra.Section5.xiMKNearSupport_finite {β : ℝ} (I : Ingredients β) (m : ℕ) (t ρ : ℝ) : (xiMKNearSupport I m t ρ).Finite

The cutoff family is uniformly finite on each bounded time neighborhood.

noncomputable def AVenhance.Infra.Section5.xiMKNearSupportFinset {β : ℝ} (I : Ingredients β) (m : ℕ) (t ρ : ℝ) : Finset ℤ

Finite index set controlling the cutoff series near t.

Equations

• AVenhance.Infra.Section5.xiMKNearSupportFinset I m t ρ = ⋯.toFinset

theorem AVenhance.Infra.Section5.FrozenAnsatzTime.xiMK_eq_zero_outside_nearSupport {β : ℝ} (I : Ingredients β) (m : ℕ) (t ρ s : ℝ) (hs : s ∈ Set.Ioo (t - ρ) (t + ρ)) {k : ℤ} (hk : k ∉ xiMKNearSupportFinset I m t ρ) : I.xiMK m k s = 0

theorem AVenhance.Infra.Section5.ansatz_hasDerivAt {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm ρ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (T' H' : ℝ → ℝ) (ξ' : ℤ → ℝ) (χ' G' : ℤ → Homogenization.Vec 2) (hρ : 0 < ρ) (hT : HasDerivAt (fun (s : ℝ) => T s x) (T' t) t) (hH : HasDerivAt (fun (s : ℝ) => I.Hm hΦ m κm T s x) (H' t) t) (hξ : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasDerivAt (I.xiMK m k) (ξ' k) t) (hχ : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasDerivAt (fun (s : ℝ) => I.chiTilde hΦ m κm k s x) (χ' k) t) (hG : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasDerivAt (fun (s : ℝ) => G I hΦ m T (lIdx β I.Λ m k) s x) (G' k) t) : HasDerivAt (fun (s : ℝ) => I.ansatz hΦ m κm T s x) (T' t + ∑ k ∈ xiMKNearSupportFinset I m t ρ, (ξ' k * Homogenization.vecDot (I.chiTilde hΦ m κm k t x) (G I hΦ m T (lIdx β I.Λ m k) t x) + I.xiMK m k t * (Homogenization.vecDot (χ' k) (G I hΦ m T (lIdx β I.Λ m k) t x) + Homogenization.vecDot (I.chiTilde hΦ m κm k t x) (G' k))) + H' t) t

The ansatz time derivative is an ordinary finite product-rule calculation once the individual pulled fields are differentiable. The support finset is uniform on a neighborhood of t, so differentiating the original ℤ-indexed tsum is justified.