Iterates Terminal Signed Pairing

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_signed_pairing_identity {f g : AmnrSpace → ℝ} (hf : ContinuousOn f (Set.Ici 0 ×ˢ Set.univ)) (hg : ContinuousOn g (Set.Ici 0 ×ˢ Set.univ)) {s : ℝ} (hs : 0 ≤ s) : ∫ (t : ℝ) in 0..s, (-∫ (x : Homogenization.Vec 2) in unitCube, f (t, x)) - ∫ (x : Homogenization.Vec 2) in unitCube, g (t, x) = (-∫ (z : AmnrSpace) in iterateTruncatedCell s, f z) - ∫ (z : AmnrSpace) in iterateTruncatedCell s, g z

Fubini preserves the two signed terms of the actual energy identity.