The time negative norm of tiny in terms of the last increment #
timeHMinusOneNorm tiny ≤ 2 b_d + √(c ∑_w ‖∇ ∂^w V‖²_{L²((0,1)×𝕋²)}) where V = T_{N*} - T_{N*-1}
is the last increment, b_d bounds the L²_{t,x} norm of d_m, and c collects the coefficient
jets of B = K_m - κ_{m-1} + s_{m-1} and the corrector size. Here only the structure of tiny
(hMinusOneNorm_tiny_le_of_components) and the slice regularity are used; no scale arithmetic.
theorem
AVenhance.Infra.Section5.Contracts.sc_slice_continuous
{F : ℝ → Homogenization.Vec 2 → ℝ}
(hF : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) tcU)
{t : ℝ}
(ht : 0 < t)
:
Continuous (F t)
Slices of a field continuous on the open half space are continuous.
theorem
AVenhance.Infra.Section5.Contracts.sc_slice_continuous_vec
{F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hF : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2 i) tcU)
{t : ℝ}
(ht : 0 < t)
:
Continuous (F t)
theorem
AVenhance.Infra.Section5.Contracts.sc_tiny_slice_le
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κm κprev : ℝ}
(hκm : 0 < κm)
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
{t : ℝ}
(ht : 0 < t)
(hmean :
Homogenization.MeanZeroOn unitCube
(tiny I hΦ m κm (sourceErrorD I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) t))
:
hMinusOneNorm (tiny I hΦ m κm (sourceErrorD I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) t) ≤ ENNReal.ofReal
√(gradNormSq fun (x : Homogenization.Vec 2) =>
sourceErrorD I hΦ m κm (T (Nstar β)) t x + iterateError I hΦ m κm κprev T t x) + ENNReal.ofReal ((2 * Real.pi)⁻¹ * √(l2NormSq (tinyNondivergencePart I hΦ m κm (iterateError I hΦ m κm κprev T) t)))
The slice bound ‖tiny(t)‖_{HDot⁻¹} ≤ ‖d+e‖_{L²} + (2π)⁻¹ ‖nd‖_{L²}.
theorem
AVenhance.Infra.Section5.Contracts.sc_scCoeff_contDiff
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κm κprev : ℝ}
(t : ℝ)
:
theorem
AVenhance.Infra.Section5.Contracts.sc_increment_contDiffOn
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
:
ContDiffOn ℝ (↑⊤) (fun (z : Section4.AmnrSpace) => Section4.iterateIncrement T (Nstar β) z.1 z.2)
(Set.Ici 0 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section5.Contracts.sc_tiny_time_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κm κprev : ℝ}
(hκm : 0 < κm)
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hmean : Integration.TinyMeanZeroContract I hΦ m κm κprev T)
{bd : ℝ}
(hbd : 0 ≤ bd)
(hd :
(∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(gradNormSq (sourceErrorD I hΦ m κm (T (Nstar β)) t)) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal bd)
{b cχ D r : ℝ}
(hb : ∀ t ∈ Set.Ioo 0 1, ∀ (x : Homogenization.Vec 2) (j k : Fin 2), |scCoeff I hΦ m κm κprev t x j k| ≤ b)
(hχ : ∀ t ∈ Set.Ioo 0 1, ∀ (k : ℤ) (x : Homogenization.Vec 2) (j : Fin 2), |I.chiTilde hΦ m κm k t x j| ≤ cχ)
(hD : 0 ≤ D)
(hr : 1 ≤ r)
(hAj :
∀ t ∈ Set.Ioo 0 1,
∀ (x : Homogenization.Vec 2) (p : List (Fin 2)),
p.length ≤ 2 →
∀ (j k : Fin 2),
|Section4.iterateMatrixWord (scCoeff I hΦ m κm κprev t) p x j k| ≤ D * ↑p.length.factorial * r ^ p.length)
:
(timeHMinusOneNorm fun (t : ℝ) =>
tiny I hΦ m κm (sourceErrorD I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) t) ≤ ENNReal.ofReal
(2 * bd + √((16 * b ^ 2 + 2 * (2 * Real.pi)⁻¹ ^ 2 * (5184 * cχ ^ 2 * (14336 * D ^ 2 * r ^ 4))) * ∑ w ∈ scWords2, spaceTimeGradNormSq (scWordGrad (Section4.iterateIncrement T (Nstar β)) w)))
The time negative norm of tiny in terms of the last increment.