OAI/MathematicalPhysics/Boltzmann/Compactness/FiniteRatesWindowUI.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Regularized entropy inequality for the actual periodic finite approximations

  1. def OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.torusEvolution line 25
  2. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.regularized_entropy_inequality line 29
  3. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.entropy_nonincrease line 77

    Source documentation

    Every finite periodic mild approximation has nonincreasing relative entropy.

    theorem entropy_nonincrease (hcarleman : Published.GPV2009CarlemanInput)
    {q b L T U R : ℝ} {f₀ : JetPrototype.Phase → ℝ}
    (F : 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₀) (hf₀b : ∀ z, 0 ≤ f₀ z ∧ f₀ z ≤ R) :
    relativeEntropy (F.torusEvolution T) ≤ relativeEntropy (TorusFlight.initialDensity q f₀) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState, OAI.BoltzmannNonuniqueness.CutoffLipschitz.frequencyConstant, OAI.BoltzmannNonuniqueness.relativeEntropy, OAI.BoltzmannNonuniqueness.TorusFlight.initialDensity

  4. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.entropy_dissipation_inequality line 143
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scatterTriple_window_measurePreserving line 199
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPreRate_window_uniformIntegrable line 212
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.massRegularizedPostRate_window_uniformIntegrable line 234