Exact current diffusion transfer at every actual terminal time.
theorem
AVenhance.Infra.Section4.iterate_truncated_laplacian_pairing_transfer
{s : ℝ}
(hs1 : s ≤ 1)
{a b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ}
(ha : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (a t))
(hb : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (b t))
(hap : ∀ (t : ℝ), 0 < t → IsZ2Periodic (a t))
(hbp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (b t))
(hL :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecDot (fun (i : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => a p.1 y i) p.2)
((Q p.1).mulVec (b p.1 p.2)))
timeCube MeasureTheory.volume)
(hR :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecDot (a p.1 p.2)
((Q p.1).mulVec fun (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => b p.1 y j) p.2))
timeCube MeasureTheory.volume)
:
∫ (p : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (fun (i : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => a p.1 y i) p.2)
((Q p.1).mulVec (b p.1 p.2)) = ∫ (p : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (a p.1 p.2)
((Q p.1).mulVec fun (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => b p.1 y j) p.2)
Fubini lifts the periodic Laplacian transfer to the time cell.
theorem
AVenhance.Infra.Section4.iterate_truncated_current_diffusion_pairing_bound
{s : ℝ}
(hs1 : s ≤ 1)
{a b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ}
{κ D E : ℝ}
(hκ : 0 < κ)
(hQ : ∀ (t : ℝ) (i j : Fin 2), |Q t i j| ≤ D)
(ha : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (a t))
(hb : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (b t))
(hap : ∀ (t : ℝ), 0 < t → IsZ2Periodic (a t))
(hbp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (b t))
(hL :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecDot (fun (i : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => a p.1 y i) p.2)
((Q p.1).mulVec (b p.1 p.2)))
timeCube MeasureTheory.volume)
(hR :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecDot (a p.1 p.2)
((Q p.1).mulVec fun (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => b p.1 y j) p.2))
timeCube MeasureTheory.volume)
(haI :
MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (a p.1 p.2)) timeCube
MeasureTheory.volume)
(hbI :
MeasureTheory.IntegrableOn
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecNormSq fun (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => b p.1 y j) p.2)
timeCube MeasureTheory.volume)
(hprevious :
(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) =>
spaceLap (fun (y : Homogenization.Vec 2) => b t y j) x) ≤ E)
:
Transfer the current diffusion derivatives before applying Young. Only the preceding field's Laplacian energy occurs in the remainder.