Slow factor of normie3

slow_{pj} = ξ_k Σ_i (F_k)_{pi} (∇G_k)_{ij} (n3Slow), so that ξ_k frob (F_kᵀ M(Y_k x)) ∇G_k = Σ_{p,j} M_{pj}(Y_k x) · slow_{pj}(x). Here: the termwise and finite-sum representation of normie3, smoothness / periodicity, and the pointwise bound slow² ≲ ε_{m-1}⁻² |∇T|² + |∇∂_0T|² + |∇∂_1T|² (no small factor: |F_k| ≤ 2 only).

noncomputable def AVenhance.Infra.Section5.Contracts.n3Slow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (p j : Fin 2) (x : Homogenization.Vec 2) : ℝ

The slow factor ξ_k Σ_i (F_k)_{pi} (∇G_k)_{ij} of normie3.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.Contracts.n3Slow_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (p j : Fin 2) (h : I.xiMK m k t = 0) : n3Slow I hΦ m T k t p j = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.Contracts.n3_term_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : I.xiMK m k t * frob ((flowGradK I hΦ m k t x).transpose * (I.flux κm m t - cellFlux I hΦ m κm k t x)) (gradG I hΦ m T (lIdx β I.Λ m k) t x) = ∑ p : Fin 2, ∑ j : Fin 2, n3Fast I κm m k t p j (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) * n3Slow I hΦ m T k t p j x

Termwise component form of normie3.

theorem AVenhance.Infra.Section5.Contracts.normie3_eq_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (S : Finset { k : ℤ // Odd k }) (hS : ∀ (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ≠ 0 → k ∈ S) (x : Homogenization.Vec 2) : normie3 I hΦ m κm T t x = ∑ k ∈ S, ∑ p : Fin 2, ∑ j : Fin 2, n3Fast I κm m (↑k) t p j (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x) * n3Slow I hΦ m T (↑k) t p j x

Finite-sum form of normie3 over any set containing the support of ξ_{m,·}(t).

Smoothness and periodicity

theorem AVenhance.Infra.Section5.Contracts.n3Slow_smooth_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (hTp : IsZ2Periodic (T t)) (k : ℤ) (p j : Fin 2) : ContDiff ℝ (↑⊤) (n3Slow I hΦ m T k t p j) ∧ Ergodic.IsZPeriodic (n3Slow I hΦ m T k t p j)

Pointwise bound

theorem AVenhance.Infra.Section5.Contracts.n3_slow_sq {f q gT h0 h1 : ℝ} (hq : 0 ≤ q) (hg : 0 ≤ gT) (h0n : 0 ≤ h0) (h1n : 0 ≤ h1) (hf : |f| ≤ 8 * h0 + 8 * h1 + 32 * (2 ^ 16 * q) * gT) : f ^ 2 ≤ (2 ^ 22 * q) ^ 2 * gT ^ 2 + 14 ^ 2 * (h0 ^ 2 + h1 ^ 2)

Squaring step: |f| ≤ 8 h₀ + 8 h₁ + 32 (2^16 q) g gives f² ≤ (2^22 q)² g² + 14² (h₀² + h₁²).

theorem AVenhance.Infra.Section5.Contracts.n3_slow_pointwise {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (k : ℤ) (p j : Fin 2) (x : Homogenization.Vec 2) : n3Slow I hΦ m T k t p j x ^ 2 ≤ (2 ^ 22 * (epsilon β I.Λ (m - 1))⁻¹) ^ 2 * Homogenization.vecNormSq (spaceGrad (T t) x) + 14 ^ 2 * (Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord [0] (T t)) x) + Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord [1] (T t)) x))

Pointwise bound of the slow factor of normie3: with ε = ε_{m-1}, slow² ≲ ε⁻² |∇T|² + |∇∂_0T|² + |∇∂_1T|² (no small factor).