instantaneous energy rate of a classical solution #
For an admissible stream φ and a classical solution θ of the homogeneous
advection–diffusion equation, the shifted function θ + c (c constant) has
d/dt ∫_cell (θ + c)² = -2κ ∫_cell |∇θ|² at every positive time. Also: joint smoothness of the
spatial gradient components up to t = 0.
theorem
AVenhance.Infra.Section5.RelativeError.spaceGrad_add_const
(f : Homogenization.Vec 2 → ℝ)
(c : ℝ)
:
spaceGrad ignores additive constants.
theorem
AVenhance.Infra.Section5.RelativeError.spaceLap_add_const
(f : Homogenization.Vec 2 → ℝ)
(c : ℝ)
:
spaceLap ignores additive constants.
theorem
AVenhance.Infra.Section5.RelativeError.spaceGrad_component_contDiffOn
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F : ℝ → Homogenization.Vec 2 → ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol b κ F θ₀ θ)
(i : Fin 2)
:
ContDiffOn ℝ (↑⊤) (Function.uncurry fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θ t) x i)
(Set.Ici 0 ×ˢ Set.univ)
The spatial gradient components of a classical solution are jointly smooth on the closed
half-space t ≥ 0.
theorem
AVenhance.Infra.Section5.RelativeError.BaseEnergyRate.continuous_spaceGrad_component
{f : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(i : Fin 2)
:
Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x i
theorem
AVenhance.Infra.Section5.RelativeError.BaseEnergyRate.continuous_spaceLap
{f : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
:
Continuous (spaceLap f)
theorem
AVenhance.Infra.Section5.RelativeError.BaseEnergyRate.continuous_vecDot'
{f g : Homogenization.Vec 2 → Homogenization.Vec 2}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (x : Homogenization.Vec 2) => Homogenization.vecDot (f x) (g x)
theorem
AVenhance.Infra.Section5.RelativeError.energy_hasDerivAt_of_pde
(φ : ℝ → Homogenization.Vec 2 → ℝ)
(hφ : IsAdmissibleStream φ)
(κ : ℝ)
(w : ℝ → Homogenization.Vec 2 → ℝ)
(hw : ContDiffOn ℝ (↑⊤) (Function.uncurry w) (Set.Ici 0 ×ˢ Set.univ))
(hwper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (w t))
(hPDE :
∀ (t : ℝ),
0 < t →
∀ (x : Homogenization.Vec 2),
Classical.classicalTimePartial w (t, x) - κ * spaceLap (w t) x + Homogenization.vecDot (streamVel φ t x) (spaceGrad (w t) x) = 0)
{t : ℝ}
(ht : 0 < t)
:
HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, w s x ^ 2)
(-(2 * κ) * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad (w t) x) (spaceGrad (w t) x))
t
Energy rate of a smooth periodic solution of w_t - κΔw + b·∇w = 0 with an admissible stream
drift: d/dt ∫_cell w² = -2κ ∫_cell |∇w|² at positive times.
theorem
AVenhance.Infra.Section5.RelativeError.classical_shift_hasDerivAt
(φ : ℝ → Homogenization.Vec 2 → ℝ)
(hφ : IsAdmissibleStream φ)
{κ : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ)
(c : ℝ)
{t : ℝ}
(ht : 0 < t)
:
HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, (θ s x + c) ^ 2)
(-(2 * κ) * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad (θ t) x) (spaceGrad (θ t) x))
t
The shifted classical solution θ + c has the same energy rate.