RelativeError: the transported scalar test along a smooth flow

The inverse flow transports initial data by characteristics. Joint C³ regularity of the flow supplies the C² regularity needed by the pairing lemma.

def AVenhance.Infra.Section5.RelativeError.inverseFlowTransportTest {h₀ : Homogenization.Vec 2 → ℝ} (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → ℝ

Pull a smooth scalar back along the inverse of the time-zero forward flow.

Equations

• AVenhance.Infra.Section5.RelativeError.inverseFlowTransportTest X t x = h₀ (X 0 x t)

theorem AVenhance.Infra.Section5.RelativeError.inverseFlowTransportTest_isClassicalTransportTest {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {h₀ : Homogenization.Vec 2 → ℝ} (hh₀ : ContDiff ℝ (↑⊤) h₀) (hh₀per : IsZ2Periodic h₀) : IsClassicalTransportTest b (inverseFlowTransportTest X)

The inverse-flow pullback is a smooth periodic solution of the homogeneous transport equation. Only C² regularity is recorded; this is sufficient for the parabolic pairing and the periodic integration by parts used there.