OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveVolterra.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Positive backward gain iteration on free kinetic characteristics

  1. def OAI.BoltzmannNonuniqueness.PositiveIteration.flight line 26
  2. def OAI.BoltzmannNonuniqueness.PositiveIteration.step line 29
  3. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_mono line 33
  4. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_inner_measurable line 38
  5. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_add line 49
  6. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_le_constant line 60
  7. theorem OAI.BoltzmannNonuniqueness.Published.positive_volterra_limit line 96
  8. def OAI.BoltzmannNonuniqueness.PositiveIteration.iterate line 178
  9. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_bound line 183
  10. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_measurable line 231
  11. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_measurable line 255
  12. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_slab_mono line 262
  13. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_slab_mono line 272
  14. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_add line 280
  15. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_step line 289
  16. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.backward_measurePreserving line 314
  17. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_congr_ae_at line 324
  18. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_congr_ae line 336
  19. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_normalized_congr_ae line 349
  20. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.residual_expansion line 382
  21. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.residual_logarithmic_bound line 401
  22. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_const_mul line 441
  23. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_const_mul line 448
  24. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_const_bound line 458
  25. def OAI.BoltzmannNonuniqueness.PositiveIteration.onSlab line 489
  26. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.onSlab_measurable line 492
  27. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.onSlab_eq line 496
  28. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_onSlab line 500
  29. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_onSlab line 509
  30. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.onSlab_positive_inequality line 519
  31. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_uniform_bound line 550
  32. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_uniform_bound line 570
  33. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_factorial_bound line 600
  34. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_count_add line 663
  35. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.iterate_first_two_le line 670
  36. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.step_source_upper line 698