OAI/MathematicalPhysics/Boltzmann/Branching/StripeCells.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exact period and mean of the cold stripes

  1. def OAI.BoltzmannNonuniqueness.JetGeometry.stripeLine line 14
  2. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripeAtPeriod_mem_iff line 18
  3. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripeLine_measurable line 21
  4. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripeLine_add_period line 26
  5. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripeLine_indicator_periodic line 34
  6. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripeLine_on_cell line 42
  7. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripeLine_integral_period line 65