OAI/MathematicalPhysics/Boltzmann/Jets/JetContinuation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Total norm control for a reconstructed geometric decomposition

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_total_norm_le line 29
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_cell_moment line 85
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_cold_sum_ae line 162
  4. def OAI.BoltzmannNonuniqueness.JetCopyDatum.escapedFrequencyConstant line 229
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.escapedFrequencyConstant_nonneg line 233
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.frequency_at_main_cap line 239
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.capped_total_bound line 292
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.total_norm_le line 332
  9. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermal_error_integrable line 383
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.survival_of_capped_family line 429
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_survival line 515
  12. def OAI.BoltzmannNonuniqueness.JetCopyDatum.freeColor line 577
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.measurable_freeColor line 581
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.freeColor_along line 586
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.physical_freeColor line 591
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_le_free_add_barrier line 604
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.eulerian_survival line 632
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_zero_hot_bound line 662
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt_local_free_error line 766
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_uniform_rebuilt_zero_control line 846
  21. def OAI.BoltzmannNonuniqueness.JetCopyDatum.continuationAmplitude line 906
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_uniform_zero_solution line 909
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_uniform_zero_solution_large line 998