Forced energy identity from the mode-path form #
If a path satisfies the Fourier mode-path form of the forced weak equation and its finite Fourier
projections converge in spacetime H¹, the exact forced energy identity holds at every time.
theorem
AVenhance.Infra.Section5.RelativeError.forced_coefficient_normSq_tendsto
{u : ℝ → Homogenization.Vec 2 → ℝ}
{t : ℝ}
(hu : Homogenization.MemL2On unitCube (u t))
:
Filter.Tendsto (fun (N : ℕ) => ‖Parabolic.WeakUniqueness.weakFourierCoefficientPath N u t‖ ^ 2) Filter.atTop
(nhds (l2NormSq (u t)))
Energy of the finite Fourier projection of an L² slice tends to the slice energy.
theorem
AVenhance.Infra.Section5.RelativeError.forced_initial_coefficients
{κ : ℝ}
{f : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
{Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{G : ℝ × Homogenization.Vec 2 → ℝ}
{F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2}
(h : ForcedModePath κ f u Du G F)
(N : ℕ)
:
Parabolic.WeakUniqueness.weakFourierCoefficientPath N u 0 = Parabolic.WeakUniqueness.weakFourierCoefficientPath N (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => f x_1) 0
The initial Fourier coefficients of a forced path are those of its datum.
theorem
AVenhance.Infra.Section5.RelativeError.forced_energy_of_mode_path
{κ : ℝ}
{f : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
{Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{G : ℝ × Homogenization.Vec 2 → ℝ}
{F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2}
(h : ForcedModePath κ f u Du G F)
(hf : Homogenization.MemL2On unitCube f)
(hproj :
Filter.Tendsto
(fun (N : ℕ) =>
∫ (p : ℝ × Homogenization.Vec 2) in timeCube, (u p.1 p.2 - Parabolic.WeakUniqueness.weakFourierModeProjection N u p.1 p.2) ^ 2)
Filter.atTop (nhds 0))
(hprojGrad :
∀ (i : Fin 2),
Filter.Tendsto
(fun (N : ℕ) =>
∫ (p : ℝ × Homogenization.Vec 2) in timeCube, (Du p.1 p.2 i - spaceGrad (Parabolic.WeakUniqueness.weakFourierModeProjection N u p.1) p.2 i) ^ 2)
Filter.atTop (nhds 0))
{t : ℝ}
(ht : t ∈ Set.Icc 0 1)
:
l2NormSq (u t) + 2 * ∫ (p : ℝ × Homogenization.Vec 2) in Parabolic.WeakUniqueness.weakEnergyRegion t, G p * u p.1 p.2 + κ * Homogenization.vecDot (Du p.1 p.2) (Du p.1 p.2) + Homogenization.vecDot (F p) (Du p.1 p.2) = l2NormSq f
Exact forced energy identity for a path with forced mode paths whose finite Fourier
projections converge in spacetime H¹.