MoserTransport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact change of variables from uniform slab density to the actual manufactured density. The identity is for arbitrary scalar integrands, including the Coulomb kernel used by the nuclear cubature.

theorem OAI.ContinuumCoulomb.moser_flowJacobian_pos line 14

theorem OAI.ContinuumCoulomb.moser_density_integral line 32

Source documentation

The actual Moser map pushes uniform density to the synthesized nonnegative nuclear density, with the entire slab preserved.

theorem moser_density_integral (hpublished : PublishedC4FlowInput)
    {rho H S : ℝ} (hrho : 0 < rho) (V : Position → ℝ) (hV : ContDiff ℝ 6 V)
    (hbound : ∀ x, |manufacturedCharge V x| ≤ rho/2)
    (hsupport : tsupport V ⊆ slabDomain H S)
    (G : Position → ℝ → Position) (hG : IsUnitTimeFlow (moserVelocity rho V) G)
    (hbij : Function.Bijective (fun x => G x 1))
    (hfix : ∀ x, x ∉ tsupport V → G x 1 = x) (f : Position → ℝ) :
    (∫ y in slabDomain H S, synthesizedDensity rho H S V y * f y) =
      rho * ∫ x in slabDomain H S, f (G x 1) := by
…

Mentions: OAI.ContinuumCoulomb.PublishedC4FlowInput, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.manufacturedCharge, OAI.ContinuumCoulomb.slabDomain, OAI.ContinuumCoulomb.IsUnitTimeFlow, OAI.ContinuumCoulomb.moserVelocity, OAI.ContinuumCoulomb.synthesizedDensity