Iterates Retained Current Forcing #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_terminal_current_word_pairing_retained_forcing
{s : ℝ}
(hs1 : s ≤ 1)
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ D : ℝ}
{F u v : ℝ → Homogenization.Vec 2 → ℝ}
{u₀ : Homogenization.Vec 2 → ℝ}
{Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ}
(hsol : IsClassicalSol b κ F u₀ u)
(w : List (Fin 2))
(hκ : 0 < κ)
(hQ : ∀ (t : ℝ) (i j : Fin 2), |Q t i j| ≤ D)
(hv : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (v t))
(hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t))
(hF : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (F t))
(huI :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (u p.1)) p.2))
timeCube MeasureTheory.volume)
(hvLap :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecNormSq fun (j : Fin 2) =>
spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (v p.1) y j) p.2)
timeCube MeasureTheory.volume)
(hL :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecDot
(fun (i : Fin 2) =>
spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w (u p.1)) y i) p.2)
((Q p.1).mulVec (spaceGrad (v p.1) p.2)))
timeCube MeasureTheory.volume)
(hR :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u p.1)) p.2)
((Q p.1).mulVec fun (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (v p.1) y j) p.2))
timeCube MeasureTheory.volume)
(hFP :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecDot (spaceGrad (iterateSpatialWord w (F p.1)) p.2) ((Q p.1).mulVec (spaceGrad (v p.1) p.2)))
timeCube MeasureTheory.volume)
:
|∫ (p : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (amnrMaterial b u p.1)) p.2)
((Q p.1).mulVec (spaceGrad (v p.1) p.2))| ≤ ((κ / 24 * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w (u t)) x) + 24 * κ * D ^ 2 * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) =>
spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (v t) y j) x) + |∫ (p : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (F p.1)) p.2) ((Q p.1).mulVec (spaceGrad (v p.1) p.2))|