RelativeError: classical periodic energy and mean identities #
These are the energy and mean bridges for the smooth torus solution used in the RelativeError trace estimate. The spatial transport and Laplacian integrations by parts reuse the established periodic calculus.
noncomputable def
AVenhance.Infra.Section5.RelativeError.classicalCellGradientEnergy
(u : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
:
The spatial Dirichlet energy of a classical solution at a fixed time, computed on the half-open torus cell.
Equations
Instances For
theorem
AVenhance.Infra.Section5.RelativeError.classical_slice_laplacian_continuous
{u : ℝ → Homogenization.Vec 2 → ℝ}
{t : ℝ}
(hu : ContDiff ℝ (↑⊤) (u t))
:
Continuous (spaceLap (u t))
theorem
AVenhance.Infra.Section5.RelativeError.classical_solution_energy_derivative
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{g : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hb : Flow.SmoothPeriodicField b)
(hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0)
(hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u)
{t : ℝ}
(ht : 0 < t)
:
HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u s x ^ 2)
(-2 * κ * classicalCellGradientEnergy u t) t
The classical PDE gives the periodic energy derivative at every positive time.
theorem
AVenhance.Infra.Section5.RelativeError.classical_solution_energy_identity
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{g : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hb : Flow.SmoothPeriodicField b)
(hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0)
(hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u)
{t : ℝ}
(ht : 0 < t)
(ht1 : t ≤ 1)
:
(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u t x ^ 2) + 2 * κ * ∫ (s : ℝ) in 0..t, classicalCellGradientEnergy u s = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g x ^ 2
Integrating the classical energy derivative from the initial trace gives the exact periodic energy identity.