RelativeError: pairing a classical solution with a transported test

The scalar test is supplied with smoothness, periodicity, and its transport equation. This file proves the parabolic/transport pairing identity; the flow construction of the specific Piola test remains a separate bridge.

structure AVenhance.Infra.Section5.RelativeError.IsClassicalTransportTest (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (h : ℝ → Homogenization.Vec 2 → ℝ) : Prop

Smooth periodic solutions of the homogeneous scalar transport equation.

• smooth : ContDiff ℝ 2 (Function.uncurry h)
• periodic (t : ℝ) : 0 ≤ t → IsZ2Periodic (h t)
• equation (t : ℝ) : 0 < t → ∀ (x : Homogenization.Vec 2), Classical.classicalTimePartial h (t, x) + Homogenization.vecDot (b t x) (spaceGrad (h t) x) = 0

theorem AVenhance.Infra.Section5.RelativeError.TransportPairing.classicalTimePartial_continuousOn_of_smooth {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) Classical.classicalPositiveTimeDomain) : ContinuousOn (Classical.classicalTimePartial u) Classical.classicalPositiveTimeDomain

theorem AVenhance.Infra.Section5.RelativeError.TransportPairing.classicalTimePartial_continuousOn_of_C2 {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ 2 (Function.uncurry u) Classical.classicalPositiveTimeDomain) : ContinuousOn (Classical.classicalTimePartial u) Classical.classicalPositiveTimeDomain

theorem AVenhance.Infra.Section5.RelativeError.classicalTimeSection_hasDerivAt_of_C2 {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ 2 (Function.uncurry u) Classical.classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : HasDerivAt (fun (s : ℝ) => u s x) (Classical.classicalTimePartial u (t, x)) t

theorem AVenhance.Infra.Section5.RelativeError.TransportPairing.classical_solution_time_partial_eq_pde {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : Classical.classicalTimePartial u (t, x) = κ * spaceLap (u t) x - Homogenization.vecDot (b t x) (spaceGrad (u t) x)

theorem AVenhance.Infra.Section5.RelativeError.TransportPairing.integral_unitCell_transport_linear_zero {b : Homogenization.Vec 2 → Homogenization.Vec 2} {f : Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ 1 b) (hbp : ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => b x i) (hdiv : ∀ (x : Homogenization.Vec 2), vecDiv b x = 0) (hf : ContDiff ℝ 1 f) (hfp : IsZ2Periodic f) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (b x) (spaceGrad f x) = 0

Divergence-free transport has zero mean on every smooth periodic scalar.

theorem AVenhance.Infra.Section5.RelativeError.TransportPairing.integral_unitCell_lap_mul_C2 {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 2 g) (hpf : IsZ2Periodic f) (hpg : IsZ2Periodic g) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x * spaceLap g x = -∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad f x) (spaceGrad g x)

theorem AVenhance.Infra.Section5.RelativeError.classical_solution_transportPairing_derivative {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {u h : ℝ → Homogenization.Vec 2 → ℝ} (hb : Flow.SmoothPeriodicField b) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u) (htest : IsClassicalTransportTest b h) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u s x * h s x) (-κ * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad (u t) x) (spaceGrad (h t) x)) t

A classical parabolic solution paired with any smooth inverse-transport test has derivative equal to minus the diffusivity times the gradient pairing.