Integer-horizon rescaling for the smooth unit-slab Galerkin limit.

def AVenhance.Infra.Classical.classicalGalerkinHorizonStream (N : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) : ℝ → Homogenization.Vec 2 → ℝ

Rescale an admissible stream by an integer time horizon, including the chain-rule factor.

Equations

• AVenhance.Infra.Classical.classicalGalerkinHorizonStream N φ s x = ↑N * φ (↑N * s) x

def AVenhance.Infra.Classical.classicalGalerkinHorizonForcing (N : ℕ) (F : ℝ → Homogenization.Vec 2 → ℝ) : ℝ → Homogenization.Vec 2 → ℝ

Rescale the forcing by the time-chain-rule factor on an integer horizon.

Equations

• AVenhance.Infra.Classical.classicalGalerkinHorizonForcing N F s x = ↑N * F (↑N * s) x

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonStream_admissible (N : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) : IsAdmissibleStream (classicalGalerkinHorizonStream N φ)

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonForcing_smooth (N : ℕ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (Function.uncurry (classicalGalerkinHorizonForcing N F)) (Set.Ici 0 ×ˢ Set.univ)

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonForcing_periodic (N : ℕ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (t : ℝ) : 0 ≤ t → IsZ2Periodic (classicalGalerkinHorizonForcing N F t)

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonStreamVel_eq (N : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (s : ℝ) (x : Homogenization.Vec 2) : streamVel (classicalGalerkinHorizonStream N φ) s x = ↑N • streamVel φ (↑N * s) x

noncomputable def AVenhance.Infra.Classical.classicalGalerkinHorizonLimit (N : ℕ) (hN : 0 < N) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) : ℝ → Homogenization.Vec 2 → ℝ

The Galerkin limit on an arbitrary positive integer horizon, obtained by rescaling the unit-slab construction.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonLimit_periodic (N : ℕ) (hN : 0 < N) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ℝ) : IsZ2Periodic (classicalGalerkinHorizonLimit N hN φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonLimit_initial (N : ℕ) (hN : 0 < N) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (x : Homogenization.Vec 2) : classicalGalerkinHorizonLimit N hN φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per 0 x = θ₀ x

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonLimit_advDiffOp (N : ℕ) (hN : 0 < N) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) {t : ℝ} (ht : t ∈ Set.Ioo 0 ↑N) (x : Homogenization.Vec 2) : advDiffOp (streamVel φ) κ (classicalGalerkinHorizonLimit N hN φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per) t x = F t x