Generic tools for the joint continuity of the pointwise §5.1 terms

Everything is stated on the open half space tcU = (0,∞) × ℝ².

• tc_contDiffOn_tsum: a locally finite tsum of C^n functions is C^n;
• tc_odd_contDiffOn_tsum: the same for the {k // Odd k} sums weighted by ξ_{m,k} (or its time derivative), using exists_active_finset;
• tc_spaceGrad_contDiffOn: the spatial gradient of a jointly C^{n+1} field is jointly C^n;
• divergence, gradDiv, matDiv and composition with the inverse flow of jointly smooth fields.

@[reducible, inline]

abbrev AVenhance.Infra.Section5.Contracts.tcU : Set (ℝ × Homogenization.Vec 2)

The open half space (0,∞) × ℝ².

Equations

• AVenhance.Infra.Section5.Contracts.tcU = Set.Ioi 0 ×ˢ Set.univ

theorem AVenhance.Infra.Section5.Contracts.tcU_isOpen : IsOpen tcU

theorem AVenhance.Infra.Section5.Contracts.tcU_uniqueDiffOn : UniqueDiffOn ℝ tcU

Locally finite sums

theorem AVenhance.Infra.Section5.Contracts.tc_contDiffOn_tsum {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : WithTop ℕ∞} {s : Set E} {g : ι → E → F} (hg : ∀ (i : ι), ContDiffOn ℝ n (g i) s) (hloc : ∀ x ∈ s, ∃ (S : Finset ι), ∀ᶠ (y : E) in nhds x, ∀ i ∉ S, g i y = 0) : ContDiffOn ℝ n (fun (y : E) => ∑' (i : ι), g i y) s

A locally finite sum of C^n functions on a set is C^n there.

theorem AVenhance.Infra.Section5.Contracts.tc_odd_contDiffOn_tsum {β : ℝ} (I : Ingredients β) (m : ℕ) {n : WithTop ℕ∞} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : { k : ℤ // Odd k } → ℝ × Homogenization.Vec 2 → F} (hg : ∀ (k : { k : ℤ // Odd k }), ContDiffOn ℝ n (g k) tcU) (hz : ∀ (k : { k : ℤ // Odd k }) (t : ℝ), (∀ᶠ (s : ℝ) in nhds t, I.xiMK m (↑k) s = 0) → ∀ (x : Homogenization.Vec 2), g k (t, x) = 0) : ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => ∑' (k : { k : ℤ // Odd k }), g k p) tcU

Odd cutoff sums. The summand g k vanishes at (t, x) as soon as ξ_{m,k} vanishes identically near t.

theorem AVenhance.Infra.Section5.Contracts.tc_odd_continuousOn_tsum {β : ℝ} (I : Ingredients β) (m : ℕ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : { k : ℤ // Odd k } → ℝ × Homogenization.Vec 2 → F} (hg : ∀ (k : { k : ℤ // Odd k }), ContinuousOn (g k) tcU) (hz : ∀ (k : { k : ℤ // Odd k }) (t : ℝ), (∀ᶠ (s : ℝ) in nhds t, I.xiMK m (↑k) s = 0) → ∀ (x : Homogenization.Vec 2), g k (t, x) = 0) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => ∑' (k : { k : ℤ // Odd k }), g k p) tcU

Continuity version of tc_odd_contDiffOn_tsum.

theorem AVenhance.Infra.Section5.Contracts.tc_deriv_xiMK_eq_zero {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) {t : ℝ} (h : ∀ᶠ (s : ℝ) in nhds t, I.xiMK m k s = 0) : deriv (I.xiMK m k) t = 0

If ξ_{m,k} vanishes near t, so does its derivative at t.

Spatial gradients and divergences

theorem AVenhance.Infra.Section5.Contracts.tc_spaceGrad_contDiffOn {F : ℝ → Homogenization.Vec 2 → ℝ} {m n : WithTop ℕ∞} (hmn : m + 1 ≤ n) (hF : ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) tcU) (j : Fin 2) : ContDiffOn ℝ m (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (F p.1) p.2 j) tcU

The spatial gradient of a jointly C^n field on the open half space is jointly C^m for m + 1 ≤ n.

theorem AVenhance.Infra.Section5.Contracts.tc_vecDiv_contDiffOn {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {m n : WithTop ℕ∞} (hmn : m + 1 ≤ n) (hV : ∀ (i : Fin 2), ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => V p.1 p.2 i) tcU) : ContDiffOn ℝ m (fun (p : ℝ × Homogenization.Vec 2) => vecDiv (V p.1) p.2) tcU

The divergence of a jointly C^n field is jointly C^m for m + 1 ≤ n.

theorem AVenhance.Infra.Section5.Contracts.tc_gradDiv_contDiffOn {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {m n : WithTop ℕ∞} (hmn : m + 1 + 1 ≤ n) (hV : ∀ (i : Fin 2), ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => V p.1 p.2 i) tcU) (j : Fin 2) : ContDiffOn ℝ m (fun (p : ℝ × Homogenization.Vec 2) => gradDiv V p.1 p.2 j) tcU

The gradient of the divergence of a jointly C^n field is jointly C^m for m + 2 ≤ n.

theorem AVenhance.Infra.Section5.Contracts.tc_comp_xFlowInv {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) {n : WithTop ℕ∞} (hn : n ≤ ↑⊤) {f : ℝ → Homogenization.Vec 2 → ℝ} (hf : ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => f p.1 p.2) tcU) : ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => f p.1 (I.xFlowInv hΦ m l p.1 p.2)) tcU

Composition with the (jointly smooth) inverse flow preserves joint regularity on the open half space, up to order ∞.