MoserJacobian.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The continuity equation yields the density-Jacobian identity along the flow. The proof uses finite-dimensional ODE regularity.

theorem OAI.ContinuumCoulomb.linear_apply_coordinates line 14
theorem OAI.ContinuumCoulomb.divergence_scalar_mul line 23
theorem OAI.ContinuumCoulomb.moser_continuity_expanded line 41
theorem OAI.ContinuumCoulomb.flowJacobian_zero line 63
theorem OAI.ContinuumCoulomb.moser_density_jacobian line 70
Source documentation
Density times the determinant of the actual flow derivative is exactly constant, including the endpoint used by cubature.
```
theorem moser_density_jacobian (hpublished : PublishedC4FlowInput)
    {rho : ℝ} (hrho : 0 < rho) (V : Position → ℝ) (hV : ContDiff ℝ 6 V)
    (hbound : ∀ x, |manufacturedCharge V x| ≤ rho/2)
    (G : Position → ℝ → Position) (hG : IsUnitTimeFlow (moserVelocity rho V) G)
    (x : Position) {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    homotopyDensity rho V t (G x t) * flowJacobian G t x = rho := by
…
```
Mentions: OAI.ContinuumCoulomb.PublishedC4FlowInput, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.manufacturedCharge, OAI.ContinuumCoulomb.IsUnitTimeFlow, OAI.ContinuumCoulomb.moserVelocity, OAI.ContinuumCoulomb.homotopyDensity, OAI.ContinuumCoulomb.flowJacobian