OAI/MathematicalPhysics/Boltzmann/Approximation/CapDilationCompactness.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Actual cap shots on horizons tending to zero

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.shrinkingHorizon line 25
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.shrinkingHorizon_pos line 27
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.shrinkingHorizon_le line 30
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.shrinkingHorizon_tendsto_zero line 34
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_diagonal_cap_indices line 40
  6. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.ShrinkingCapFamily line 58
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_shrinking_cap_family line 69
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.cap_time line 103
  9. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hotSize line 159
  10. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence line 165
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_attained_cap_sequence line 172
  12. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.radius line 187
  13. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldFraction line 190
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.radius_pos line 193
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.radius_tendsto_zero line 196
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.coldFraction_mem line 202
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalized_time line 206
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.fraction_subsequence line 210
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.horizon_limit_ge_one line 215
  20. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHorizon line 241
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.lower_horizon_tendsto line 244
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.joint_subsequence line 255
  23. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot line 298
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_properties line 303
  25. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_regular line 353
  26. def OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hotNetSource line 418
  27. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_net_source_bound line 424
  28. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_net_source_cap line 480
  29. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_scaled_slab line 533
  30. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_scaled_time line 551
  31. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledHot line 579
  32. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledHot_measurable line 583
  33. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledHot_nonneg line 593
  34. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.rescaledHot_bound_at line 601
  35. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_rescaledHot_bound line 620
  36. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotTimeDomain line 654
  37. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotTimeDomain_measurable line 657
  38. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.extendedHot line 661
  39. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.extendedHot_measurable line 664
  40. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.extendedHot_nonneg line 671
  41. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.extendedHot_bound_at line 677
  42. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.extendedHot_uniform_bound_at line 689
  43. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_extendedHot_eq line 698
  44. abbrev OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotKineticPhase line 726
  45. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotDensity line 730
  46. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotWindowVolume line 733
  47. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotDensity_measurable line 737
  48. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotDensity_nonneg line 744
  49. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotDensity_bound line 750
  50. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hot_majorant_integrable line 768
  51. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotDensity_uniformIntegrable line 776
  52. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotDensity_unifTight line 787
  53. abbrev OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotPairPhase line 817
  54. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotBaseWindowVolume line 819
  55. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotPairWindowVolume line 823
  56. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotPair_bounds line 828
  57. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.hotWeightedPair_bounds line 877
  58. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.hot_spacetime_cap line 923