Scalar zeroth-order T estimate, independent of actual-flow discharge.
theorem
AVenhance.Infra.Section4.iterate_T_abstract_upgrade_of_diffusivity_and_flow_scalar_zero
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hm : 2 ≤ m)
(hκm : 0 < κm)
(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)
(hCk : 0 ≤ Ck)
(hK : 0 ≤ K)
(hCf : 0 ≤ Cflow)
(hCm : 0 ≤ Cmean)
(hRf : 256 ≤ Rflow)
(hRθ : 0 < Rθ)
(hlower : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κprev)
(hupper : κprev ≤ Ck * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)))
(hC₀ : iterateSourceConstant (iterateBudgetUniversalConstant K Ck c (2 ^ (-25)) Cflow Cmean) Rflow Cθ ≤ C₀)
(hsmall :
C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * max 1 (epsilon β I.Λ (m - 1) ^ (2 + gamma β) * Rθ ^ (-2)) ≤ 1 / 4)
(hKm : ∀ (t : ℝ) (j k : Fin 2), |I.Kmat κm m t j k| ≤ K * κprev)
(hmean :
∀ (j k : Fin 2), |(timeAvgMat (I.Kmat κm m) - κprev • 1) j k| ≤ κprev * 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)
(hκscale : |κm| ≤ κprev)
(hbase :
iterateCoordinateEnergyProfile θprev κprev N (max (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) (C₀ / Rθ)) 0)
(hscalar : ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (θprev s)) ≤ N)
(s : ℝ)
:
theorem
AVenhance.Infra.Section4.iterate_T_source_upgrade_of_diffusivity_and_flow_scalar_zero
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hm : 2 ≤ m)
(hκm : 0 < κm)
(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)
(hCk : 0 ≤ Ck)
(hK : 0 ≤ K)
(hCf : 0 ≤ Cflow)
(hCm : 0 ≤ Cmean)
(hRf : 256 ≤ Rflow)
(hRθ : 0 < Rθ)
(hlower : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κprev)
(hupper : κprev ≤ Ck * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)))
(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 κm m t j k| ≤ K * κprev)
(hmean :
∀ (j k : Fin 2), |(timeAvgMat (I.Kmat κm m) - κprev • 1) j k| ≤ κprev * 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)
(hκscale : |κm| ≤ κprev)
(hbase : iterateCoordinateEnergyProfile θprev κprev N (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0)
(hscalar : ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (θprev s)) ≤ N)
(s : ℝ)
: