RelativeError: mean-zero data are controlled by total dissipation

The slice Poincare inequality is averaged against the exact classical energy identity. This avoids requiring a derivative at the initial time.

theorem AVenhance.Infra.Section5.RelativeError.MeanZeroEstimate.interval_energy_average_bound {E G : ℝ → ℝ} {κ Cₚ E₀ : ℝ} (hκ : 0 ≤ κ) (hG : ContinuousOn G (Set.Icc 0 1)) (hGnonneg : ∀ t ∈ Set.Icc 0 1, 0 ≤ G t) (henergy : ∀ t ∈ Set.Icc 0 1, E t + 2 * κ * ∫ (s : ℝ) in 0..t, G s = E₀) (hP : ∀ t ∈ Set.Icc 0 1, E t ≤ Cₚ * G t) : E₀ ≤ (Cₚ + 2 * κ) * ∫ (s : ℝ) in 0..1, G s

theorem AVenhance.Infra.Section5.RelativeError.classical_meanZero_initial_energy_le {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) (hκ : 0 < κ) (hκ1 : κ ≤ 1) (hmean : ∫ (x : Homogenization.Vec 2) in unitCube, g x = 0) : l2NormSq g ≤ 3 * ∫ (t : ℝ) in 0..1, classicalCellGradientEnergy u t

Mean-zero smooth classical data have initial squared norm bounded by the time-integrated gradient energy, uniformly for diffusivity at most one.

theorem AVenhance.Infra.Section5.RelativeError.classical_meanZero_initial_l2_le {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) (hκ : 0 < κ) (hκ1 : κ ≤ 1) (hmean : ∫ (x : Homogenization.Vec 2) in unitCube, g x = 0) : √(l2NormSq g) ≤ √3 * (√κ)⁻¹ * (√κ * √(∫ (t : ℝ) in 0..1, classicalCellGradientEnergy u t))

Norm form of the mean-zero dissipation estimate, with S = sqrt κ * ‖∇u‖_{L²((0,1)×cell)}.