The determinant evolution of the two-dimensional variational flow.

def AVenhance.Infra.Flow.Liouville.flowBasis0 : Homogenization.Vec 2

First coordinate basis vector used in the two-dimensional Liouville calculation.

Equations

• AVenhance.Infra.Flow.Liouville.flowBasis0 = Pi.single 0 1

def AVenhance.Infra.Flow.Liouville.flowBasis1 : Homogenization.Vec 2

Second coordinate basis vector used in the two-dimensional Liouville calculation.

Equations

• AVenhance.Infra.Flow.Liouville.flowBasis1 = Pi.single 1 1

theorem AVenhance.Infra.Flow.Liouville.linearMap_apply_two (A : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (v : Homogenization.Vec 2) (i : Fin 2) : A v i = A flowBasis0 i * v 0 + A flowBasis1 i * v 1

noncomputable def AVenhance.Infra.Flow.spatialDivergence (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The divergence of a spatial vector field is the trace of its spatial Fréchet derivative.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Flow.flowSpatialJacobianDet (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) : ℝ

The determinant of the spatial Fréchet derivative of a two-dimensional flow map, written in the canonical coordinate basis.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Flow.Liouville.continuousLinearMap_det_two (J : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) : J.det = J flowBasis0 0 * J flowBasis1 1 - J flowBasis1 0 * J flowBasis0 1

theorem AVenhance.Infra.Flow.flowSpatialJacobianDet_eq_fderiv_det (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) : flowSpatialJacobianDet X t x s = (fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x).det

The explicit coordinate expression above is Mathlib's determinant on the Fréchet derivative.

theorem AVenhance.Infra.Flow.exists_flow_liouville_determinant {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s : ℝ) (hdiv : ∀ (r : ℝ), spatialDivergence b r (X r x s) = 0) : ∃ (V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2), IsFlow (linearizedFieldAlongFlow b X x s) V ∧ ∀ (t : ℝ), V t Liouville.flowBasis0 s 0 * V t Liouville.flowBasis1 s 1 - V t Liouville.flowBasis1 s 0 * V t Liouville.flowBasis0 s 1 = 1

Under the divergence-free condition, the determinant of the variational flow stays equal to one. The variational solution is the same unique system already characterized as the spatial derivative of the flow.

theorem AVenhance.Infra.Flow.flow_spatial_jacobian_det_eq_one_of_divergence_free {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), spatialDivergence b t x = 0) (x : Homogenization.Vec 2) (s t : ℝ) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x).det = 1

A divergence-free smooth field has unit spatial Jacobian determinant at every point and every pair of times.