Finite Leibniz regularity for the word-indexed Galerkin equation.

theorem AVenhance.Infra.Classical.GalerkinHorizonSmoothnessRhs.classicalBoundaryWordDerivative_add (w : List (Fin 2)) (f g : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (classicalWordDerivative w fun (x : Homogenization.Vec 2) => f x + g x) = fun (x : Homogenization.Vec 2) => classicalWordDerivative w f x + classicalWordDerivative w g x

theorem AVenhance.Infra.Classical.GalerkinHorizonSmoothnessRhs.classicalBoundaryWordDerivative_append (v w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : classicalWordDerivative v (classicalWordDerivative w f) = classicalWordDerivative (v ++ w) f

theorem AVenhance.Infra.Classical.classicalBoundarySpaceLap_contDiff (u : Homogenization.Vec 2 → ℝ) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceLap u x

theorem AVenhance.Infra.Classical.classicalBoundaryTransport_contDiff (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (classicalTransport b u)

noncomputable def AVenhance.Infra.Classical.classicalGalerkinUnitWordRhsExpansion (φ : ℝ → Homogenization.Vec 2 → ℝ) (κ : ℝ) (F : ℝ → Homogenization.Vec 2 → ℝ) (f : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : ℝ

The right-hand side with the product rule fully expanded in joint space-time coordinates.

Equations

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

theorem AVenhance.Infra.Classical.GalerkinHorizonSmoothnessRhs.classicalBoundaryListMapSum_contDiffOn {α : Type u_1} (k : ℕ) (S : Set (ℝ × Homogenization.Vec 2)) (L : List α) (g : α → ℝ × Homogenization.Vec 2 → ℝ) (hg : ∀ a ∈ L, ContDiffOn ℝ (↑k) (g a) S) : ContDiffOn ℝ (↑k) (List.map g L).sum S

theorem AVenhance.Infra.Classical.GalerkinHorizonSmoothnessRhs.classicalBoundaryWordRhsExpansion_contDiffOn (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) classicalHalfSpace) (f : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ) (S : Set (ℝ × Homogenization.Vec 2)) (hS : S = Set.Icc 0 1 ×ˢ Set.univ) (k : ℕ) (hk : ∀ (w : List (Fin 2)), ContDiffOn ℝ (↑k) (f w) S) (w : List (Fin 2)) : ContDiffOn ℝ (↑k) (classicalGalerkinUnitWordRhsExpansion φ κ F f w) S

theorem AVenhance.Infra.Classical.classicalGalerkinUnitWordRhs_eq_expansion_on (φ : ℝ → 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) (hp : p ∈ Set.Icc 0 1 ×ˢ Set.univ) : classicalGalerkinUnitWordRhs φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w p = classicalGalerkinUnitWordRhsExpansion φ κ F (classicalGalerkinUnitWordFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per) w p

On the closed unit slab the equation word equals its finite spatial Leibniz expansion.

theorem AVenhance.Infra.Classical.classicalGalerkinUnitWordRhs_contDiffOn_of_family (φ : ℝ → 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 θ₀) (S : Set (ℝ × Homogenization.Vec 2)) (hS : S = Set.Icc 0 1 ×ˢ Set.univ) (k : ℕ) (hf : ∀ (w : List (Fin 2)), ContDiffOn ℝ (↑k) (classicalGalerkinUnitWordFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) S) (w : List (Fin 2)) : ContDiffOn ℝ (↑k) (classicalGalerkinUnitWordRhs φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) S