OAI/MathematicalPhysics/Boltzmann/Jets/JetFamilyBounds.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Uniform hot-source control from the periodic cold decomposition

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.scale_antitone line 34
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.select_remainder line 45
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.uniform_hot_source line 70
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.hot_source_bound line 124
  5. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermal_integral_one line 204
  6. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.masked_thermal_bound line 210
  7. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.free_average_bound line 224
  8. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.dilated_free_average_bound line 251
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.family_hot_source_bound line 280
  10. theorem OAI.BoltzmannNonuniqueness.JetPeriodicDatum.measurable_pullback line 367
  11. def OAI.BoltzmannNonuniqueness.JetPeriodicDatum.truncated line 371
  12. theorem OAI.BoltzmannNonuniqueness.JetPeriodicDatum.truncated_integrable line 374
  13. theorem OAI.BoltzmannNonuniqueness.JetPeriodicDatum.truncated_L1_tendsto line 391
  14. theorem OAI.BoltzmannNonuniqueness.JetConvergence.add_L1_tendsto line 406
  15. def OAI.BoltzmannNonuniqueness.JetCopyDatum.periodicInitial line 427
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.periodicInitial_eq line 431
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.periodicInitial_L1_tendsto line 447
  18. theorem OAI.BoltzmannNonuniqueness.JetGeometry.enlargement_dilated_shell line 486
  19. theorem OAI.BoltzmannNonuniqueness.JetGeometry.enlargement_mesh_window line 502
  20. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.window_eventually_below_top line 515
  21. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.masked_thermal_integrable line 537
  22. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.dilatedMask_eq line 552
  23. theorem OAI.BoltzmannNonuniqueness.JetGeometry.maskError_average_eq line 565
  24. def OAI.BoltzmannNonuniqueness.JetCopyDatum.scalarMajorant line 605
  25. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.hot_source_norm_bound line 611
  26. def OAI.BoltzmannNonuniqueness.JetCoreDensity.limitingCoefficient line 709
  27. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.limitingCoefficient_measurable line 714
  28. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.limitingCoefficient_bound line 729
  29. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.free_average_measurable line 738
  30. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.mask_average_measurable line 751
  31. theorem OAI.BoltzmannNonuniqueness.JetLocalFreeError.integral_error_le line 784
  32. def OAI.BoltzmannNonuniqueness.JetCopyDatum.colorAmplitude line 839
  33. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.colorAmplitude_nonneg line 842
  34. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.color_le_amplitude line 848
  35. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cold_sum_le_of_core_bound line 857
  36. def OAI.BoltzmannNonuniqueness.JetCopyDatum.finiteAmplitude line 890
  37. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.finiteAmplitude_nonneg line 894
  38. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.amplitude_le_finite line 901
  39. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cell_cold_sum_bound line 914
  40. def OAI.BoltzmannNonuniqueness.JetCopyDatum.coldNormBound line 966
  41. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.coldNormBound_nonneg line 970
  42. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cold_sum_bound line 975
  43. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.cell_outer_bound line 1040
  44. def OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt line 1106
  45. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_envelope line 1110
  46. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_zero line 1139
  47. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_shift line 1150
  48. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_cell_outer_bound line 1182
  49. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.scalarMajorant_eq_source line 1253
  50. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.tail_small line 1267