The differential energy identity and inequality for w = u - v

For t > 0 write w = u - v, f = advDiffOp b κ v. Then ∂ₜ w = κ Δw - b·∇w - f, the energy satisfies d/dt ∫ w² = -2κ ∫ |∇w|² - 2 ∫ f w, and (when ‖f t‖_{HDot⁻¹} < ∞) the Young inequality gives d/dt ∫ w² + κ ∫ |∇w|² ≤ ‖f t‖²_{HDot⁻¹} / κ.

structure AVenhance.Infra.Section5.Integration.Energy.ForcedSetup (φ : ℝ → Homogenization.Vec 2 → ℝ) (κ : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (u v : ℝ → Homogenization.Vec 2 → ℝ) : Prop

The standing hypotheses of the forced energy estimate.

• hφ : IsAdmissibleStream φ
• hκ : 0 < κ
• hu : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ u
• hv : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => v p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)
• hvs (t : ℝ) : 0 ≤ t → ContDiff ℝ (↑⊤) (v t)
• hvp (t : ℝ) : 0 ≤ t → IsZ2Periodic (v t)

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.hu1 {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : ContDiffOn ℝ 1 (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.hv1 {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : ContDiffOn ℝ 1 (Function.uncurry v) (Set.Ici 0 ×ˢ Set.univ)

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.hw1 {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : ContDiffOn ℝ 1 (Function.uncurry fun (t : ℝ) (x : Homogenization.Vec 2) => u t x - v t x) (Set.Ici 0 ×ˢ Set.univ)

The error w = u - v is jointly C¹ on [0,∞) × ℝ².

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.hw1Open {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : ContDiffOn ℝ 1 (Function.uncurry fun (t : ℝ) (x : Homogenization.Vec 2) => u t x - v t x) Classical.classicalPositiveTimeDomain

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.wSlice {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => u t x - v t x

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.wPeriodic {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) {t : ℝ} (ht : 0 ≤ t) : IsZ2Periodic fun (x : Homogenization.Vec 2) => u t x - v t x

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.drift_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : Continuous (Function.uncurry (streamVel φ))

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.forcing_continuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v p.1 p.2) Classical.classicalPositiveTimeDomain

The forcing is jointly continuous on (0,∞) × ℝ².

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.deriv_w_eq {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : deriv (fun (s : ℝ) => u s x - v s x) t = κ * spaceLap (fun (y : Homogenization.Vec 2) => u t y - v t y) x - Homogenization.vecDot (streamVel φ t x) (spaceGrad (fun (y : Homogenization.Vec 2) => u t y - v t y) x) - advDiffOp (streamVel φ) κ v t x

The equation for the error w = u - v at positive times.