RelativeError: integrate the parabolic/transport pairing identity from time zero

def AVenhance.Infra.Section5.RelativeError.TransportPairingIntegral.transportClosedCube : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section5.RelativeError.TransportPairingIntegral.transportClosedCube = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section5.RelativeError.TransportPairingIntegral.transportClosedCube_compact : IsCompact transportClosedCube

theorem AVenhance.Infra.Section5.RelativeError.TransportPairingIntegral.transportUnitCube_ae_closedCube : unitCube =ᵐ[MeasureTheory.volume] transportClosedCube

theorem AVenhance.Infra.Section5.RelativeError.continuousOn_unitCubeIntegral_Icc {T : ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContinuousOn (Function.uncurry F) (Set.Icc 0 T ×ˢ Set.univ)) : ContinuousOn (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, F s x) (Set.Icc 0 T)

theorem AVenhance.Infra.Section5.RelativeError.classical_solution_transportPairing_integral_identity {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) (hhSmooth : ContDiff ℝ (↑⊤) (Function.uncurry h)) {t : ℝ} (ht : 0 < t) : (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u t x * h t x) + κ * ∫ (s : ℝ) in 0..t, ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad (u s) x) (spaceGrad (h s) x) = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u 0 x * h 0 x

The integrated pairing identity for a smooth classical solution and a smooth transported test. It includes the initial trace at t = 0.