Joint continuity of cutoff1, twistie1, twistie4, twistie5, normie3 for a smooth T

Each term is a locally finite (in time) sum over odd cutoff indices of products of jointly smooth fields, with at most one spatial derivative of the C¹/C² fields ∇ΧTilde, ∇Χ, ∇X⁻¹, and div/gradDiv of jointly C^∞ fields.

Odd sums weighted by ξ_{m,k}

theorem AVenhance.Infra.Section5.Contracts.tc_xi_tsum_continuousOn {β : ℝ} (I : Ingredients β) (m : ℕ) {g : { k : ℤ // Odd k } → ℝ → Homogenization.Vec 2 → ℝ} (hg : ∀ (k : { k : ℤ // Odd k }), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => g k p.1 p.2) tcU) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) p.1 * g k p.1 p.2) tcU

∑_k ξ_{m,k}(t) g_k(t,x) is continuous when each g_k is.

theorem AVenhance.Infra.Section5.Contracts.tc_vecDot_mulVec_continuousOn {u : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {M : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {w : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => u p.1 p.2 i) tcU) (hM : ∀ (i j : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => M p.1 p.2 i j) tcU) (hw : ∀ (j : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => w p.1 p.2 j) tcU) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (u p.1 p.2) ((M p.1 p.2).mulVec (w p.1 p.2))) tcU

A product of continuous coordinates, in the shape ⟨u, M v⟩.

theorem AVenhance.Infra.Section5.Contracts.tc_vecDot_continuousOn {u v : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hu : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => u p i) tcU) (hv : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => v p i) tcU) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (u p) (v p)) tcU

A product of continuous coordinates, in the shape ⟨u, v⟩.

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

The coordinates of the twisted corrector are continuous.

theorem AVenhance.Infra.Section5.Contracts.tc_G_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => G I hΦ m T l p.1 p.2 i) tcU

The coordinates of the pulled gradient are continuous.

theorem AVenhance.Infra.Section5.Contracts.tc_flowGradK_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (i j : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => flowGradK I hΦ m k p.1 p.2 i j) tcU

The coordinates of the flow-gradient matrix are continuous.

cutoff1

theorem AVenhance.Infra.Section5.Contracts.tc_cutoff1_continuousOn {β : ℝ} (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)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => cutoff1 I hΦ m κm T p.1 p.2) tcU

cutoff1 of a smooth T is jointly continuous on the open half space.

Matrix-vector helper

theorem AVenhance.Infra.Section5.Contracts.tc_mulVec_contDiffOn {n : WithTop ℕ∞} {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hA : ∀ (i j : Fin 2), ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => A p.1 p.2 i j) tcU) (hv : ∀ (j : Fin 2), ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => v p.1 p.2 j) tcU) (i : Fin 2) : ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => (A p.1 p.2).mulVec (v p.1 p.2) i) tcU

Coordinates of A v are jointly C^n when those of A and v are.

theorem AVenhance.Infra.Section5.Contracts.tc_KmatAddSMat_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (i j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => (I.Kmat κm m p.1 + I.sMat hΦ m κm p.1 p.2) i j) tcU

The averaged forcing matrix 𝐊_m + 𝐬_{m-1} is jointly C^∞.

theorem AVenhance.Infra.Section5.Contracts.tc_spaceGrad_T_contDiffOn {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (T p.1) p.2 j) tcU

The gradient coordinates of a smooth T are jointly C^∞ on the open half space.

twistie1

theorem AVenhance.Infra.Section5.Contracts.tc_twistie1_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => twistie1 I hΦ m κm T p.1 p.2) tcU

twistie1 of a smooth T is jointly continuous on the open half space.

Divergence-form fluxes of twistie4, twistie5

theorem AVenhance.Infra.Section5.Contracts.tc_xi_tsum_vec_contDiffOn {β : ℝ} (I : Ingredients β) (m : ℕ) {n : WithTop ℕ∞} (hn : n ≤ ↑⊤) {g : { k : ℤ // Odd k } → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hg : ∀ (k : { k : ℤ // Odd k }) (j : Fin 2), ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => g k p.1 p.2 j) tcU) (i : Fin 2) : ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => (∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) p.1 • g k p.1 p.2) i) tcU

The i-th coordinate of ∑_k ξ_{m,k}(t) g_k(t,x) is jointly C^n when those of each g_k are.

theorem AVenhance.Infra.Section5.Contracts.tc_twistie4Field_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (i j : Fin 2) : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => (κm • ((gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m (lIdx β I.Λ m k) p.1 z) p.2 - 1) * gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m k p.1 z) (I.xFlowInv hΦ m (lIdx β I.Λ m k) p.1 p.2))) i j) tcU

The matrix field inside the flux of twistie4 is jointly C¹.

theorem AVenhance.Infra.Section5.Contracts.tc_twistie4Flux_contDiffOn {β : ℝ} (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)) (i : Fin 2) : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => (∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) p.1 • (κm • ((gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) p.1 z) p.2 - 1) * gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m (↑k) p.1 z) (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) p.1 p.2))).mulVec (G I hΦ m T (lIdx β I.Λ m ↑k) p.1 p.2)) i) tcU

The flux ∑_k ξ_k D_k G_k of twistie4 is jointly C¹ on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_twistie4_continuousOn {β : ℝ} (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)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => twistie4 I hΦ m κm T p.1 p.2) tcU

twistie4 of a smooth T is jointly continuous on the open half space.

twistie5

theorem AVenhance.Infra.Section5.Contracts.tc_twistie5Field_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (i j : Fin 2) : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => ((1 - (flowGradK I hΦ m k p.1 p.2).transpose) * ((I.hatZetaML m (lIdx β I.Λ m k) p.1 * I.zetaMK m k p.1 * psi β I.Λ m k (I.xFlowInv hΦ m (lIdx β I.Λ m k) p.1 p.2)) • sigmaMat + κm • gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m k p.1 z) (I.xFlowInv hΦ m (lIdx β I.Λ m k) p.1 p.2))) i j) tcU

The matrix field inside the flux of twistie5 is jointly C¹.

theorem AVenhance.Infra.Section5.Contracts.tc_twistie5Flux_contDiffOn {β : ℝ} (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)) (i : Fin 2) : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => (∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) p.1 • ((1 - (flowGradK I hΦ m (↑k) p.1 p.2).transpose) * ((I.hatZetaML m (lIdx β I.Λ m ↑k) p.1 * I.zetaMK m (↑k) p.1 * psi β I.Λ m (↑k) (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) p.1 p.2)) • sigmaMat + κm • gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m (↑k) p.1 z) (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) p.1 p.2))).mulVec (G I hΦ m T (lIdx β I.Λ m ↑k) p.1 p.2)) i) tcU

The flux ∑_k ξ_k E_k G_k of twistie5 is jointly C¹ on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_twistie5_continuousOn {β : ℝ} (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)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => twistie5 I hΦ m κm T p.1 p.2) tcU

twistie5 of a smooth T is jointly continuous on the open half space.

Corrector flux

normie3

theorem AVenhance.Infra.Section5.Contracts.tc_cellFlux_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (i j : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => cellFlux I hΦ m κm k p.1 p.2 i j) tcU

The unpulled cell-flux matrix entries are jointly continuous on the open half space.

theorem AVenhance.Infra.Section5.Contracts.tc_normie3_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => normie3 I hΦ m κm T p.1 p.2) tcU

normie3 of a smooth T is jointly continuous on the open half space.