Short-time stability of the gradient energy #
(9/10) ‖∇θ₀‖² ≤ ‖∇θ(r)‖² ≤ (11/10) ‖∇θ₀‖² on [0,t], from the differential inequalities of
Derivs and the abstract chain G_two_sided.
theorem
AVenhance.Infra.FullTheorem.Separation.gradE_continuousOn
{Ψ θ : ℝ → Homogenization.Vec 2 → ℝ}
{κ : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ)
:
ContinuousOn (gradE θ) (Set.Ici 0)
theorem
AVenhance.Infra.FullTheorem.Separation.hessE_continuousOn
{Ψ θ : ℝ → Homogenization.Vec 2 → ℝ}
{κ : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ)
{T : ℝ}
(hT : 0 ≤ T)
:
ContinuousOn (hessE θ) (Set.Icc 0 T)
theorem
AVenhance.Infra.FullTheorem.Separation.gradE_two_sided
{Ψ θ : ℝ → Homogenization.Vec 2 → ℝ}
{κ Lu lam t : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
(hΨ : IsAdmissibleStream Ψ)
(hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ)
(hκ : 0 < κ)
(hLu0 : 0 ≤ Lu)
(ht : 0 < t)
(ht1 : t ≤ 1)
(hLu :
∀ s ∈ Set.Icc 0 1,
∀ (x : Homogenization.Vec 2) (i k : Fin 2),
|spaceGrad (fun (y : Homogenization.Vec 2) => streamVel Ψ s y k) x i| ≤ Lu)
(hLt : Lu * t ≤ 1 / 10000)
(hkl : κ * t * lam ≤ 1 / 10000)
(hinit : hessE θ 0 ≤ lam * gradE θ 0)
(r : ℝ)
: