OAI/MathematicalPhysics/Boltzmann/Jets/AnnularEnvelopes.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

The integrable square of the cold annular time envelope

  1. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.time_square_continuous line 22
  2. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.time_square_integral line 30
  3. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.time_square_integral_le line 46
  4. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.annular_square_summable line 51
  5. theorem OAI.BoltzmannNonuniqueness.GrowthContradiction.annular_to_late_growth line 79
  6. def OAI.BoltzmannNonuniqueness.AnnularEnvelope.shell line 148
  7. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.shell_measurable line 151
  8. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.shell_disjoint line 155
  9. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.shell_subset_ball line 165
  10. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.shell_finite line 170
  11. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.shell_area_le line 173
  12. def OAI.BoltzmannNonuniqueness.AnnularEnvelope.term line 185
  13. def OAI.BoltzmannNonuniqueness.AnnularEnvelope.finiteEnvelope line 188
  14. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.term_measurable line 191
  15. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.finiteEnvelope_square line 201
  16. def OAI.BoltzmannNonuniqueness.AnnularEnvelope.timeSpaceVolume line 240
  17. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.inverse_square_integrable line 243
  18. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.inverse_square_integral_le line 252
  19. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.term_square_eq line 268
  20. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.term_square_integrable line 273
  21. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.term_square_integral_le line 281
  22. def OAI.BoltzmannNonuniqueness.AnnularEnvelope.squareEnvelope line 296
  23. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.term_square_summable line 299
  24. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.term_square_integrals_summable line 309
  25. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.squareEnvelope_integrable line 321
  26. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.finiteEnvelope_square_le line 334
  27. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.finiteEnvelope_measurable line 358
  28. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.squareEnvelope_nonneg line 362
  29. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.finite_squares_uniformIntegrable line 365
  30. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.finite_squares_tendsto line 383
  31. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.scale_tail_integral_tendsto line 391

    Source documentation

    Discarding all sufficiently small scales makes the squared-envelope integral vanish.

    theorem scale_tail_integral_tendsto {s₀ η T : ℝ}
    (hs₀ : 0 < s₀) (hη : 0 < η) (hηmax : η ≤ Real.log 2) (hT : 0 ≤ T) :
    Tendsto (fun N => ∫ u : ℝ × Transverse,
      squareEnvelope s₀ η u-(finiteEnvelope s₀ η (Finset.range N) u.1 u.2)^2
      ∂timeSpaceVolume T) atTop (𝓝 0) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.AnnularEnvelope.squareEnvelope, OAI.BoltzmannNonuniqueness.AnnularEnvelope.finiteEnvelope, OAI.BoltzmannNonuniqueness.AnnularEnvelope.timeSpaceVolume

  32. def OAI.BoltzmannNonuniqueness.AnnularEnvelope.cell line 432
  33. def OAI.BoltzmannNonuniqueness.AnnularEnvelope.momentMajorant line 434
  34. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.momentMajorant_nonneg line 437
  35. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.momentMajorant_integrable line 444
  36. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.affine_square_le line 465
  37. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.affine_squares_uniformIntegrable line 476
  38. def OAI.BoltzmannNonuniqueness.AnnularEnvelope.tailRegion line 517
  39. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.tailRegion_measurable line 520
  40. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.eventually_outside_tail line 528
  41. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.tail_integral_tendsto line 539
  42. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.tail_lintegral_tendsto line 554
  43. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.finiteEnvelope_le_inv_time line 581
  44. theorem OAI.BoltzmannNonuniqueness.AnnularEnvelope.finiteEnvelope_le_minimum_scale line 616