OAI/MathematicalPhysics/Boltzmann/Jets/ColdMildRepresentative.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

The polynomial optical depth used in the cold-core survival estimate

  1. def OAI.BoltzmannNonuniqueness.coldOpticalDepth line 24
  2. theorem OAI.BoltzmannNonuniqueness.coldOpticalDepth_zero line 27
  3. theorem OAI.BoltzmannNonuniqueness.coldOpticalDepth_derivative line 31
  4. theorem OAI.BoltzmannNonuniqueness.coldOpticalDepth_nonneg line 50
  5. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.cold_survival_polynomial line 58
  6. def OAI.BoltzmannNonuniqueness.WeightedLocal.normalizedFamily line 97
  7. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.measurable_normalizedFamily line 102
  8. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.normalizedFamily_bounds line 115
  9. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.normalizedFamily_sum_le line 125
  10. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.normalizedFamily_ae_at_time line 133
  11. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.normalizedFamily_summable line 145
  12. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.family_sum_pull line 171
  13. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.familyReplacement_pull line 180
  14. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.remainderForcing_pull line 189
  15. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.cold_family_difference_ae line 221
  16. theorem OAI.BoltzmannNonuniqueness.abs_sub_le_of_survival line 343
  17. theorem OAI.BoltzmannNonuniqueness.integral_abs_sub_le_of_survival line 351
  18. theorem OAI.BoltzmannNonuniqueness.scaled_survival_error_tendsto_zero line 370
  19. def OAI.BoltzmannNonuniqueness.coldDilationError line 412

    Source documentation

    S bounds the rescaled jet size, and U bounds rescaled time.

    def coldDilationError (C A D S U : ℝ) (m : ℕ) (r : ℝ) : ℝ :=
…
  20. theorem OAI.BoltzmannNonuniqueness.coldOpticalDepth_le_dilationError line 415
  21. theorem OAI.BoltzmannNonuniqueness.coldDilationError_nonneg line 428
  22. theorem OAI.BoltzmannNonuniqueness.coldDilationError_tendsto_zero line 434
  23. theorem OAI.BoltzmannNonuniqueness.coldOpticalDepth_tendsto_zero line 441
  24. theorem OAI.BoltzmannNonuniqueness.scaled_local_error_le line 472
  25. theorem OAI.BoltzmannNonuniqueness.scaled_local_error_tendsto_zero line 485
  26. theorem OAI.BoltzmannNonuniqueness.jet_epsilon_tendsto_zero line 497
  27. theorem OAI.BoltzmannNonuniqueness.ColdDilationMeasure.space_finrank line 525
  28. theorem OAI.BoltzmannNonuniqueness.ColdDilationMeasure.setIntegral_space_smul line 528
  29. theorem OAI.BoltzmannNonuniqueness.ColdDilationMeasure.dilated_error_integral line 535
  30. theorem OAI.BoltzmannNonuniqueness.ColdDilationMeasure.spaceVolume_real_smul line 543
  31. theorem OAI.BoltzmannNonuniqueness.eventually_cold_survival_geometry line 568
  32. def OAI.BoltzmannNonuniqueness.ColdDilationMeasure.spaceEquiv line 604
  33. def OAI.BoltzmannNonuniqueness.ColdDilationMeasure.phaseEquiv line 607
  34. theorem OAI.BoltzmannNonuniqueness.ColdDilationMeasure.map_space_restrict line 610
  35. theorem OAI.BoltzmannNonuniqueness.ColdDilationMeasure.map_phase_restrict line 625
  36. theorem OAI.BoltzmannNonuniqueness.ColdDilationMeasure.integrable_dilate line 634
  37. theorem OAI.BoltzmannNonuniqueness.ColdDilationMeasure.integrable_dilated_error line 648
  38. theorem OAI.BoltzmannNonuniqueness.ColdDilationMeasure.product_dilated_error_integral line 655
  39. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.ColdMildAE.representative line 681