Full analytic theta estimate under the conditional stream-regularity and diffusivity-recursion conclusion data.
theorem
AVenhance.Infra.Section4.ThetaAnalyticBound.theta_gradient_only_order_zero_bound
{κ N : ℝ}
{φ : ℝ → Homogenization.Vec 2 → ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(hφ : IsAdmissibleStream φ)
(hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ)
(hκ : 0 < κ)
(hN : N = √(l2NormSq θ₀))
:
theorem
AVenhance.Infra.Section4.theta_analytic_energy_bound_of_A3_A5
{β : ℝ}
{M m : ℕ}
(I : Ingredients β)
(Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ)
(hΦ : IsStreamSeq I Φ)
(hm : 2 ≤ m)
(hmM : m ≤ M)
{κ : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θ : ℝ → Homogenization.Vec 2 → ℝ}
{c C R : ℝ}
(hR : 0 < R)
(hθ₀ : IsThetaAnalytic R θ₀)
(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)))
(hA5 :
0 < c ∧ c < C ∧ ∀ (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) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)))
(hsol :
IsClassicalSol (streamVel fun (t : ℝ) => Φ (m - 1) t) (I.kappaSeq κ M (m - 1))
(fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ)
(n : ℕ)
:
The §4 analytic estimate for every ordered derivative energy level. The zero-order induction datum is only the dissipative gradient term; the full zero-order estimate is supplied separately by the energy identity.