Per-iterate spatial jets of the S-amplitude

The AMNR engine consumes L² bounds on the spatial words of amnrTGradient (T i) p over the time-cell product measure, for every partial iterate T i, i ≤ Nstar β. Upstream supplies the dissipation spaceTimeGradNormSq of the iterate spatial words of θprev (profile) and of the increments V_j = T j - T (j-1) (amplitude theorem). This file proves the adapter:

• a single-function bridge from a spatial dissipation bound to the L² bound of the actual amnrWord of amnrTGradient u p, for any u that is smooth up to the initial time;
• telescoping T i = ∑_{j ≤ i} V_j at the level of eLpNorm;
• the scalar bookkeeping at the scales ε_{m-1} and the final adapter relative_iterate_gradient_jets.

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Section5.RelativeError.unitCellMeasure : MeasureTheory.Measure Section4.AmnrSpace

The time-cell product measure on (0,1] × (0,1)².

Equations

• AVenhance.Infra.Section5.RelativeError.unitCellMeasure = (MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod (MeasureTheory.volume.restrict AVenhance.unitCube)

theorem AVenhance.Infra.Section5.RelativeError.iterateSpatialWord_eq_amnrSpaceWord (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : Section4.iterateSpatialWord w f = Section4.amnrSpaceWord w f

theorem AVenhance.Infra.Section5.RelativeError.spaceTimeGradNormSq_nonneg (Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ spaceTimeGradNormSq Dθ

theorem AVenhance.Infra.Section5.RelativeError.tGradient_contDiffOn {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : Section4.AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (p : Fin 2) : ContDiffOn ℝ (↑⊤) (Section4.amnrTGradient u p) (Set.Ioi 0 ×ˢ Set.univ)

The actual gradient is smooth on the open positive-time domain once the function is smooth up to the initial time.

theorem AVenhance.Infra.Section5.RelativeError.amnrWord_tGradient_ae_eq {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : Section4.AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (b : Section4.AmnrSpace → Homogenization.Vec 2) (p : Fin 2) (α : List (Fin 2)) : Section4.amnrWord b (List.map some α) (Section4.amnrTGradient u p) =ᵐ[unitCellMeasure] fun (z : Section4.AmnrSpace) => spaceGrad (Section4.amnrSpaceWord α (u z.1)) z.2 p

On the product measure, the actual spatial word of the gradient is the coordinate of the gradient of the spatial word of the slices.

theorem AVenhance.Infra.Section5.RelativeError.amnrWord_tGradient_eLpNorm_le {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : Section4.AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (b : Section4.AmnrSpace → Homogenization.Vec 2) (p : Fin 2) (α : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrWord b (List.map some α) (Section4.amnrTGradient u p)) 2 unitCellMeasure ≤ ENNReal.ofReal √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (Section4.iterateSpatialWord α (u t)))

Bridge: the spatial dissipation of u bounds the L² norm of every actual spatial word of its gradient on the unit time-cell product.

theorem AVenhance.Infra.Section5.RelativeError.amnrWord_tGradient_sum_eqOn {V : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {T : ℝ → Homogenization.Vec 2 → ℝ} (s : Finset ℕ) (hV : ∀ j ∈ s, ContDiffOn ℝ (↑⊤) (fun (z : Section4.AmnrSpace) => V j z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hT : ∀ (t : ℝ) (x : Homogenization.Vec 2), T t x = ∑ j ∈ s, V j t x) (b : Section4.AmnrSpace → Homogenization.Vec 2) (p : Fin 2) (α : List (Fin 2)) : Set.EqOn (Section4.amnrWord b (List.map some α) (Section4.amnrTGradient T p)) (∑ j ∈ s, Section4.amnrWord b (List.map some α) (Section4.amnrTGradient (V j) p)) (Set.Ioi 0 ×ˢ Set.univ)

A finite decomposition of a temperature into smooth pieces decomposes every actual spatial word of its gradient on the positive-time domain.

theorem AVenhance.Infra.Section5.RelativeError.amnrWord_tGradient_eLpNorm_sum_le {V : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {T : ℝ → Homogenization.Vec 2 → ℝ} (s : Finset ℕ) (hV : ∀ j ∈ s, ContDiffOn ℝ (↑⊤) (fun (z : Section4.AmnrSpace) => V j z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hT : ∀ (t : ℝ) (x : Homogenization.Vec 2), T t x = ∑ j ∈ s, V j t x) (b : Section4.AmnrSpace → Homogenization.Vec 2) (p : Fin 2) (α : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrWord b (List.map some α) (Section4.amnrTGradient T p)) 2 unitCellMeasure ≤ ∑ j ∈ s, ENNReal.ofReal √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (Section4.iterateSpatialWord α (V j t)))

Telescoped L² bound: the gradient word of T is bounded by the sum of the dissipation bounds of the pieces.

Scalar bookkeeping

theorem AVenhance.Infra.Section5.RelativeError.iterate_jets_scale_simplify {e γ R C : ℝ} (he : 0 < e) (hC : 0 < C) (hscale : e ^ (1 + γ / 2) ≤ R) : max 1 (e ^ (2 + γ) * R ^ (-2)) = 1 ∧ max (C * e ^ (-1 - γ / 2)) (C / R) = C * e ^ (-1 - γ / 2)

At the profile scale E^{1+γ/2} ≤ Rθ the two maxima in the amplitude theorem collapse.

theorem AVenhance.Infra.Section5.RelativeError.iterate_jets_epsilon_rpow_delta_le {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} (hm : 1 ≤ m) {K : ℝ} (hK : 0 < K) (hbig : K ^ (1 / delta β) ≤ ↑Λ) : epsilon β Λ m ^ delta β ≤ K⁻¹

ε^δ ≤ K⁻¹ once Λ ≥ K^{1/δ}.

theorem AVenhance.Infra.Section5.RelativeError.iterateAmplitude_le_one {η : ℝ} (h0 : 0 ≤ η) (h1 : η ≤ 1) (i : ℕ) : Section4.iterateAmplitude η i ≤ 1

The amplitude profile is at most one for a smallness parameter in [0,1].

theorem AVenhance.Infra.Section5.RelativeError.iterateAnalyticWeight_le {n i k : ℕ} {L : ℝ} (hL : 0 ≤ L) (hn : n ≤ k) (hi : i ≤ k) : Section4.iterateAnalyticWeight n i L ≤ ↑(3 * k).factorial * L ^ n

theorem AVenhance.Infra.Section5.RelativeError.iterateAnalyticWeight_nonneg {n i : ℕ} {L : ℝ} (hL : 0 ≤ L) : 0 ≤ Section4.iterateAnalyticWeight n i L

theorem AVenhance.Infra.Section5.RelativeError.sqrt_stg_le_of_profile {G N κ W : ℝ} (hN : 0 ≤ N) (hκ : 0 < κ) (hW : 0 ≤ W) (h : G ≤ (N / √κ) ^ 2 * W ^ 2) : √G ≤ N / √κ * W

Dissipation bound from the profile shape, in square-root form.

theorem AVenhance.Infra.Section5.RelativeError.sqrt_stg_le_of_amplitude {G P N κ A W : ℝ} (hP : 0 ≤ P) (hN : 0 ≤ N) (hκ : 0 < κ) (hW : 0 ≤ W) (hA : A ≤ 1) (h : P + √κ * G ≤ N * A * W) : G ≤ N / √κ * W

Dissipation bound from the amplitude shape.

Regularity of the increments

theorem AVenhance.Infra.Section5.RelativeError.iterateIncrement_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) {j : ℕ} (hj : j ≤ Nstar β) : ContDiffOn ℝ (↑⊤) (fun (z : Section4.AmnrSpace) => Section4.iterateIncrement T j z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)

Every increment V_j = T j - T (j-1) (with V_0 = θprev) is smooth up to the initial time.

The adapter

theorem AVenhance.Infra.Section5.RelativeError.relative_iterate_gradient_jets (β Cs : ℝ) (hCs : 0 < Cs) : ∃ (Cg : ℝ), 0 ≤ Cg ∧ ∃ (Λ₀ : ℝ), ∀ (I : Ingredients β), Λ₀ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M m : ℕ), 2 ≤ m → ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), 0 < I.kappaSeq κ M m → 0 < I.kappaSeq κ M (m - 1) → IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → ∀ (N Rθ : ℝ), 0 ≤ N → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ → Section4.iterateCoordinateEnergyProfile θprev (I.kappaSeq κ M (m - 1)) N (Cs * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0 → (∀ (i : ℕ), 1 ≤ i → i ≤ Nstar β → ∀ (v w : List (Fin 2)), v.length = w.length → ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (Section4.iterateSpatialWord v (Section4.iterateIncrement T i s))) + √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (Section4.iterateSpatialWord w (Section4.iterateIncrement T i t))) ≤ N * Section4.iterateAmplitude (Cs ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * max 1 (epsilon β I.Λ (m - 1) ^ (2 + gamma β) * Rθ ^ (-2))) i * Section4.iterateAnalyticWeight v.length i (max (Cs * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) (Cs / Rθ))) → ∀ i ≤ Nstar β, ∀ (p : Fin 2) (α : List (Fin 2)), α.length ≤ Nstar β → MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (Section4.amnrTGradient (T i) p)) 2 ((MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod (MeasureTheory.volume.restrict unitCube)) ≤ ENNReal.ofReal (Cg * N / √(I.kappaSeq κ M (m - 1)) * (max Cs 1 * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ α.length)

Relative step inputs. The θ profile and the V-increment amplitude conclusion supply the positive spatial jets of the gradient of every partial iterate T i, i ≤ Nstar β, in the form consumed by the AMNR engine.