Regularity and periodicity of the ansatz θTilde_m

Source: enhance.tex (e.ansatz). With T = T_{m-1} and HTilde_m the only premises:

• ansatz_contDiffOn_two: joint C² regularity on [0,∞) × ℝ². The ξ-sum is locally finite in time (each ξ_{m,k} is supported in a window of length (5/2)τ_m about kτ_m), so near each time it is a finite sum of C² terms: ξ_{m,k} is C^∞, ΧTilde_{m,k} = -corrTime · u ∘ X⁻¹ is C² (corrTime is C², u and X⁻¹ are jointly C^∞) and the transported gradient is jointly C^∞ (transportedGrad_contDiffOn).
• ansatz_slice_contDiff: at a fixed time the ansatz is C^∞ in space.
• ansatz_periodic: at a fixed time the ansatz is ℤ²-periodic.

Smoothness of the shear field and of the twisted corrector

theorem AVenhance.Infra.Section5.Integration.contDiff_uShear' (β : ℝ) (Λ m : ℕ) (k : ℤ) : ContDiff ℝ (↑⊤) (uShear β Λ m k)

The shear field u_{m,k} is C^∞.

theorem AVenhance.Infra.Section5.Integration.chiTilde_component_contDiff_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (i : Fin 2) : ContDiff ℝ 2 fun (p : ℝ × Homogenization.Vec 2) => I.chiTilde hΦ m κm k p.1 p.2 i

Each coordinate of ΧTilde_{m,k} is jointly C² in time and position.

The summands of the ansatz

noncomputable def AVenhance.Infra.Section5.Integration.ansatzSummand {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The k-th summand of the series in the ansatz.

Equations

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

theorem AVenhance.Infra.Section5.Integration.ansatz_eq_summand {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : I.ansatz hΦ m κm T t x = T t x + ∑' (k : ℤ), ansatzSummand I hΦ m κm T k t x + I.Hm hΦ m κm T t x

theorem AVenhance.Infra.Section5.Integration.ansatzSummand_eq_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {k : ℤ} {t : ℝ} (h : I.xiMK m k t = 0) (x : Homogenization.Vec 2) : ansatzSummand I hΦ m κm T k t x = 0

theorem AVenhance.Infra.Section5.Integration.contDiff_xiMK {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : ContDiff ℝ (↑⊤) (I.xiMK m k)

ξ_{m,k} is C^∞.

theorem AVenhance.Infra.Section5.Integration.ansatzSummand_contDiffOn_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => ansatzSummand I hΦ m κm T k p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)

Each summand is jointly C² on [0,∞) × ℝ².

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

Nonvanishing of ξ_{m,k}(t) forces t to lie within (5/4) τ_m of k τ_m.

theorem AVenhance.Infra.Section5.Integration.exists_active_finset {β : ℝ} (I : Ingredients β) (m : ℕ) (t₀ : ℝ) : ∃ (S : Finset ℤ), ∀ k ∉ S, ∀ (t : ℝ), |t - t₀| < 1 → I.xiMK m k t = 0

The finite set of modes that can be active within unit time of t₀.

theorem AVenhance.Infra.Section5.Integration.ansatz_series_contDiffOn_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => ∑' (k : ℤ), ansatzSummand I hΦ m κm T k p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)

Joint C² regularity of the ansatz series on [0,∞) × ℝ².

theorem AVenhance.Infra.Section5.Integration.ansatz_contDiffOn_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (hH : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => I.Hm hΦ m κm T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => I.ansatz hΦ m κm T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)

Joint C² regularity of the ansatz θTilde_m on [0,∞) × ℝ², given C^∞ regularity of the iterate T_{m-1} and C² regularity of HTilde_m.

Fixed-time smoothness

theorem AVenhance.Infra.Section5.Integration.contDiff_spaceGrad_component {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceGrad f x i

The gradient of a C^∞ function is C^∞.

theorem AVenhance.Infra.Section5.Integration.ansatzSummand_slice_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => ansatzSummand I hΦ m κm T k t x

At a fixed time, each summand is C^∞ in the position.

theorem AVenhance.Infra.Section5.Integration.ansatz_slice_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (hHt : ContDiff ℝ (↑⊤) (I.Hm hΦ m κm T t)) : ContDiff ℝ (↑⊤) (I.ansatz hΦ m κm T t)

Fixed-time smoothness of the ansatz: θTilde_m(t) is C^∞ in space.

Periodicity

theorem AVenhance.Infra.Section5.Integration.epsilon_inv_exists_nat (β : ℝ) (Λ m : ℕ) : ∃ (N : ℕ), (epsilon β Λ m)⁻¹ = ↑N

The reciprocal cell length ε_m⁻¹ is a natural number (ε_0 = 1).

theorem AVenhance.Infra.Section5.Integration.AnsatzRegularity.cos_integer_frequency_periodic' (ε : ℝ) {N : ℕ} (hεinv : ε⁻¹ = ↑N) (x : ℝ) (n : ℤ) : Real.cos (2 * Real.pi * (x + ↑n) / ε) = Real.cos (2 * Real.pi * x / ε)

theorem AVenhance.Infra.Section5.Integration.uShear_isZ2Periodic (β : ℝ) (Λ m : ℕ) (k : ℤ) : IsZ2Periodic (uShear β Λ m k)

The shear field u_{m,k} is ℤ²-periodic.

theorem AVenhance.Infra.Section5.Integration.spaceGrad_isZ2Periodic {f : Homogenization.Vec 2 → ℝ} (hf : IsZ2Periodic f) : IsZ2Periodic (spaceGrad f)

The gradient of a ℤ²-periodic function is ℤ²-periodic.

theorem AVenhance.Infra.Section5.Integration.ansatzSummand_isZ2Periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTp : IsZ2Periodic (T t)) : IsZ2Periodic fun (x : Homogenization.Vec 2) => ansatzSummand I hΦ m κm T k t x

Each summand is ℤ²-periodic when T(t) is.

theorem AVenhance.Infra.Section5.Integration.ansatz_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ 1 (T t)) (hTp : IsZ2Periodic (T t)) (hHp : IsZ2Periodic (I.Hm hΦ m κm T t)) : IsZ2Periodic (I.ansatz hΦ m κm T t)

Periodicity of the ansatz: θTilde_m(t) is ℤ²-periodic when T(t) and HTilde_m(t) are.