The third term of e.ergodic.break.up: integration by parts in time #
Source: enhance.tex 8640–8830 (e.ergodic.break.up.last). The zero-mean periodic matrix
J - ⟨⟨J⟩⟩ is the time derivative of a bounded primitive Q with Q(0) = Q(1) = 0; integrating
by parts in time against A_ij(t) = ∫_{𝕋²} ∂_iT ∂_jT and using ∂_t A_ij = ∫ (D_t∂_iT ∂_jT + ∂_iT D_t∂_jT) (since ∇·b = 0) gives the stated bound.
The three ingredients live in the TimeIBP/ modules: Abstract (the abstract time integration by
parts), Derivative (hasDerivAt_integral_gradProduct), EntryBound (the Cauchy–Schwarz bound
on ∫ |A_ij'|).
theorem
AVenhance.Infra.Section5.LeftToShow.abs_integral_mul_gradProd_le
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hb : Flow.SmoothPeriodicField b)
(hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), Flow.spatialDivergence b t x = 0)
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(hTper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (T t))
{G : ℝ → ℝ}
{P B : ℝ}
{N : ℕ}
(hP : 0 < P)
(hNP : ↑N * P = 1)
(hG : Continuous G)
(hGper : Function.Periodic G P)
(hGmean : ∫ (t : ℝ) in 0..1, G t = 0)
(hB : ∀ (t : ℝ), |G t| ≤ B)
(i j : Fin 2)
:
Entrywise integration by parts in time.
theorem
AVenhance.Infra.Section5.LeftToShow.third_term_ibp
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : Flow.SmoothPeriodicField b)
(hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), Flow.spatialDivergence b t x = 0)
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(hTper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (T t))
(J : ℝ → Matrix (Fin 2) (Fin 2) ℝ)
(hJ : ∀ (i j : Fin 2), Continuous fun (t : ℝ) => J t i j)
{P B : ℝ}
{N : ℕ}
(hP : 0 < P)
(hNP : ↑N * P = 1)
(hJper : ∀ (i j : Fin 2), Function.Periodic (fun (t : ℝ) => J t i j) P)
(hB : ∀ (t : ℝ) (i j : Fin 2), |(J t - timeAvgMat J) i j| ≤ B)
:
e.ergodic.break.up.last, generic matrix field form: for J with continuous P-periodic
entries, N P = 1, and |J - ⟨⟨J⟩⟩| ≤ B entrywise.