EuclideanKineticMap.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Euclidean coordinates for the physical characteristic equation

def OAI.BoltzmannNonuniqueness.EuclideanFlight.flight line 21
Source documentation
Euclidean free transport, with the same velocity convention as GLPS.
```
def flight (t : ℝ) (p : Velocity × Velocity) : Velocity × Velocity :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
def OAI.BoltzmannNonuniqueness.EuclideanFlight.spaceEquiv line 24
def OAI.BoltzmannNonuniqueness.EuclideanFlight.phaseEquiv line 27
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.spaceEquiv_apply line 30
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.phaseEquiv_apply line 35
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.phaseEquiv_measurePreserving line 40
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.phaseEquiv_flight line 46
def OAI.BoltzmannNonuniqueness.EuclideanFlight.density line 53
Source documentation
The physical density lifted to the Euclidean kinetic domain of GLPS.
```
def density (q : ℝ) (F : ℝ × JetPrototype.Phase → ℝ)
    (z : Published.KineticPhase) : ℝ :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.Published.KineticPhase
def OAI.BoltzmannNonuniqueness.EuclideanFlight.source line 57
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.density_measurable line 61
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.source_eq_collision line 68
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.flight_measurePreserving line 89
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.characteristic_back line 99
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.characteristic_endpoint line 109
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.phaseEquiv_snd line 131
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.density_along line 133
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.source_along line 140
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.localized line 147

theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.smooth_localized line 172

Source documentation

A smooth kinetic cutoff, with its derivative actually computed along the transport field, gives the local source required by velocity averaging.

theorem smooth_localized (hcarleman : Published.GPV2009CarlemanInput)
    {q b L T U R : ℝ} {f₀ : JetPrototype.Phase → ℝ}
    (F : WeightedLocalControl.PeriodicMildState q b L U R f₀)
    (hq₁ : 1 < q) (hq₂ : q < 2) (hb : 0 ≤ b) (hR : 0 ≤ R) (hT : 0 ≤ T) (hTU : T ≤ U)
    (hloss : R*CutoffLipschitz.frequencyConstant q b ≤ L) (hf₀ : Measurable f₀)
    {χ : Published.KineticPhase → ℝ} (hχ : ContDiff ℝ (⊤ : ℕ∞) χ)
    (hzero : ∀ p : Velocity × Velocity, χ (TransportCutoff.characteristic p 0) = 0) :
    ∀ᵐ p ∂(volume : Measure (Velocity × Velocity)),
      χ (TransportCutoff.characteristic p T)*density q F.value (TransportCutoff.characteristic p T) =
        ∫ t in 0..T, Real.exp (-(T-t)) *
          (χ (TransportCutoff.characteristic p t)*source b q F.value (TransportCutoff.characteristic p t) +
            (TransportCutoff.transportDerivative χ (TransportCutoff.characteristic p t)+
…

theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.characteristic line 214
def OAI.BoltzmannNonuniqueness.EuclideanFlight.kineticMap line 246
theorem OAI.BoltzmannNonuniqueness.EuclideanFlight.kineticMap_measurePreserving line 249