Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.RelativeError.TransportFlowCellIntegral

RelativeError: inverse-flow change of variables on the periodic cell #

source
noncomputable def AVenhance.Infra.Section5.RelativeError.flowPeriodicVolumePreservingDiffeomorphism {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) (t : ℝ) :
Ergodic.PeriodicVolumePreservingDiffeomorphism 2

The fixed-time flow and its inverse form a smooth periodic measure-preserving diffeomorphism of the torus.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AVenhance.Infra.Section5.RelativeError.integral_unitCell_comp_inverseFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) {f : Homogenization.Vec 2 → ℝ} (hf : IsZ2Periodic f) (t : ℝ) :
    ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f (X 0 x t) = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x

    Inverse transport preserves integrals over one periodic cell. The proof uses the induced measure-preserving torus diffeomorphism, represented by its Euclidean lift.