OAI/MathematicalPhysics/Boltzmann/Jets/PeriodicJetFamilies.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Countably labeled periodic copies of the finite cold datum

  1. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.(instance at line 26) line 26
  2. def OAI.BoltzmannNonuniqueness.JetCopyDatum.displacement line 32
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.color line 35
  4. def OAI.BoltzmannNonuniqueness.JetCopyDatum.seed line 40
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.measurable_color line 43
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.measurable_seed line 51
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.color_nonneg line 54
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.in_enlargement line 62
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.color_disjoint line 85
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.color_summable line 93
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.coefficient_le_amplitude line 115
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.color_bound line 126
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.seed_bounds line 150
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.finite_sum_le_seed line 167
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.physical_color_le line 174
  16. def OAI.BoltzmannNonuniqueness.JetCopyDatum.relabel line 200
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.displacement_add line 206
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.shift_shift line 213
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.color_shift line 220
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.seed_periodic line 232
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.integer_zero_of_close line 257
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.term_shift_lattice_zero line 267
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.color_central line 295
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.seed_on_cube line 307
  25. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.coldLimit_shift line 384
  26. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.coldSum_shift line 394
  27. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.hotRemainder_shift line 407
  28. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.hotForcing_shift line 418
  29. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.familyReplacement_shift line 439
  30. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.remainderForcing_shift line 450
  31. def OAI.BoltzmannNonuniqueness.JetCopyDatum.initial line 489
  32. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.initial_color_bounds line 492
  33. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_periodic_solution line 507
  34. def OAI.BoltzmannNonuniqueness.JetCopyDatum.cold line 560
  35. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cold_envelope line 564
  36. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cold_family_summable line 589
  37. theorem OAI.BoltzmannNonuniqueness.JetHotGain.remainder_bound line 624
  38. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.outside_iff_not_mem line 664
  39. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.main_or_outside line 668
  40. def OAI.BoltzmannNonuniqueness.JetCopyDatum.coordinates line 707
  41. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.tsum_labels line 713
  42. def OAI.BoltzmannNonuniqueness.JetCopyDatum.escaped line 720
  43. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.escaped_bound line 726
  44. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.sum_sub_main line 781
  45. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.sum_all_escaped line 801
  46. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cold_zero line 830
  47. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.normalized_escaped_bound line 839
  48. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.remainder_at_main line 884
  49. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.frequency_at_main line 903
  50. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.color_initial_core line 967
  51. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.shifted_flight_position line 978
  52. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.central_enlargement_coordinates line 990
  53. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.color_flight_geometry line 1014
  54. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.enlargement_central_lattice line 1063
  55. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.enlargement_central_shell line 1090
  56. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.main_coefficient_le line 1102
  57. def OAI.BoltzmannNonuniqueness.JetCopyDatum.escapedConstant line 1137
  58. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cell_moment_bound line 1140
  59. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.spatialMap_surjective line 1232
  60. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_shift_in_cell line 1239