OAI/MathematicalPhysics/Boltzmann/Branching/WeightedJetSolutions.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Monotone and dominated limits for the weighted representative gain

  1. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.integrable_cutoff line 29
  2. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.gain_mono line 40
  3. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.gain_tendsto line 59
  4. def OAI.BoltzmannNonuniqueness.WeightedLocal.forcing line 104
  5. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.measurable_forcing line 107
  6. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.exists_normalized line 111
  7. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.exists_normalized_time line 145
  8. def OAI.BoltzmannNonuniqueness.weightFrequencyConstant line 186
  9. theorem OAI.BoltzmannNonuniqueness.weightFrequencyConstant_nonneg line 189
  10. theorem OAI.BoltzmannNonuniqueness.H_frequency_integrable line 196
  11. theorem OAI.BoltzmannNonuniqueness.H_frequency_le line 201
  12. theorem OAI.BoltzmannNonuniqueness.integral_rate_sum line 211
  13. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.core_add_weight_frequency_bound_ae line 226
  14. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.core_add_weight_frequency_bound line 272
  15. def OAI.BoltzmannNonuniqueness.WeightedFiniteSeed.amplitude line 303
  16. def OAI.BoltzmannNonuniqueness.WeightedFiniteSeed.seed line 306
  17. theorem OAI.BoltzmannNonuniqueness.WeightedFiniteSeed.measurable_seed line 309
  18. theorem OAI.BoltzmannNonuniqueness.WeightedFiniteSeed.amplitude_pos line 314
  19. theorem OAI.BoltzmannNonuniqueness.WeightedFiniteSeed.seed_bound line 318
  20. theorem OAI.BoltzmannNonuniqueness.WeightedFiniteSeed.exists_local line 334

    Source documentation

    A prescribed bounded nonnegative hot seed may be added to the actual finite periodic cold datum before the positive local construction.

    theorem exists_local {s₀ η K d₀ α q b B : ℝ} (hs₀ : 0 < s₀) (hsmax : s₀ ≤ 1 / 8)
    (hη : 0 ≤ η) (hK : 0 ≤ K) (hd₀ : 0 < d₀)
    (hwidth : d₀ * (1 / 8 : ℝ)^10 ≤ 1 / 64) (hα : 0 ≤ α) (hαmax : α ≤ 1 / 4)
    (hq : q < 2) (hb : 0 ≤ b) (hB : 0 ≤ B) (γ : ℝ) (N : ℕ)
    {h₀ : JetPrototype.Phase → ℝ} (hh₀m : Measurable h₀)
    (hh₀ : ∀ p, 0 ≤ h₀ p ∧ h₀ p ≤ B) :
    ∃ T L : ℝ, 0 < T ∧ 0 ≤ L ∧
      ∃ F : ℝ × JetPrototype.Phase → ℝ, Measurable F ∧
        (∀ z, 0 ≤ F z ∧ F z ≤ 2*(amplitude s₀ η K d₀ N+B)) ∧
        ∀ z, F z = PositiveIntegral.value T L JetBarrier.flight
          (fun p => seed s₀ η K α γ d₀ q N p + h₀ p) (WeightedLocal.forcing q b L F) z := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.WeightedFiniteSeed.amplitude, OAI.BoltzmannNonuniqueness.PositiveIntegral.value, OAI.BoltzmannNonuniqueness.JetBarrier.flight, OAI.BoltzmannNonuniqueness.WeightedFiniteSeed.seed, OAI.BoltzmannNonuniqueness.WeightedLocal.forcing

  21. def OAI.BoltzmannNonuniqueness.WeightedLocal.physical line 373
  22. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.physical_source line 376
  23. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.physical_mild line 391
  24. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.exists_positive_mild line 416
  25. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.density_velocity_integrable line 468
  26. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.physical_gain_add line 479
  27. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.physical_frequency_add line 516
  28. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.normalized_difference line 547
  29. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.finite_sum_gain_le line 613
  30. def OAI.BoltzmannNonuniqueness.HotRepresentative.coldSource line 676
  31. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.measurable_coldSource line 679
  32. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.coldSource_bounds line 683
  33. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.coldSource_mono line 701
  34. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.coldSource_tendsto line 711
  35. def OAI.BoltzmannNonuniqueness.WeightedLocal.coldForcing line 734
  36. def OAI.BoltzmannNonuniqueness.WeightedLocal.coldPicard line 737
  37. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.measurable_coldForcing line 743
  38. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.coldPicard_properties line 748
  39. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.physical_gain_le line 808
  40. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.physical_coldForcing_le line 824
  41. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.physical_value_along line 838
  42. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.physical_cold_integrable line 855
  43. def OAI.BoltzmannNonuniqueness.WeightedLocal.coldLimit line 897
  44. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.coldLimit_solution line 901
  45. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.cold_path_eq_damped line 979
  46. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.cold_survival line 991
  47. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.density_congr line 1060
  48. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.gain_congr line 1066
  49. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.frequency_congr line 1073
  50. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.source_congr line 1077
  51. def OAI.BoltzmannNonuniqueness.WeightedLocal.timeSlice line 1097
  52. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.forcing_timeSlice line 1100
  53. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.forcing_eq_of_slice line 1103
  54. def OAI.BoltzmannNonuniqueness.WeightedLocal.paste line 1109
  55. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.forcing_paste_left line 1112
  56. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.forcing_paste_right line 1117
  57. def OAI.BoltzmannNonuniqueness.WeightedTranslation.shift line 1139
  58. def OAI.BoltzmannNonuniqueness.WeightedTranslation.pull line 1141
  59. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.measurable_shift line 1144
  60. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.measurable_pull line 1148
  61. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.shift_flight line 1151
  62. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.forcing_pull line 1157
  63. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.coldForcing_pull line 1160
  64. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.value_pull line 1164
  65. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.fixed_point_pull line 1171
  66. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.coldPicard_pull line 1180
  67. theorem OAI.BoltzmannNonuniqueness.WeightedTranslation.coldLimit_pull line 1189
  68. theorem OAI.BoltzmannNonuniqueness.WeightedJetComparison.step_le line 1214