All-order terminal energy with the actual explicit flux pairings.
theorem
AVenhance.Infra.Section4.iterate_classical_word_flux_time_energy_identity
{φ : ℝ → Homogenization.Vec 2 → ℝ}
(hφ : IsAdmissibleStream φ)
{κ : ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
{u₀ : Homogenization.Vec 2 → ℝ}
{A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
{v : ℝ → Homogenization.Vec 2 → ℝ}
(hsol :
IsClassicalSol (streamVel φ) κ
(fun (t : ℝ) => vecDiv fun (x : Homogenization.Vec 2) => (A t x).mulVec (spaceGrad (v t) x)) u₀ u)
(hA : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (A t))
(hAp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (A t))
(hv : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (v t))
(hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t))
(w : List (Fin 2))
{s : ℝ}
(hs : 0 ≤ s)
:
(l2NormSq (iterateSpatialWord w (u s)) - l2NormSq (iterateSpatialWord w u₀)) / 2 + κ * ∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (u t)) x) = ∫ (t : ℝ) in 0..s, (-∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u t)) x) (iterateWordFlux (A t) (v t) w x)) - ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u t)) x)
(iterateWordFlux (fun (y : Homogenization.Vec 2) => φ t y • sigmaMat) (u t) w x)
The differentiated time energy has the literal preceding flux and the current stream error on its right-hand side. The equality is at every terminal time; no supremum and full-dissipation interchange is used.
theorem
AVenhance.Infra.Section4.iterates_smooth_up_to_initial
{β : ℝ}
(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)
(hθ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => θprev z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
{i : ℕ}
(hi : i ≤ Nstar β)
:
Every actual iterate in the range has the initial-boundary smooth carrier.
theorem
AVenhance.Infra.Section4.iterateIncrement_smooth_up_to_initial
{β : ℝ}
(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)
(hθ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => θprev z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
{i : ℕ}
(hi : i ≤ Nstar β)
:
ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => iterateIncrement T i z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)
The preceding increment's smoothness is derived from the actual carriers.
theorem
AVenhance.Infra.Section4.iterateIncrement_periodic
{β : ℝ}
(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)
(hθ : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (θprev t))
{i : ℕ}
(hi : i ≤ Nstar β)
{t : ℝ}
(ht : 0 ≤ t)
:
IsZ2Periodic (iterateIncrement T i t)
Actual increments inherit periodicity throughout the iteration range.
theorem
AVenhance.Infra.Section4.iterate_sMat_periodic_of_flow
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm t : ℝ)
(hp : ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t))
:
IsZ2Periodic (I.sMat hΦ m κm t)
The actual sMat is periodic when the pulled flow Jacobians are periodic.
theorem
AVenhance.Infra.Section4.iterate_increment_word_flux_time_energy_identity
{β : ℝ}
(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)
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hflow : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), ContDiff ℝ (↑⊤) (I.flowGrad hΦ m l t))
(hflowp : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t))
(hm : 1 ≤ m)
(i : ℕ)
(hi : i + 1 ≤ Nstar β)
(w : List (Fin 2))
{s : ℝ}
(hs : 0 ≤ s)
:
l2NormSq (iterateSpatialWord w (iterateIncrement T (i + 1) s)) / 2 + κprev * ∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (iterateIncrement T (i + 1) t)) x) = ∫ (t : ℝ) in 0..s, (-∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (iterateIncrement T (i + 1) t)) x)
(iterateWordFlux (fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y)
(iterateIncrement T i t) w x)) - ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (iterateIncrement T (i + 1) t)) x)
(iterateWordFlux (fun (y : Homogenization.Vec 2) => Φ (m - 1) t y • sigmaMat) (iterateIncrement T (i + 1) t) w
x)
Literal all-order increment energy with both forcing fluxes explicit. Coefficient regularity and periodicity are discharged from the conditional actual flow carriers. No forcing formula, energy bound or recurrence is assumed.