OAI/MathematicalPhysics/Boltzmann/Branching/ReferenceGrowthBlocks.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Uniform transverse-velocity entry for the actual Poisson flight

  1. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poissonKernel_term_le line 18
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.state_two_transverse_entry line 32
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.poisson_transverse_entry line 51
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightKernel_displacement line 62
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flight_transverse_entry line 68
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.blockTarget line 97
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.blockTarget_measurable line 100
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flight_block_geometry line 104
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.growth_damping_cancel line 144
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.growth_damping_split line 151
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.growth_damping_clock line 160
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.time_cut_scale line 167
  13. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.terminalBlock line 195
  14. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.driftBlock line 198
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.terminalBlock_apply line 201
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.driftBlock_lower line 206
  17. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight_changed_damping line 259
  18. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingAt line 350
  19. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingAt_sFinite line 353
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingAt_apply line 360
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingAt_physical line 365
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingAt_lower line 377
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branchingAt_mass_bound line 392
  24. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight_damped_subsolution line 424
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight_le_damped_series line 459
  26. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.blockFirstTime line 498
  27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.large_driftBlock_lower line 500
  28. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weighted_driftBlock_growth line 553
  29. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flightKernel_free_lower line 599
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.driftBlock_le_flight line 612
  31. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.blockFirstTime_sum line 622
  32. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.full_flight_block_growth line 627
  33. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight_indicator line 679
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.weightedFlight_window_bound line 687
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branching_remainder_uniform line 698
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finite_branching_block_growth line 721
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_branching_remainder line 781
  38. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_branching_remainder_on_window line 806
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_damped_finite_block_growth line 820
  40. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.branching_remainder_on_window line 883
  41. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_finite_branching_block_growth line 893
  42. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBlockTarget line 950
  43. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.block_target_perturb line 953
  44. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finite_position_error_of_total line 966