The middle term: same drift, two diffusivities; the two vanishing-viscosity families

noncomputable def AVenhance.Infra.FullTheorem.kfam (β : ℝ) (Λ : ℕ) (t : ℝ) (j : ℕ) : ℝ

The diffusivity family κ_j = t ε_{2j+1}^{p}, p = 2β/(qβ+1).

Equations

• AVenhance.Infra.FullTheorem.kfam β Λ t j = t * AVenhance.epsilon β Λ (2 * j + 1) ^ (2 * β / (AVenhance.q β + 1))

theorem AVenhance.Infra.FullTheorem.kfam_mem {β : ℝ} {Λ : ℕ} {t : ℝ} (ht : t = 1 / 2 ∨ t = 2) (j : ℕ) (hε : 0 ≤ epsilon β Λ (2 * j + 1)) : kfam β Λ t j ∈ permittedInterval β Λ (2 * j + 1)

theorem AVenhance.Infra.FullTheorem.kfam_mem_permissible {β : ℝ} {Λ : ℕ} {t : ℝ} (ht : t = 1 / 2 ∨ t = 2) (j : ℕ) (hε : 0 ≤ epsilon β Λ (2 * j + 1)) : kfam β Λ t j ∈ permissibleSet β Λ

theorem AVenhance.Infra.FullTheorem.sqrt_l2_tri {u v w : Homogenization.Vec 2 → ℝ} (hu : Homogenization.MemL2On unitCube u) (hv : Homogenization.MemL2On unitCube v) (hw : Homogenization.MemL2On unitCube w) : √(l2NormSq fun (x : Homogenization.Vec 2) => u x - w x) ≤ √(l2NormSq fun (x : Homogenization.Vec 2) => u x - v x) + √(l2NormSq fun (x : Homogenization.Vec 2) => v x - w x)

Triangle inequality through an intermediate L² function.

theorem AVenhance.Infra.FullTheorem.sqrt_l2_comm (u v : Homogenization.Vec 2 → ℝ) : √(l2NormSq fun (x : Homogenization.Vec 2) => u x - v x) = √(l2NormSq fun (x : Homogenization.Vec 2) => v x - u x)

theorem AVenhance.Infra.FullTheorem.middle_bound {Ψ : ℝ → Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) {a b D L e : ℝ} (ha : 0 < a) (hb : 0 < b) (hD : 0 < D) (h1 : |Real.log (a / D) - L| ≤ e) (h2 : |Real.log (b / D) - L| ≤ e) (he : 2 * e ≤ 1) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hper : IsZ2Periodic θ₀) {θ θ' : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel Ψ) a (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (hθ' : IsClassicalSol (streamVel Ψ) b (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ') {t : ℝ} (ht : t ∈ Set.Icc 0 1) : √(l2NormSq fun (x : Homogenization.Vec 2) => θ t x - θ' t x) ≤ 4 * e * √(l2NormSq θ₀)

Two classical solutions with the same drift and flip-flop-close diffusivities.