OAI/MathematicalPhysics/Boltzmann/Compactness/WeakTimeLocalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A locally integrable weakly time-constant function is constant on an interval

  1. theorem OAI.BoltzmannNonuniqueness.WeakTime.exists_normalized_test line 19
  2. theorem OAI.BoltzmannNonuniqueness.WeakTime.weakly_constant_test_integral line 31
  3. theorem OAI.BoltzmannNonuniqueness.WeakTime.ae_eq_const_of_weak_deriv_zero line 66
  4. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.timePrimitive_slice line 110
  5. theorem OAI.BoltzmannNonuniqueness.Published.timePrimitive_slice_integrable line 130
  6. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.mild_slice line 138
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.weak_localize_time line 163