OAI/MathematicalPhysics/Boltzmann/Branching/PerturbedFiniteBlock.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Positive marked histories in a measurable two-beam medium

  1. structure OAI.BoltzmannNonuniqueness.ReferenceGeometry.BeamCoefficients line 17
  2. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.PhysicalFlightState line 27
  3. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.embedFlightState line 29
  4. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumPoint line 31
  5. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumParameterState line 34
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumParameterDensity line 39
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumPoint_measurable line 46
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumParameterState_measurable line 51
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumParameterDensity_measurable line 86
  10. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumWordState line 152
  11. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumWordDensity line 157
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumWordState_measurable line 163
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumWordDensity_measurable line 175
  14. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.GoodReferenceWord line 187
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.goodReferenceWord_of_density_ne_zero line 193
  16. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.WordNearby line 206
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedParameterState_velocity line 233
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_parameter_velocity_error line 239
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_parameter_position_error line 249
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterWordState_time line 260
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_word_geometry line 269
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.nearby_marked_rate_bounds line 317
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.nearby_parameter_density_bounds line 357
  24. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.wordWeightError line 418
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.wordWeightError_ne_top line 422
  26. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.WordCoefficientClose line 429
  27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.word_weight_comparison line 438
  28. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.word_coefficients_close line 475
  29. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.BeamNear line 514
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.wordNearby_of_excursion line 518
  31. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.wordNearby_from_start line 559
  32. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.finishMediumFlight line 589
  33. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finishMediumFlight_error line 592
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_word_endpoint_error line 603
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_word_target line 624
  36. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumBlockIntegrand line 652
  37. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyPerturbationError line 659
  38. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_word_integrand_bound line 663
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.medium_word_integral_lower line 698
  40. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.historyPerturbationError_continuous line 733
  41. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteHistoryError line 737
  42. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteHistoryError_continuous line 740
  43. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteHistoryError_zero line 747
  44. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteHistoryError_small line 750
  45. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.mediumBlockMass line 777
  46. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finite_history_block_transfer line 781
  47. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_perturbed_block_growth line 837