Joint smoothness of the closed unit-slab Galerkin limit from its spatial word family.

theorem AVenhance.Infra.Classical.GalerkinHorizonSmoothnessProducer.classicalBoundaryClamp_continuous : Continuous classicalGalerkinUnitSlabClamp

theorem AVenhance.Infra.Classical.GalerkinHorizonSmoothnessProducer.classicalBoundaryToTorus_continuous : Continuous (Torus.toUnitTorus 2)

noncomputable def AVenhance.Infra.Classical.classicalGalerkinUnitWordFamily (φ : ℝ → 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 θ₀) : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ

The real spatial derivative word of the limiting Galerkin lift, clamped to the unit slab.

Equations

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

noncomputable def AVenhance.Infra.Classical.classicalGalerkinUnitWordRhs (φ : ℝ → 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 θ₀) : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ

The spatial word of the physical equation right-hand side on the clamped unit slab.

Equations

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

theorem AVenhance.Infra.Classical.classicalGalerkinUnitWordFamily_continuous (φ : ℝ → 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 θ₀) (w : List (Fin 2)) : Continuous (classicalGalerkinUnitWordFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w)

theorem AVenhance.Infra.Classical.classicalGalerkinUnitWordRhs_eq_torusPath (φ : ℝ → 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 θ₀) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : classicalGalerkinUnitWordRhs φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w p = ((classicalGalerkinSmoothWordRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) (classicalGalerkinUnitSlabClamp p.1, Torus.toUnitTorus 2 p.2)).re

theorem AVenhance.Infra.Classical.classicalGalerkinUnitWordRhs_continuous (φ : ℝ → 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 θ₀) (w : List (Fin 2)) : Continuous (classicalGalerkinUnitWordRhs φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w)