Separation at one level, with the time and scale bookkeeping #
level_sep: classical solutions θ₁, θ₂ with the same admissible drift Ψ, the same cosine-type
datum, and diffusivities κ₁ ≤ κ₂ ∈ [3κ₁, 5κ₁] that are ≍ E^{β+γ} are separated at the time
t = c′ E^{2-β} by ≳ E^δ ‖θ₀‖.
The body of SeparationContract with the constant c₀ a parameter.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.FullTheorem.NoSel.level_sep
{c₀ Cb k0 K0 c' E β γ δ c₁ lam κ₁ κ₂ : ℝ}
{Ψ : ℝ → Homogenization.Vec 2 → ℝ}
(hS : SepWith c₀)
(hΨ : IsAdmissibleStream Ψ)
(hCb : 0 ≤ Cb)
(hLu :
∀ t ∈ Set.Icc 0 1,
∀ (x : Homogenization.Vec 2) (i j : Fin 2),
|spaceGrad (fun (y : Homogenization.Vec 2) => streamVel Ψ t y i) x j| ≤ Cb * E ^ (β - 2))
{θ₀ : Homogenization.Vec 2 → ℝ}
(hθ₀ : ContDiff ℝ (↑⊤) θ₀)
(hper : IsZ2Periodic θ₀)
(hlam0 : 0 ≤ lam)
(hG : gradNormSq (spaceGrad θ₀) = lam * l2NormSq θ₀)
(hH : hessNormSq θ₀ ≤ lam * gradNormSq (spaceGrad θ₀))
(hE : 0 < E)
(hE1 : E ≤ 1)
(hβ2 : β ≤ 2)
(hc₁ : 0 < c₁)
(hc' : 0 < c')
(hc'1 : c' ≤ 1)
(hCbc : Cb * c' ≤ c₀)
(hKc : K0 * c' ≤ c₀)
(hK0 : 0 ≤ K0)
(hk0 : 0 ≤ k0)
(hκ₁ : k0 * E ^ (β + γ) ≤ κ₁)
(hκ₁pos : 0 < κ₁)
(hκ₂ : κ₂ ≤ K0 * E ^ (β + γ))
(h3 : 3 * κ₁ ≤ κ₂)
(h5 : κ₂ ≤ 5 * κ₁)
(hlam1 : lam * E ^ (2 + γ) ≤ 1)
(hlam2 : E ^ δ ≤ c₁ ^ 2 * (lam * E ^ (2 + γ)))
{θ₁ θ₂ : ℝ → Homogenization.Vec 2 → ℝ}
(hs1 : IsClassicalSol (streamVel Ψ) κ₁ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ₁)
(hs2 : IsClassicalSol (streamVel Ψ) κ₂ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ₂)
: