Joint continuity of the leading matrix F

Source: enhance.tex 8298–8302. Near each time only finitely many modes ξ_{m,k} are active (their supports have length (5/2)τ_m), so F is locally a finite sum of jointly continuous matrix fields ξ_{m,k}(t) (I + ∇Χ_{m,k}(t,·)) ∘ X⁻¹_{m-1,l_k}(t,x).

theorem AVenhance.Infra.Section5.LeftToShow.epsilon_ne_zero {β : ℝ} (I : Ingredients β) (m : ℕ) : epsilon β I.Λ m ≠ 0

theorem AVenhance.Infra.Section5.LeftToShow.continuous_gradMatrix_chiMK {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) {k : ℤ} (hk : Odd k) : Continuous fun (q : ℝ × Homogenization.Vec 2) => gradMatrix (I.chiMK κ m k q.1) q.2

A single mode's corrector gradient is jointly continuous in time and position.

theorem AVenhance.Infra.Section5.LeftToShow.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.LeftToShow.continuous_xiMK {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : Continuous (I.xiMK m k)

noncomputable def AVenhance.Infra.Section5.LeftToShow.leadingSummand {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (q : ℝ × Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

The k-th summand of F, as a function of the spacetime point.

Equations

• AVenhance.Infra.Section5.LeftToShow.leadingSummand I hΦ m κm k q = I.xiMK m k q.1 • (1 + AVenhance.gradMatrix (I.chiMK κm m k q.1) (I.xFlowInv hΦ m (AVenhance.lIdx β I.Λ m k) q.1 q.2))

theorem AVenhance.Infra.Section5.LeftToShow.continuous_leadingSummand {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {k : ℤ} (hk : Odd k) : Continuous (leadingSummand I hΦ m κm k)

theorem AVenhance.Infra.Section5.LeftToShow.leadingMatrix_continuous {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (_hm : 1 ≤ m) {κm : ℝ} (_hκm : 0 < κm) : Continuous fun (p : ℝ × Homogenization.Vec 2) => leadingMatrix I hΦ m κm p.1 p.2

Joint continuity of F (finitely many active modes near each time).