SourceErrorDContract: the θ profile in the big-bound premise block #
Contracts/ThetaProfile.lean produces ThetaProfileContract at N = 2‖θ₀‖ in the step-down
premise block
(OnA8Instances, which carries an unused classical θ_m); its core lemma is private. The
big-bound estimate
block has no θ_m, so the core lemma is reproduced here and produces the profile in the
OnA7Instances block with a free
profile constant Cs ≥ 8 max(r(c), 2).
theorem
AVenhance.Infra.Section5.Contracts.SourceErrorDTheta.sed_theta_profile_of_explicit_A3_A5
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m M : ℕ}
(hm : 2 ≤ m)
(hmM : m ≤ M)
{κ R : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
(hR : 0 < R)
(hscale : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R)
(hθ₀ : IsThetaAnalytic R θ₀)
(hθprev :
IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀
θprev)
{c C Cs : ℝ}
(hc : 0 < c)
(hcC : c < C)
(hRadius : 8 * max (Section4.thetaAnalyticRadiusBase c) 2 ≤ Cs)
(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 :
∀ (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 β)))
:
theorem
AVenhance.Infra.Section5.Contracts.sed_thetaProfile_A7
(β C₀ : ℝ)
:
∃ (Cθ : ℝ),
∀ (Cs : ℝ),
Cθ ≤ Cs →
Integration.OnA7Instances β C₀ 0
fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ)
(_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θprev : ℝ → Homogenization.Vec 2 → ℝ)
(_T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) =>
Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs (2 * √(l2NormSq θ₀))
The θ profile at amplitude 2‖θ₀‖ in the big-bound premise block, for every profile constant
Cs ≥ Cθ (Cθ depends only on β, C₀).