RelativeError: mean preservation and mean-zero energy control

The mean is conserved by the classical periodic equation. This supplies the mean-zero hypothesis for the Fourier Poincare inequality at each time slice.

theorem AVenhance.Infra.Section5.RelativeError.MeanZeroEnergy.classical_solution_time_partial_eq_pde {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : Classical.classicalTimePartial u (t, x) = κ * spaceLap (u t) x - Homogenization.vecDot (b t x) (spaceGrad (u t) x)

theorem AVenhance.Infra.Section5.RelativeError.MeanZeroEnergy.integral_unitCell_laplacian_zero {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, spaceLap f x = 0

theorem AVenhance.Infra.Section5.RelativeError.MeanZeroEnergy.integral_unitCell_transport_mean_zero {b : Homogenization.Vec 2 → Homogenization.Vec 2} {f : Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hbp : ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => b x i) (hdiv : ∀ (x : Homogenization.Vec 2), vecDiv b x = 0) (hf : ContDiff ℝ (↑⊤) f) (hfp : IsZ2Periodic f) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (b x) (spaceGrad f x) = 0

theorem AVenhance.Infra.Section5.RelativeError.MeanZeroEnergy.classical_time_partial_continuousOn {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) Classical.classicalPositiveTimeDomain) : ContinuousOn (Classical.classicalTimePartial u) Classical.classicalPositiveTimeDomain

theorem AVenhance.Infra.Section5.RelativeError.classical_solution_mean_derivative_zero {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) 0 t

The spatial integral of the time derivative vanishes at every positive time for a smooth periodic classical solution.

theorem AVenhance.Infra.Section5.RelativeError.classical_solution_mean_preserved {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 : t ∈ Set.Icc 0 1) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u t x = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g x

The mean of a smooth periodic classical solution is conserved on the unit time interval.