Energy identity for finite Fourier coefficients of weak solutions #
Each real Fourier coefficient satisfies a scalar integral equation. Applying the finite-path energy identity coefficientwise and summing gives the exact energy identity for every Fourier cutoff.
noncomputable def
AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierCoefficientPath
(N : ℕ)
(u : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
:
The finite vector of real Fourier coefficients of a weak path at time t.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Parabolic.WeakUniqueness.weak_solution_finite_fourier_energy_identity
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{f : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
{D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hu : IsWeakSolutionGrad b κ f u D)
(hf : Homogenization.MemL2On unitCube f)
(N : ℕ)
{t : ℝ}
(ht : t ∈ Set.Icc 0 1)
:
‖weakFourierCoefficientPath N u t‖ ^ 2 + ∫ (s : ℝ) in 0..t, 2 * ∑ i : Fin (FourierGalerkin.RealFourierDimension N),
weakModePairing u
(FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) s * weakModeForcing b κ D
(FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) s = ‖weakFourierCoefficientPath N u 0‖ ^ 2
Coefficientwise integration by parts in time gives the exact energy balance for the finite real Fourier projection of a weak solution.