Proof of the separation statement #
separation_contract : SeparationContract with c₀ = 1/10000. Assembly of the energy-loss bounds
Separation.energy_loss_bounds for the two solutions, the gap E₁ - E₂ ≥ 3.2 κ₁ t λ E₀
(using κ₂ ≥ 3 κ₁), and Separation.sqrt_gap.
theorem
AVenhance.Infra.FullTheorem.Contracts.initial_energies
{Ψ θ : ℝ → Homogenization.Vec 2 → ℝ}
{κ : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ)
(hθ₀ : ContDiff ℝ (↑⊤) θ₀)
:
Separation.gradE θ 0 = gradNormSq (spaceGrad θ₀) ∧ Separation.hessE θ 0 = hessNormSq θ₀ ∧ Separation.wEnergy [] θ 0 = l2NormSq θ₀
The initial values of the three energies are the corresponding quantities of θ₀.