PhysicalCharacteristic.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Physical collision source in the localized characteristic equation

def OAI.BoltzmannNonuniqueness.PhysicalLocalization.density line 19
def OAI.BoltzmannNonuniqueness.PhysicalLocalization.source line 22
theorem OAI.BoltzmannNonuniqueness.PhysicalLocalization.source_eq line 26

theorem OAI.BoltzmannNonuniqueness.PhysicalLocalization.localized line 35

Source documentation

The constructed positive periodic solutions satisfy the physical localized Duhamel formula; the artificial iteration damping has disappeared.

theorem 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₀)
    (χ χ' : JetPrototype.Phase → ℝ → ℝ)
    (hχ : ∀ p, ContinuousOn (χ p) (Icc 0 T))
    (hχ' : ∀ p, ContinuousOn (χ' p) (Icc 0 T))
    (hdχ : ∀ p t, t ∈ Icc 0 T → HasDerivAt (χ p) (χ' p t) t) :
    ∀ᵐ p ∂FlightMeasure.phaseVolume,
      χ p T*density q F.value (T,JetBarrier.flight T p) =
        Real.exp (-T)*χ p 0*(H q p.2*f₀ p) +
…

Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState, OAI.BoltzmannNonuniqueness.CutoffLipschitz.frequencyConstant, OAI.BoltzmannNonuniqueness.FlightMeasure.phaseVolume, OAI.BoltzmannNonuniqueness.PhysicalLocalization.density, OAI.BoltzmannNonuniqueness.JetBarrier.flight

theorem OAI.BoltzmannNonuniqueness.PhysicalLocalization.characteristic line 105