Iterates Actual Seven Flux Energy #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_increment_terminal_seven_flux_energy_inequality
{β : ℝ}
(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 : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2)
(hflowp : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t))
(hm : 1 ≤ m)
(hκm : 0 < κm)
(i : ℕ)
(hi : i + 1 ≤ Nstar β)
(w : List (Fin 2))
{s : ℝ}
(hs : 0 ≤ s)
(hs1 : s ≤ 1)
:
have u := fun (t : ℝ) => iterateSpatialWord w (iterateIncrement T (i + 1) t);
have v := fun (t : ℝ) => iterateSpatialWord w (iterateIncrement T i t);
have b := streamVel (Φ (m - 1));
have Q := iterateKmatPrimitive I κm m;
l2NormSq (u s) / 2 + κprev * ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecNormSq (spaceGrad (u z.1) z.2) ≤ |∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (u s) x) ((Q s).mulVec (spaceGrad (v s) x))| + |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (u z.1) z.2)
((Q z.1).mulVec (spaceGrad (amnrMaterial b v z.1) z.2))| + |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (amnrMaterial b u z.1) z.2) ((Q z.1).mulVec (spaceGrad (v z.1) z.2))| + |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (u z.1) z.2)
((Q z.1).mulVec ((gradMatrix (b z.1) z.2).mulVec (spaceGrad (v z.1) z.2)))| + |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot ((gradMatrix (b z.1) z.2).mulVec (spaceGrad (u z.1) z.2))
((Q z.1).mulVec (spaceGrad (v z.1) z.2))| + |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (u z.1) z.2)
(iterateWordFlux
(fun (y : Homogenization.Vec 2) => timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm z.1 y)
(iterateIncrement T i z.1) w z.2)| + |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (u z.1) z.2)
(iterateWordFlux (fun (y : Homogenization.Vec 2) => Φ (m - 1) z.1 y • sigmaMat)
(iterateIncrement T (i + 1) z.1) w z.2)|
Complete differentiated energy inequality for the actual increment. Every flux is exposed in the form used by its independently proved bound.