Exact first stream multiplicity and analytic radius gain at every terminal time.
theorem
AVenhance.Infra.Section4.iterate_truncated_first_stream_time_pairing_bound
{φ u : ℝ → Homogenization.Vec 2 → ℝ}
{H M : ℝ}
(hH : 0 < H)
(hφ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => φ z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
{s : ℝ}
(hs0 : 0 ≤ s)
(hs1 : s ≤ 1)
(hφp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (φ t))
(hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t))
(i j : Fin 2)
(w q : List (Fin 2))
(hq : q.length = w.length)
(hjet :
∀ (t : ℝ) (x : Homogenization.Vec 2) (k : Fin 2),
|spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (φ t) y j) x k| ≤ H)
(hM :
∀ (r : List (Fin 2)),
r.length = w.length → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord r (u t))) ≤ M)
:
|∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord (i :: w) (u z.1)) z.2)
((spaceGrad (φ z.1) z.2 j • sigmaMat).mulVec (spaceGrad (iterateSpatialWord q (u z.1)) z.2))| ≤ 2 * H * M
One actual first stream-jet pairing uses only preceding derivative-order gradient energies. Joint smoothness discharges all time integrability.
theorem
AVenhance.Infra.Section4.iterate_truncated_first_stream_time_sum_bound
{φ u : ℝ → Homogenization.Vec 2 → ℝ}
{H M : ℝ}
(hH : 0 < H)
(hφ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => φ z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
{s : ℝ}
(hs0 : 0 ≤ s)
(hs1 : s ≤ 1)
(hφp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (φ t))
(hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t))
(i : Fin 2)
(w : List (Fin 2))
(hjet :
∀ (t : ℝ) (x : Homogenization.Vec 2) (j k : Fin 2),
|spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (φ t) y j) x k| ≤ H)
(hM :
∀ (q : List (Fin 2)),
q.length = w.length → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord q (u t))) ≤ M)
:
|(List.map
(fun (p : List (Fin 2) × List (Fin 2)) =>
∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord (i :: w) (u z.1)) z.2)
((iterateSpatialWord p.1 (φ z.1) z.2 • sigmaMat).mulVec (spaceGrad (iterateSpatialWord p.2 (u z.1)) z.2)))
(List.filter (fun (p : List (Fin 2) × List (Fin 2)) => p.1.length == 1) (iterateSpatialSplits (i :: w)))).sum| ≤ 2 * H * ↑(w.length + 1) * M
Every first coefficient derivative uses the same preceding derivative energy. Exact ordered multiplicity supplies n, including repeated letters.
theorem
AVenhance.Infra.Section4.iterate_truncated_first_stream_time_analytic_bound
{φ u : ℝ → Homogenization.Vec 2 → ℝ}
{H B L d : ℝ}
(hH : 0 < H)
(hL : 0 < L)
(hφ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => φ z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
{s : ℝ}
(hs0 : 0 ≤ s)
(hs1 : s ≤ 1)
(hφp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (φ t))
(hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t))
(j : Fin 2)
(w : List (Fin 2))
(i : ℕ)
(hjet :
∀ (t : ℝ) (x : Homogenization.Vec 2) (j k : Fin 2),
|spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (φ t) y j) x k| ≤ H)
(hM :
∀ (q : List (Fin 2)),
q.length = w.length →
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord q (u t))) ≤ B ^ 2 * (↑(w.length + 2 * i).factorial * L ^ w.length) ^ 2 * d ^ 2)
:
|(List.map
(fun (p : List (Fin 2) × List (Fin 2)) =>
∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord (j :: w) (u z.1)) z.2)
((iterateSpatialWord p.1 (φ z.1) z.2 • sigmaMat).mulVec (spaceGrad (iterateSpatialWord p.2 (u z.1)) z.2)))
(List.filter (fun (p : List (Fin 2) × List (Fin 2)) => p.1.length == 1) (iterateSpatialSplits (j :: w)))).sum| ≤ 2 * H * B ^ 2 / L ^ 2 * (↑(w.length + 1 + 2 * i).factorial * L ^ (w.length + 1)) ^ 2 * d ^ 2
The full first stream-jet contribution has precisely the n-1 norm squared and one squared radius gain; multiplicity causes no order loss.