the energy identity in the carriers

Translates the cell-integral identities of BaseEnergyIdentity into l2NormSq, gradNormSq (over unitCube) and spaceTimeGradNormSq (over timeCube), and adds the mean-zero Poincaré inequality along the solution.

theorem AVenhance.Infra.Section5.RelativeError.l2NormSq_eq_cell (f : Homogenization.Vec 2 → ℝ) : l2NormSq f = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x ^ 2

theorem AVenhance.Infra.Section5.RelativeError.gradNormSq_spaceGrad_eq_cellGrad (f : ℝ → Homogenization.Vec 2 → ℝ) (s : ℝ) : gradNormSq (spaceGrad (f s)) = cellGrad f s

theorem AVenhance.Infra.Section5.RelativeError.classical_energy_hasDerivAt {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, θ s x ^ 2) (-(2 * κ) * cellGrad θ t) t

theorem AVenhance.Infra.Section5.RelativeError.classical_cell_energy_identity {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) {T : ℝ} (hT : 0 ≤ T) : (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, θ T x ^ 2) - ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g x ^ 2 = ∫ (s : ℝ) in 0..T, -(2 * κ) * cellGrad θ s

The integrated energy identity in cell form.

theorem AVenhance.Infra.Section5.RelativeError.classical_energy_identity_frozen {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) {t : ℝ} (ht : 0 ≤ t) : l2NormSq (θ t) + 2 * κ * ∫ (s : ℝ) in 0..t, gradNormSq (spaceGrad (θ s)) = l2NormSq g

The integrated energy identity in the carriers, for every t ≥ 0.

theorem AVenhance.Infra.Section5.RelativeError.gradNormSq_continuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) {T : ℝ} (hT : 0 ≤ T) : ContinuousOn (fun (s : ℝ) => gradNormSq (spaceGrad (θ s))) (Set.Icc 0 T)

theorem AVenhance.Infra.Section5.RelativeError.gradNormSq_nonneg' (f : Homogenization.Vec 2 → ℝ) : 0 ≤ gradNormSq (spaceGrad f)

theorem AVenhance.Infra.Section5.RelativeError.spaceTimeGradNormSq_eq_intervalIntegral {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) : (spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θ t) x) = ∫ (s : ℝ) in 0..1, gradNormSq (spaceGrad (θ s))

Fubini: the space-time gradient norm is the time integral of the slice norms.