Glue compatible smooth Galerkin limits on increasing integer horizons.

noncomputable def AVenhance.Infra.Classical.classicalGlueHorizonFamily (family : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

Select the first integer horizon extending past a nonnegative time; use zero before time zero.

Equations

• AVenhance.Infra.Classical.classicalGlueHorizonFamily family t x = if 0 ≤ t then family (⌊t⌋₊ + 1) t x else 0

theorem AVenhance.Infra.Classical.classicalGlueHorizonFamily_apply_of_nonneg (family : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (ht : 0 ≤ t) : classicalGlueHorizonFamily family t x = family (⌊t⌋₊ + 1) t x

theorem AVenhance.Infra.Classical.classicalGlueHorizonFamily_fun_of_nonneg (family : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (ht : 0 ≤ t) : classicalGlueHorizonFamily family t = family (⌊t⌋₊ + 1) t

theorem AVenhance.Infra.Classical.classicalClassicalSol_of_consistent_horizon_family (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) (F : ℝ → Homogenization.Vec 2 → ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (family : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hsmooth : ∀ (N : ℕ), 0 < N → ContDiffOn ℝ (↑⊤) (Function.uncurry (family N)) (Set.Icc 0 ↑N ×ˢ Set.univ)) (hperiodic : ∀ (N : ℕ), 0 < N → ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (family N t)) (hinitial : ∀ (N : ℕ), 0 < N → ∀ (x : Homogenization.Vec 2), family N 0 x = θ₀ x) (hpde : ∀ (N : ℕ), 0 < N → ∀ t ∈ Set.Ioo 0 ↑N, ∀ (x : Homogenization.Vec 2), advDiffOp b κ (family N) t x = F t x) (hcompatible : ∀ (M N : ℕ), M ≤ N → ∀ t ∈ Set.Icc 0 ↑M, family M t = family N t) : ∃ (θ : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol b κ F θ₀ θ

Compatible smooth solutions on every integer horizon glue to a global classical solution. The hypotheses are local in time: they do not assume the global conclusion.