Frozen-field weak solutions and convolution derivatives #
The linear weak equation, frozen-flow existence, and differentiation of the convolution field support the weak-to-Lagrangian argument without its transported-test machinery.
Linear (external-field) weak Vlasov solutions #
The self-consistent weak predicate IsVlasovSolutionOn drives the convolution field by the
solution's own spatial marginal. For the superposition argument we need the linear
version, where the field is driven by an external (frozen) measure curve ρ — both the given
weak solution f (with ρ := spatialMarginal ∘ f) and the pushforward g along the
frozen-field flow solve the same IsLinearVlasovSolutionOn gradW ρ · T, and uniqueness for it
(the crux, C3) forces f = g.
Linear weak Vlasov evolution on Ioo 0 T for a test function φ, with the convolution field
driven by an external measure curve ρ (frozen), not the solution's own spatial marginal.
The self-consistent WeakEvolutionEqOn gradW μ φ … (fun _ => 0) T is the special case
ρ = spatialMarginal ∘ μ (modulo the + 0 remainder term).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A measure curve μ solves the linear Vlasov equation on [0,T] driven by the external
field ρ: the distributional identity LinearWeakEvolutionEqOn holds for every C_c^∞ test
function. Mirror of IsVlasovSolutionOn with the field externalized.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A self-consistent weak solution is a linear solution driven by its own spatial marginal.
The two differ only by WeakEvolutionEqOn's + (fun _ => 0) t = + 0 remainder.
C1 #1 — pushforward solves the frozen linear weak equation.
For a characteristic flow (charX, charV) solving the ODE with an external field ρ on
Ioo 0 T, the pushforward g := (charX t, charV t)_# f₀ solves the linear Vlasov equation
driven by that same ρ. Proof: the generic SC.1–SC.3 machinery (change of variables +
chain rule + differentiation-under-the-integral, all parametric in ρ) recomposed at this ρ,
with SC.4's push-back inlined as integral_map (SC.4's packaged form hard-codes the
self-consistent marginal). This is vlasovSolutionViaPushforward_isVlasovSolutionOn with ρ
left free — the _hself self-consistency hypothesis is unused.
C1 #2 — characteristic flow for a frozen field from window data (L11 clamp).
Build the characteristic flow for the given external curve ρ on Ioo 0 T (with boundary
regularity), from probability/moment/integrability/continuity data on the window [0,T] only.
exists_vlasov_characteristicFlow_global_smallT demands universal-in-t instances; we clamp
t ↦ ρ (max 0 (min t T)) into the window (L11), apply the universal producer to the clamped
curve, and transfer on [0,T] where the clamp is the identity.
Final-step layer (crux-independent): constancy + measure extensionality #
C2 #7 — constancy from a vanishing derivative.
If a real function is continuous on [0,T] and has zero derivative throughout the open
interval, its endpoint values agree. This is the dual argument's payoff step: s ↦ ∫ ψ_s dμ_s
is constant, so its value at T (= ∫ φ dμ_T) equals its value at 0 (= ∫ ψ_0 dμ_0). Mean
value theorem (exists_hasDerivAt_eq_slope).
C2 #9 — C_c^∞ test functions determine a finite measure.
If ∫ φ dμ = ∫ φ dν for every smooth compactly-supported φ, then μ = ν (finite measures on
phase space). The dual argument yields equality of integrals against the IsVlasovSolution test
class C_c^∞; this closes the bridge's final step f T = g T. Route: extend C_c^∞ →
bounded-continuous (smooth approximation), then the in-house bounded-continuous extensionality
ext_of_forall_integral_eq_of_IsFiniteMeasure (cf. Wasserstein.lean).
Convenience extractor: under [AssW2 W], a gradient field gradW= ∇W is C¹.
AssW2.gradContDiff gives ContDiff ℝ 1 (fun x => fderiv ℝ W x); composing with the (smooth,
linear) Riesz isometry gradient W x = (toDual ℝ _).symm (fderiv ℝ W x) and rewriting by hgradW
yields ContDiff ℝ 1 gradW.
Crux layer (C3): the variational equation and the dual-transport assembly #
The two interfaces below were the load-bearing pieces of the bridge — both now proven and
axiom-clean. #3 was the genuine research gap (C¹ dependence of an ODE flow on its initial point
— absent from Mathlib), closed via route (b) (difference-quotient + Gronwall); #8 is the
bridge-specific dual-transported-test-function assembly that consumes it. #10 (the public
theorem) composes the reuse layer (exists_frozenField_charFlow_On, #2) with #8.
The dual-argument internals #4/#5/#6 (test-class enlargement C_c^∞ → C¹_c, the
transported test function ψ_s = φ ∘ Φ_{s→t} and its transport identity, and the zero-derivative
of s ↦ ∫ ψ_s dμ_s) are realized against the two-time-flow representation Φ_{s→t} = Φ_t ∘ Φ_s⁻¹
and proven below (weakEvolution_test_C1c_On, transportedTest_transport_identity,
transportedIntegral_hasDerivAt_zero).
C3 F1 — the convolution force field is C¹ in space (Fréchet derivative under the
integral). For gradW ∈ C¹ (and L-Lipschitz, a probability measure ρ with the kernel
integrable), x ↦ ∫ y, gradW (x − y) ∂ρ is Fréchet-differentiable with derivative
∫ y, fderiv ℝ gradW (x₀ − y) ∂ρ. This is the field-regularity foundation of the variational
equation (#3): it makes D_z (vlasovVectorField …) exist and continuous, so the variational ODE
M' = (D_z b)·M has continuous coefficients.
Differentiation under the integral sign (hasFDerivAt_integral_of_dominated_loc_of_lip): the
per-fibre map x ↦ gradW (x − y) is L-Lipschitz (a uniform, integrable bound against a
probability measure) and differentiable, so the parametric integral differentiates with derivative
the integral of the fibrewise derivatives.
C3 F2 — the Vlasov field is C¹ in the phase-space variable, with the block Jacobian.
At fixed time t, vlasovVectorField gradW ρ t = fun (x,v) ↦ (v, −conv(x)) is
Fréchet-differentiable in z = (x,v) with derivative the block continuous-linear map
δ ↦ (δ.2, −(D_x conv)(δ.1)), where D_x conv = ∫ y, fderiv ℝ gradW (z.1 − y) ∂(ρ t) (F1).
This is the coefficient A(t) := D_z b(t, Φ_t z) of the variational ODE M' = A(t)·M.
C3 F1c — the convolution derivative is continuous in space. x ↦ ∫ y, fderiv ℝ gradW (x − y) ∂ρ (the Fréchet derivative of the convolution field, F1) is continuous, by dominated
convergence: the integrand is continuous in x and bounded by ‖fderiv gradW‖ ≤ L (a constant,
integrable against the probability measure ρ). Continuity of the variational coefficient
A(t) in its spatial argument — half of the t-continuity of A (the other half is the
measure-curve regularity t ↦ ρ t, supplied at the V1c ODE-existence step).
C3 A-cont — the variational coefficient is continuous in time.
Compose the convolution-derivative continuity with the flow, then express the block map as a
sum of continuous compositions. This supplies the coefficient regularity for
exists_fundamentalMatrix.