OAI/MathematicalPhysics/Boltzmann/Compactness/LocalAdmissibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual cold datum has a nonnegative strong local mild solution

  1. structure OAI.BoltzmannNonuniqueness.LocalMildSolution line 20

    Source documentation

    The local solution properties established before the entropy and continuation steps.

    structure LocalMildSolution (T : ℝ) (f₀ : Density) (F : Evolution) : Prop where
…

    Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Evolution

  2. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.localMildSolution line 34
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_local_mild_solution line 49
  4. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_moment line 101
  5. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.positiveEvolution_outer_bound line 114
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_bounded_local_mild_solution line 129
  7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.kineticFrequency_integrable_local line 180
  8. structure OAI.BoltzmannNonuniqueness.AdmissibleLocal line 232

    Source documentation

    Local admissibility retains endpoint terms for arbitrary tests. This permits pasting at T without assuming that a test vanishes at the joining time.

    structure AdmissibleLocal (T : ℝ) (f₀ : Density) (F : Evolution) : Prop
    extends LocalMildSolution T f₀ F where
…

    Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Evolution, OAI.BoltzmannNonuniqueness.LocalMildSolution

  9. theorem OAI.BoltzmannNonuniqueness.LocalMildSolution.weak_continuity line 276