Energy loss of a classical solution on [0,t]

‖θ₀‖² - ‖θ(t)‖² = 2κ ∫_0^t ‖∇θ‖² lies in [2κ t (9/10) G₀, 2κ t (11/10) G₀], G₀ = ‖∇θ₀‖².

theorem AVenhance.Infra.FullTheorem.Separation.energy_identity {Ψ θ : ℝ → Homogenization.Vec 2 → ℝ} {κ t : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (ht : 0 < t) : wEnergy [] θ 0 - wEnergy [] θ t = 2 * κ * ∫ (s : ℝ) in 0..t, gradE θ s

theorem AVenhance.Infra.FullTheorem.Separation.energy_loss_bounds {Ψ θ : ℝ → 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) : 2 * κ * t * (9 / 10 * gradE θ 0) ≤ wEnergy [] θ 0 - wEnergy [] θ t ∧ wEnergy [] θ 0 - wEnergy [] θ t ≤ 2 * κ * t * (11 / 10 * gradE θ 0)