OAI/MathematicalPhysics/Boltzmann/Branching/HotSeedCoreLower.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

A localized periodic thermal seed, normalized in the singular weighted norm

  1. def OAI.BoltzmannNonuniqueness.HotSeedProfile.centered line 20
  2. def OAI.BoltzmannNonuniqueness.HotSeedProfile.centeredSpace line 22
  3. def OAI.BoltzmannNonuniqueness.HotSeedProfile.raw line 25
  4. def OAI.BoltzmannNonuniqueness.HotSeedProfile.bound line 29
  5. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.bound_pos line 31
  6. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.centered_sub_int line 35
  7. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.centeredSpace_shift line 39
  8. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.raw_periodic line 46
  9. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.measurable_centered line 52
  10. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.measurable_centeredSpace line 55
  11. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.measurable_raw line 62
  12. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.raw_nonneg line 70
  13. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.velocity_bound line 73
  14. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.raw_le line 93
  15. def OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized line 101
  16. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized_size line 104
  17. theorem OAI.BoltzmannNonuniqueness.PhaseEssSup.size_pos_of_positive_set line 127
  18. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.centered_eq line 138
  19. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.centeredSpace_eq line 144
  20. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.J_pos line 153
  21. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.raw_pos line 160
  22. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.raw_size_pos line 176
  23. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized_measurable line 208
  24. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized_periodic line 211
  25. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized_bounds line 216
  26. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized_norm line 225
  27. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized_velocity_support line 229
  28. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized_data line 236
  29. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.J_eq_bound line 260
  30. def OAI.BoltzmannNonuniqueness.HotSeedProfile.velocityCore line 266
  31. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.velocityCore_open line 268
  32. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.velocityCore_nonempty line 275
  33. def OAI.BoltzmannNonuniqueness.HotSeedProfile.velocityBound line 287
  34. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.velocityBound_pos line 289
  35. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.H_le_velocityBound line 293
  36. def OAI.BoltzmannNonuniqueness.HotSeedProfile.normLower line 305
  37. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normLower_pos line 307
  38. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.spatial_core line 310
  39. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.raw_ge_normLower line 324
  40. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normLower_le_size line 335
  41. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized_uniform_bound line 351
  42. def OAI.BoltzmannNonuniqueness.HotSeedProfile.periodicDensity line 382
  43. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.periodicDensity_measurable line 385
  44. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.periodicDensity_nonneg line 391
  45. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.periodicDensity_bound line 396
  46. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.integrable_weight_torus line 400
  47. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.periodicDensity_integrable line 406
  48. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.periodicDensity_support line 414
  49. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.periodicDensity_L1_tendsto line 422

    Source documentation

    Every allowed bounded cap-shot parameter gives the same vanishing hot perturbation.

    theorem periodicDensity_L1_tendsto {q : ℝ} (hq : 0 ≤ q) (hqmax : q < 2)
    {δ ell : ℕ → ℝ} (hδ : ∀ n, 0 < δ n) (hδmax : ∀ n, δ n ≤ 1)
    (hδlim : Tendsto δ atTop (𝓝 0)) (hell : ∀ n, ell n ∈ Set.Icc (0:ℝ) 2) :
    Tendsto (fun n => ∫ p : Phase, ‖ell n*periodicDensity q (δ n) p‖) atTop (𝓝 0) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Phase, OAI.BoltzmannNonuniqueness.HotSeedProfile.periodicDensity

  50. theorem OAI.BoltzmannNonuniqueness.HotScalarBound.remainder_majorant line 464
  51. theorem OAI.BoltzmannNonuniqueness.HotSeedProfile.normalized_core_lower line 506