The integrated energy inequality on a positive-time interval [s,t] #
For 0 < s ≤ t ≤ 1:
∫ w(t)² + κ ∫_s^t ∫ |∇w|² ≤ ∫ w(s)² + κ⁻¹ ‖f‖²_{L²(0,1;HDot⁻¹)}, for w = u - v with v only
jointly C² on (0,∞) × ℝ². Reduces to the Energy development through the cutoff
cutoffV s v.
theorem
AVenhance.Infra.Section5.Integration.EnergyIoi.sub_le_integral_of_deriv_le_Ioo
{E D h : ℝ → ℝ}
{s t : ℝ}
(hs : 0 < s)
(hst : s ≤ t)
(hEd : ∀ (x : ℝ), 0 < x → HasDerivAt E (D x) x)
(hDc : ContinuousOn D (Set.Ioi 0))
(hh : IntervalIntegrable h MeasureTheory.volume s t)
(hineq : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo s t), D x ≤ h x)
:
Integrated differential inequality on a compact subinterval of (0,∞); the inequality is only
needed almost everywhere on the open interval.
theorem
AVenhance.Infra.Section5.Integration.EnergyIoi.IoiSetup.interval_bound
{φ : ℝ → Homogenization.Vec 2 → ℝ}
{κ : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{u v : ℝ → Homogenization.Vec 2 → ℝ}
(S : IoiSetup φ κ θ₀ u v)
(hfin : (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x) ≠ ⊤)
{s t : ℝ}
(hs : 0 < s)
(hst : s ≤ t)
(ht : t ≤ 1)
:
(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, (u t x - v t x) ^ 2) + κ * ∫ (r : ℝ) in s..t, Energy.errGrad u v r ≤ (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, (u s x - v s x) ^ 2) + (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x).toReal ^ 2 / κ
The integrated forced energy inequality on [s,t] ⊆ (0,1].