OAI/MathematicalPhysics/Boltzmann/Collision/SheetKernelLimits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Kernel limits for the manuscript's probability mixtures of sheets

  1. theorem OAI.BoltzmannNonuniqueness.SheetKernelLimits.mixture_region_bound line 20
  2. theorem OAI.BoltzmannNonuniqueness.SheetKernelLimits.dominated_region_bound line 28
  3. theorem OAI.BoltzmannNonuniqueness.SheetKernelLimits.mixture_large_output line 38
  4. theorem OAI.BoltzmannNonuniqueness.SheetKernelLimits.mixture_axis_input line 52
  5. theorem OAI.BoltzmannNonuniqueness.SheetKernelLimits.mixture_axis_mismatch line 67
  6. def OAI.BoltzmannNonuniqueness.SheetKernelLimits.IsThinElementary line 84

    Source documentation

    The actual elementary subclass with a prescribed upper transverse width.

    def IsThinElementary (L η : ℝ) (c : Measure Velocity) : Prop :=
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity

  7. theorem OAI.BoltzmannNonuniqueness.SheetKernelLimits.measurableSet_smallRegion line 88
  8. theorem OAI.BoltzmannNonuniqueness.SheetKernelLimits.mixture_small_input line 92