The zeroth spatial-derivative consequence of l.V.m-1.reg.upgrade:
the actual iterates telescope to T_{m-1} - θ_{m-1}, and their
factorial-weighted amplitudes close to the scale in l.Tm.minus.thetam.
The conditional input below is exactly the n = 0, positive-increment slice
of the upstream l.V estimate, expressed in the torus norms.
theorem
AVenhance.Infra.Section4.TLemmasMinusTheta.classical_spatial_smooth
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F : ℝ → Homogenization.Vec 2 → ℝ}
{u₀ : Homogenization.Vec 2 → ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hu : IsClassicalSol b κ F u₀ u)
{t : ℝ}
(ht : 0 ≤ t)
:
theorem
AVenhance.Infra.Section4.TLemmasMinusTheta.iterateIncrement_value_memL2On
{β : ℝ}
(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)
(hThetaSmooth : ∀ (t : ℝ), 0 ≤ t → ContDiff ℝ (↑⊤) (θprev t))
{i : ℕ}
(hi : 1 ≤ i)
(hiN : i ≤ Nstar β)
{t : ℝ}
(ht : 0 ≤ t)
:
The pointwise value estimate uses only the positive-increment value part
of l.V. Its torus-cell integrability follows from the actual classical
iterates, so no spacetime-gradient integrability premise is needed.
theorem
AVenhance.Infra.Section4.iterate_Tm_minus_theta_value_bound_of_V_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)
(hThetaSmooth : ∀ (t : ℝ), 0 ≤ t → ContDiff ℝ (↑⊤) (θprev t))
{S : ℝ}
(hS : 0 ≤ S)
{η A ρ : ℝ}
(hη : 0 ≤ η)
(hηsmall : η ≤ 1 / 4)
(hscale : η ≤ A * ρ)
(hAρ : 0 ≤ A * ρ)
(hV :
∀ i ∈ Finset.range (Nstar β),
∀ t ∈ Set.Icc 0 1,
√(l2NormSq (iterateIncrement T (i + 1) t)) + √κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) =>
spaceGrad (iterateIncrement T (i + 1) s) x) ≤ ↑(2 * (i + 1)).factorial * iterateAmplitude η (i + 1) * S)
(t : ℝ)
(ht : t ∈ Set.Icc 0 1)
:
Value-only finite telescope from the positive-increment l.V bound.