The forced finite Fourier systems associated with the smooth classical data.

def AVenhance.Infra.Classical.GalerkinProblem.classicalProblemClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Classical.GalerkinProblem.classicalProblemClosedCell = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Classical.GalerkinProblem.classicalProblemClosedCell_compact : IsCompact classicalProblemClosedCell

theorem AVenhance.Infra.Classical.GalerkinProblem.classicalProblem_cube_subset_closedCell : unitCube ⊆ classicalProblemClosedCell

theorem AVenhance.Infra.Classical.GalerkinProblem.classicalProblem_smooth_memL2On {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : ContDiff ℝ (↑⊤) θ₀) : Homogenization.MemL2On unitCube θ₀

def AVenhance.Infra.Classical.GalerkinProblem.classicalForcingJointCell : Set (ℝ × Homogenization.Vec 2)

Compact time-space cell used to control the forcing on the unit time interval.

Equations

• AVenhance.Infra.Classical.GalerkinProblem.classicalForcingJointCell = Set.Icc 0 1 ×ˢ AVenhance.Infra.Classical.GalerkinProblem.classicalProblemClosedCell

theorem AVenhance.Infra.Classical.GalerkinProblem.classicalForcingJointCell_compact : IsCompact classicalForcingJointCell

noncomputable def AVenhance.Infra.Classical.classicalFrozenDriftProblem (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) : Parabolic.FourierGalerkin.FrozenDriftProblem

The classical smooth hypotheses instantiate the finite Fourier data.

Equations

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

noncomputable def AVenhance.Infra.Classical.classicalForcedGalerkinData (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (N : ℕ) : ForcedGalerkinData (Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) ↥Parabolic.FourierGalerkin.SpatialGradientL2

The cutoff Galerkin path forced by the Fourier projection of F.

Equations

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

noncomputable def AVenhance.Infra.Classical.classicalGalerkinCoefficientPath (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (N : ℕ) : C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))

Every smooth cutoff system has its classical forced coefficient path.

Equations

• AVenhance.Infra.Classical.classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N = Classical.choose ⋯

theorem AVenhance.Infra.Classical.classicalGalerkinCoefficientPath_isSolution (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (N : ℕ) : (classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).ode.IsSolution (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N)