OAI/MathematicalPhysics/Boltzmann/Approximation/CapMildLimit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the actual right-hand sides of the cap equations

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_cutoff_equation_limit_with_pair line 22
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_cutoff_equation_limit line 64
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.periodicInitial_measurable line 98
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.spacetime_mild line 110
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.characteristic_slice line 144
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.periodicInitial_integrable line 181
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CompactCapFamily.initial_weak_limit line 199
  8. structure OAI.BoltzmannNonuniqueness.MildCollisionSolution line 232

    Source documentation

    The characteristic identity uses the full physical collision terms and the prescribed initial density. The spacetime identity determines a continuous-time representative through the Bochner integral of the collision source.

    structure MildCollisionSolution (T : ℝ) (f₀ : Density)
    (g : (ℝ × Position) × Velocity → ℝ) : Prop where
…

    Mentions: OAI.BoltzmannNonuniqueness.Density, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity

  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_mild_limit_with_convergence line 247
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_mild_limit line 307