Generic tools for the flux contracts

Locally finite tsums of jointly smooth families, the order-shifting spatial gradient on the open half space, and the local-in-time finiteness of the ζ_{m,k} and ξ̂_{m,l} cutoff families.

@[reducible, inline]

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

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

Equations

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

theorem AVenhance.Infra.Section5.Contracts.tf_contDiffOn_tsum {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : WithTop ℕ∞} {U : Set (ℝ × Homogenization.Vec 2)} (f : ι → ℝ × Homogenization.Vec 2 → F) (P : ι → ℝ → Prop) (hact : ∀ (t₀ : ℝ), ∃ (S : Finset ι), ∀ k ∉ S, ∀ (t : ℝ), |t - t₀| < 1 → P k t) (hzero : ∀ (k : ι) (q : ℝ × Homogenization.Vec 2), P k q.1 → f k q = 0) (hf : ∀ (k : ι), ContDiffOn ℝ n (f k) U) : ContDiffOn ℝ n (fun (q : ℝ × Homogenization.Vec 2) => ∑' (k : ι), f k q) U

A tsum over a family whose terms vanish outside a finite set, uniformly for times within one unit of any given time, is as smooth as its terms.

theorem AVenhance.Infra.Section5.Contracts.tf_active_odd {P : ℤ → ℝ → Prop} (h : ∀ (t₀ : ℝ), ∃ (S : Finset ℤ), ∀ k ∉ S, ∀ (t : ℝ), |t - t₀| < 1 → P k t) (t₀ : ℝ) : ∃ (S : Finset { k : ℤ // Odd k }), ∀ k ∉ S, ∀ (t : ℝ), |t - t₀| < 1 → P (↑k) t

Odd-subtype version of local-in-time finiteness.

theorem AVenhance.Infra.Section5.Contracts.tf_exists_active {τ ρ : ℝ} (hτ : 0 < τ) {f : ℤ → ℝ → ℝ} (hf : ∀ (l : ℤ) (t : ℝ), f l t ≠ 0 → |t - ↑l * τ| ≤ ρ) (t₀ : ℝ) : ∃ (S : Finset ℤ), ∀ l ∉ S, ∀ (t : ℝ), |t - t₀| < 1 → f l t = 0

A family on the lattice kτ whose members vanish outside |t - kτ| ≤ ρ is locally finite in time.

theorem AVenhance.Infra.Section5.Contracts.tf_zetaMK_ne_zero_abs_le {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (t : ℝ) (hne : I.zetaMK m k t ≠ 0) : |t - ↑k * tau β I.Λ m| ≤ 2 / 3 * tau β I.Λ m

ζ_{m,k} is supported in |t - kτ_m| ≤ (2/3)τ_m.

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

Local-in-time finiteness of the ζ_{m,k} family.

theorem AVenhance.Infra.Section5.Contracts.tf_hatXiML_active {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t₀ : ℝ) : ∃ (S : Finset ℤ), ∀ l ∉ S, ∀ (t : ℝ), |t - t₀| < 1 → I.hatXiML m l t = 0

Local-in-time finiteness of the ξ̂_{m,l} family.

Spatial derivatives on the open half space

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

On the open half space the spatial gradient components of a jointly C^n function are jointly C^m, m + 1 ≤ n.

theorem AVenhance.Infra.Section5.Contracts.tf_vecDiv_continuousOn {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hV : ∀ (i : Fin 2), ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => V p.1 p.2 i) (Set.Ioi 0 ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => vecDiv (V p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)

The divergence of a jointly C² vector field is jointly continuous on the open half space.

Matrix-vector smoothness

theorem AVenhance.Infra.Section5.Contracts.tf_mulVec_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {s : Set E} {A : E → Matrix (Fin 2) (Fin 2) ℝ} {v : E → Homogenization.Vec 2} (hA : ∀ (i j : Fin 2), ContDiffOn ℝ n (fun (e : E) => A e i j) s) (hv : ∀ (j : Fin 2), ContDiffOn ℝ n (fun (e : E) => v e j) s) (i : Fin 2) : ContDiffOn ℝ n (fun (e : E) => (A e).mulVec (v e) i) s