OAI/MathematicalPhysics/Boltzmann/Compactness/StrongMassClip.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Strong L¹ convergence implies the bounded-test weak convergence used here

  1. theorem OAI.BoltzmannNonuniqueness.Published.weakL1_of_integral_norm_sub line 25
  2. theorem OAI.BoltzmannNonuniqueness.Published.WeakL1Converges.add line 56
  3. theorem OAI.BoltzmannNonuniqueness.Published.weakL1_of_strong line 86
  4. theorem OAI.BoltzmannNonuniqueness.Compactness.integral_abs_tendsto_zero_of_sq line 112
  5. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_L1_of_weak_and_squares line 138
  6. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_of_small_complements line 199
  7. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_of_exhaustion line 219
  8. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_of_pairwise_subsequences line 253
  9. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_on_union line 313
  10. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_of_countable_cover line 325
  11. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_of_nonzero_patches line 347
  12. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_average_of_weak_pairs line 392
  13. def OAI.BoltzmannNonuniqueness.Compactness.massClip line 447
  14. theorem OAI.BoltzmannNonuniqueness.Compactness.massClip_measurable line 449
  15. theorem OAI.BoltzmannNonuniqueness.Compactness.massClip_bounds line 453
  16. theorem OAI.BoltzmannNonuniqueness.Compactness.massClip_lipschitz line 457
  17. theorem OAI.BoltzmannNonuniqueness.Compactness.strong_massClip line 462
  18. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_comp_fst line 473