OAI/MathematicalPhysics/Boltzmann/Branching/WeightedJetStability.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Recovering a weighted weak limit from its unweighted density

  1. theorem OAI.BoltzmannNonuniqueness.Published.identify_weighted_weak_limit line 27
  2. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.forcing_window line 66
  3. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.coldForcing_window line 70
  4. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.MildAE.window line 75
  5. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.ColdMildAE.window line 92
  6. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.normalized_difference_ae line 128
  7. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.family_hot_mildAE line 199
  8. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.normalized_unique line 271
  9. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.bounded_interval_stability_uniform line 303
  10. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.exists_mild_limit line 403
  11. def OAI.BoltzmannNonuniqueness.WeightedLocalControl.damping line 481
  12. def OAI.BoltzmannNonuniqueness.WeightedLocalControl.sourceBound line 483
  13. def OAI.BoltzmannNonuniqueness.WeightedLocalControl.lipschitz line 485
  14. def OAI.BoltzmannNonuniqueness.WeightedLocalControl.lifespan line 488
  15. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.bounds line 490
  16. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.lifespan_pos line 497
  17. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.small line 501
  18. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.exists_solution line 510
  19. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.bounded_interval_stability line 543
  20. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.MildAE.restrict_clamp line 641
  21. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.clampTime_idempotent line 652
  22. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.shift_neg_shift line 676
  23. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.shift_shift_neg line 679
  24. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.solution_covariance line 682
  25. theorem OAI.BoltzmannNonuniqueness.WeightedJetComparison.picard_le line 714
  26. theorem OAI.BoltzmannNonuniqueness.WeightedJetComparison.limit_le line 741
  27. theorem OAI.BoltzmannNonuniqueness.WeightedJetComparison.shifted_limit_le line 777