The limit of one vanishing-viscosity family #
For the family κ_j = t ε_{2j+1}^p of weak solutions with cosine data: uniformly Cauchy in sup-L²
(pair_bound), hence convergent to a transport weak solution Θ (transportLimit_contract),
and HolderTimeL2Le (μ/2) η-close for large j (uniformHolder_contract and interpolation).
theorem
AVenhance.Infra.FullTheorem.eps_rpow_tendsto
{β : ℝ}
{Λ : ℕ}
(hβ1 : 1 < β)
(hβ2 : β < 4 / 3)
(hΛ : 2 ^ 7 ≤ Λ)
{x : ℝ}
(hx : 0 < x)
{u : ℕ → ℕ}
(hu : Filter.Tendsto u Filter.atTop Filter.atTop)
:
Filter.Tendsto (fun (j : ℕ) => epsilon β Λ (u j) ^ x) Filter.atTop (nhds 0)
theorem
AVenhance.Infra.FullTheorem.uniform_cauchy_of_pair
{f : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{g : ℕ → ℝ}
(hg : Filter.Tendsto g Filter.atTop (nhds 0))
{J : ℕ}
(hpair : ∀ j ≥ J, ∀ j' ≥ j, ∀ s ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => f j s x - f j' s x) ≤ g j)
(η : ℝ)
:
theorem
AVenhance.Infra.FullTheorem.family_limit
(β C₀ : ℝ)
:
∃ (μ : ℝ) (Λ₄ : ℝ),
0 < μ ∧ ∀ (I : Ingredients β),
I.Czeta ≤ C₀ →
I.Cxi ≤ C₀ →
I.Chat ≤ C₀ →
Λ₄ ≤ ↑I.Λ →
∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ),
IsStreamSeq I Φ →
∀ (φ : ℝ → Homogenization.Vec 2 → ℝ),
(∀ (t : ℝ) (x : Homogenization.Vec 2),
Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) →
∀ (n : ℕ),
1 ≤ n →
∀ (c t : ℝ),
t = 1 / 2 ∨ t = 2 →
∀ (θ : ℝ → ℝ → Homogenization.Vec 2 → ℝ),
(∀ (j : ℕ),
IsWeakSolution (streamVel φ) (kfam β I.Λ t j)
(fun (x : Homogenization.Vec 2) => c * Real.cos (2 * Real.pi * ↑n * x 0))
(θ (kfam β I.Λ t j))) →
∃ (Θ : ℝ → Homogenization.Vec 2 → ℝ),
IsTransportWeakSolution (streamVel φ)
(fun (x : Homogenization.Vec 2) => c * Real.cos (2 * Real.pi * ↑n * x 0)) Θ ∧ (∀ s ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (Θ s)) ∧ (∀ (η : ℝ),
0 < η →
∃ (N : ℕ),
∀ j ≥ N,
∀ s ∈ Set.Icc 0 1,
√(l2NormSq fun (x : Homogenization.Vec 2) =>
θ (kfam β I.Λ t j) s x - Θ s x) ≤ η) ∧ ∀ (η : ℝ),
0 < η →
∀ᶠ (j : ℕ) in Filter.atTop, HolderTimeL2Le (μ / 2) η fun (s : ℝ) (x : Homogenization.Vec 2) =>
θ (kfam β I.Λ t j) s x - Θ s x