The integrated energy inequality for w = u - v

For t ∈ [0,1]: ∫ w(t)² + κ ∫₀ᵗ ∫ |∇w|² ≤ ∫ w(0)² + κ⁻¹ ‖f‖²_{L²(0,1;HDot⁻¹)}.

noncomputable def AVenhance.Infra.Section5.Integration.Energy.errGrad (u v : ℝ → Homogenization.Vec 2 → ℝ) (s : ℝ) : ℝ

Slice energy gradient ∫ |∇u(s) - ∇v(s)|² over the unit cube.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.Integration.Energy.errGrad_nonneg (u v : ℝ → Homogenization.Vec 2 → ℝ) (s : ℝ) : 0 ≤ errGrad u v s

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.errGrad_jointContinuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (u p.1) p.2 - spaceGrad (v p.1) p.2) (Set.Ici 0 ×ˢ Set.univ)

The error gradient is jointly continuous on [0,∞) × ℝ².

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.errGrad_continuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : ContinuousOn (errGrad u v) (Set.Icc 0 1)

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

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.errEnergy_continuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, (u t x - v t x) ^ 2) (Set.Icc 0 1)

Continuity of the error energy on [0,1].

theorem AVenhance.Infra.Section5.Integration.Energy.ForcedSetup.energyRate_continuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, 2 * (u t x - v t x) * deriv (fun (s : ℝ) => u s x - v s x) t) (Set.Ioi 0)

Continuity of the energy rate on (0,∞).

theorem AVenhance.Infra.Section5.Integration.Energy.integrated_energy_bound {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : ForcedSetup φ κ θ₀ u v) (hfin : (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x) ≠ ⊤) (t : ℝ) : t ∈ Set.Icc 0 1 → (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, (u t x - v t x) ^ 2) + κ * ∫ (s : ℝ) in 0..t, errGrad u v s ≤ (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, (u 0 x - v 0 x) ^ 2) + (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x).toReal ^ 2 / κ

The integrated forced energy inequality.