TwoDiffusivityContract #
Two classical solutions with the same drift and diffusivities κ, κ', same data θ₀:
‖θ(t) - θ'(t)‖² ≤ (κ-κ')²/(4κκ') ‖θ₀‖². With w = θ - θ' and δ = κ - κ',
d/dt ‖w‖² = -2κ‖∇w‖² - 2δ⟨∇w,∇θ'⟩ ≤ δ²/(2κ) ‖∇θ'‖² (Young), and
2κ' ∫₀ᵗ ‖∇θ'‖² ≤ ‖θ₀‖² is the energy identity of θ'.
theorem
AVenhance.Infra.FullTheorem.NoSelectionInputs.young_integral
{f h : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hh : ContDiff ℝ (↑⊤) h)
{κ δ : ℝ}
(hκ : 0 < κ)
:
(-2 * κ * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad f x)) - 2 * δ * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad f x) (spaceGrad h x) ≤ δ ^ 2 / (2 * κ) * ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad h x)
Integrated Young inequality: -2κ ∫|g|² - 2δ ∫ g·h ≤ δ²/(2κ) ∫ |h|².
theorem
AVenhance.Infra.FullTheorem.NoSelectionInputs.diff_energy_le
{Ψ θ θ' : ℝ → Homogenization.Vec 2 → ℝ}
{κ κ' : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
(hΨ : IsAdmissibleStream Ψ)
(hκ : 0 < κ)
(hκ' : 0 < κ')
(hθ : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ)
(hθ' : IsClassicalSol (streamVel Ψ) κ' (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ')
{t : ℝ}
(ht : 0 ≤ t)
:
‖θ(t) - θ'(t)‖² ≤ (κ-κ')²/(4κκ') ‖θ₀‖².