OAI/MathematicalPhysics/Boltzmann/Branching/CentralRetainedLimit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The central cube gives the closest periodic origin in every coordinate

  1. theorem OAI.BoltzmannNonuniqueness.TorusChart.interval_abs_le_shift line 23
  2. theorem OAI.BoltzmannNonuniqueness.TorusChart.scaled_coordinate_nearest line 32
  3. theorem OAI.BoltzmannNonuniqueness.TorusChart.central_coordinate_nearest line 39
  4. theorem OAI.BoltzmannNonuniqueness.TorusChart.central_axial_nearest line 44
  5. theorem OAI.BoltzmannNonuniqueness.TorusChart.central_transverse_nearest line 49
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.central_away_retained_le_originScale line 81
  7. theorem OAI.BoltzmannNonuniqueness.TorusChart.exists_lattice_central line 124
  8. theorem OAI.BoltzmannNonuniqueness.TorusChart.ae_le_of_central line 139
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.central_retained_five_tendsto line 179