TUpgrade Consumers Scalar Zero #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_T_upgrade_conditional_A3_A5_flow_material_scalar_zero
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(κ : ℝ)
(M : ℕ)
{m : ℕ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m (I.kappaAt κ m (M - m)) (I.kappaAt κ (m - 1) (M - (m - 1))) θ₀ θprev T)
(hθ :
IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaAt κ (m - 1) (M - (m - 1)))
(fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hm : 2 ≤ m)
(hmM : m ≤ M)
(hκtop : 0 < κ)
(hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2)
(hflowp : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t))
(hA3 :
∀ (j : ℕ),
1 ≤ j →
∀ (t : ℝ) (n : ℕ),
2 ≤ n →
barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3)))
{c Ck K Cflow Cmean Rflow Cθ Rθ C₀ N : ℝ}
(hN : 0 < N)
(hc : 0 < c)
(hcC : c < Ck)
(hA5 :
∀ (j : ℕ),
1 ≤ j →
j < M →
c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (M - j) ∧ I.kappaAt κ j (M - j) ≤ Ck * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)))
(hK : 0 ≤ K)
(hCf : 0 ≤ Cflow)
(hCm : 0 ≤ Cmean)
(hRf : 256 ≤ Rflow)
(hRθ : 0 < Rθ)
(hC₀ : iterateSourceConstant (iterateBudgetUniversalConstant K Ck c (2 ^ (-25)) Cflow Cmean) Rflow Cθ ≤ C₀)
(hradius : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ)
(hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹)
(hKm : ∀ (t : ℝ) (j k : Fin 2), |I.Kmat (I.kappaAt κ m (M - m)) m t j k| ≤ K * I.kappaAt κ (m - 1) (M - (m - 1)))
(hcondition : epsilon β I.Λ m ^ 2 ≤ I.kappaAt κ m (M - m) * tau β I.Λ m / 2)
(hMeanScale :
iterateMeanErrorBound I (I.kappaAt κ m (M - m)) m ≤ I.kappaAt κ (m - 1) (M - (m - 1)) * Cmean * epsilon β I.Λ (m - 1) ^ (2 * delta β))
(hzero :
∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (j k : Fin 2), |(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * epsilon β I.Λ (m - 1) ^ (2 * delta β))
(hpositive :
∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (p : List (Fin 2)),
1 ≤ p.length →
∀ (j k : Fin 2),
|iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) j k) x| ≤ Cflow * ↑p.length.factorial * (Rflow / epsilon β I.Λ (m - 1)) ^ p.length)
(hbase :
iterateCoordinateEnergyProfile θprev (I.kappaAt κ (m - 1) (M - (m - 1))) N
(C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0)
(hscalar : ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (θprev s)) ≤ N)
(s : ℝ)
:
theorem
AVenhance.Infra.Section4.iterate_T_upgrade_of_theta_flow_material_scalar_zero
(β Ccut : ℝ)
:
∃ (c : ℝ) (Ck : ℝ),
0 < c ∧ c < Ck ∧ ∀ (I : Ingredients β),
I.Czeta ≤ Ccut →
I.Cxi ≤ Ccut →
I.Chat ≤ Ccut →
∀ {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) {m : ℕ}
{θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ},
I.IsTIterates hΦ m (I.kappaAt κ m (M - m)) (I.kappaAt κ (m - 1) (M - (m - 1))) θ₀ θprev T →
IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaAt κ (m - 1) (M - (m - 1)))
(fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev →
2 ≤ m →
m ≤ M →
κ ∈ permittedInterval β I.Λ M →
(∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) →
(∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t)) →
∀ (Cflow Rflow Cθ Rθ C₀ N : ℝ),
0 < N →
0 ≤ Cflow →
256 ≤ Rflow →
0 < Rθ →
iterateReducedSourceConstant β Ccut c Ck Cflow Rflow Cθ ≤ C₀ →
epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ →
epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹ →
(∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (j k : Fin 2),
|(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * epsilon β I.Λ (m - 1) ^ (2 * delta β)) →
(∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (p : List (Fin 2)),
1 ≤ p.length →
∀ (j k : Fin 2),
|iterateSpatialWord p
(fun (y : Homogenization.Vec 2) =>
(I.flowGrad hΦ m l t y - 1) j k)
x| ≤ Cflow * ↑p.length.factorial * (Rflow / epsilon β I.Λ (m - 1)) ^ p.length) →
iterateCoordinateEnergyProfile θprev
(I.kappaAt κ (m - 1) (M - (m - 1))) N
(C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0 →
(∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (θprev s)) ≤ N) →
∀ (s : ℝ),
0 ≤ s →
s ≤ 1 →
√(l2NormSq (T (Nstar β) s)) + √(I.kappaAt κ (m - 1) (M - (m - 1))) * √(spaceTimeGradNormSq fun (t : ℝ) =>
spaceGrad (T (Nstar β) t)) ≤ 2 * N * (1 + C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * ↑(Nstar β) * ↑(2 * Nstar β).factorial)
theorem
AVenhance.Infra.Section4.iterate_T_upgrade_of_theta_scalar_zero
(β Ccut : ℝ)
:
∃ (c : ℝ) (Ck : ℝ),
0 < c ∧ c < Ck ∧ ∀ (I : Ingredients β),
I.Czeta ≤ Ccut →
I.Cxi ≤ Ccut →
I.Chat ≤ Ccut →
∀ {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) {m : ℕ}
{θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ},
I.IsTIterates hΦ m (I.kappaAt κ m (M - m)) (I.kappaAt κ (m - 1) (M - (m - 1))) θ₀ θprev T →
IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaAt κ (m - 1) (M - (m - 1)))
(fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev →
2 ≤ m →
m ≤ M →
κ ∈ permittedInterval β I.Λ M →
∀ (Cθ Rθ C₀ N : ℝ),
0 < N →
0 < Rθ →
iterateReducedSourceConstant β Ccut c Ck 40 (2 ^ 10) Cθ ≤ C₀ →
epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ →
epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹ →
iterateCoordinateEnergyProfile θprev (I.kappaAt κ (m - 1) (M - (m - 1))) N
(C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0 →
(∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (θprev s)) ≤ N) →
∀ (s : ℝ),
0 ≤ s →
s ≤ 1 →
√(l2NormSq (T (Nstar β) s)) + √(I.kappaAt κ (m - 1) (M - (m - 1))) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T (Nstar β) t)) ≤ 2 * N * (1 + C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * ↑(Nstar β) * ↑(2 * Nstar β).factorial)