OAI/MathematicalPhysics/Boltzmann/Jets/JetCoreMomentBound.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Replacing the annular part of the full oscillating mask

  1. theorem OAI.BoltzmannNonuniqueness.JetGeometry.mask_indicator_factor line 19
  2. theorem OAI.BoltzmannNonuniqueness.JetGeometry.mask_error_le line 26
  3. theorem OAI.BoltzmannNonuniqueness.JetGeometry.spatial_mask_L1_tendsto line 37
  4. def OAI.BoltzmannNonuniqueness.SheetClass.exponentialMoment line 111
  5. theorem OAI.BoltzmannNonuniqueness.SheetClass.exponentialMoment_mono line 114
  6. theorem OAI.BoltzmannNonuniqueness.SheetClass.exponentialMoment_smul line 117
  7. theorem OAI.BoltzmannNonuniqueness.SheetClass.exponentialMoment_add line 120
  8. theorem OAI.BoltzmannNonuniqueness.SheetClass.elementary_exponentialMoment line 123
  9. theorem OAI.BoltzmannNonuniqueness.SheetClass.exponentialMoment_density line 133
  10. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.exponential_moment_le line 147
  11. def OAI.BoltzmannNonuniqueness.JetEscapedTotal.annulus line 225
  12. def OAI.BoltzmannNonuniqueness.JetEscapedTotal.total line 229
  13. def OAI.BoltzmannNonuniqueness.JetEscapedTotal.coefficient line 232
  14. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.coefficient_nonneg line 235
  15. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.annulus_bound line 244
  16. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.scale_bound line 271
  17. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.annular_tail_summable line 276
  18. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.annular_tail_bound line 281
  19. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.total_amplitude_bound line 298
  20. def OAI.BoltzmannNonuniqueness.JetEscapedTotal.powerConstant line 322
  21. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.powerConstant_nonneg line 326
  22. theorem OAI.BoltzmannNonuniqueness.JetEscapedTotal.arbitrary_power line 335
  23. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.epsilon_eq line 381
  24. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.epsilon_small line 387
  25. def OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.escapedSum line 395
  26. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.sum_le_twice line 401
  27. def OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.constant line 440
  28. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.constant_nonneg line 443
  29. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.arbitrary_power line 448
  30. def OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.exponent line 479
  31. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.exponent_large line 481
  32. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.le_exponent line 485
  33. theorem OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.real_power line 492

    Source documentation

    The same constant works for every time, spatial point, and retained subset.

    theorem real_power {s₀ η K α γ d₀ t : ℝ} (hs₀ : 0 < s₀) (hsmax : s₀ ≤ 1 / 8)
    (hη : 0 < η) (hηmax : η ≤ Real.log 2) (hK : 0 ≤ K) (hα : 0 ≤ α) (hαmax : α ≤ 1)
    (hγ : 0 ≤ γ) (hd₀ : 0 < d₀) (hd₀max : d₀ ≤ 1) (ht : 0 < t) (htmax : t ≤ 1 / 32)
    (hsmall : JetComparisonCoefficient.coefficient K * d₀ * s₀ ^ 9 ≤ 1) (A q : ℝ)
    (S : ℕ → Bool → Lattice → Prop) (F : ℕ → Bool → Lattice → ℝ)
    (x v : Velocity) (hx : ∀ k, |x k| ≤ 1)
    (hF : ∀ j a n, S j a n → F j a n ≤ JetSupersolution.U η K α γ
      (jetScale s₀ η j) (d₀ * jetScale s₀ η j ^ 10) t a (shifted x n, v)) :
    escapedSum s₀ η t x S F ≤
      ENNReal.ofReal (constant s₀ η α K d₀ (exponent A) * t ^ A * H q v) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetComparisonCoefficient.coefficient, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.JetSupersolution.U, OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.escapedSum, OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.constant, OAI.BoltzmannNonuniqueness.JetEscapedEnvelope.exponent

  34. def OAI.BoltzmannNonuniqueness.JetMainGain.sheetConstant line 529
  35. theorem OAI.BoltzmannNonuniqueness.JetMainGain.sheetConstant_pos line 532
  36. theorem OAI.BoltzmannNonuniqueness.JetMainGain.sheet_bound line 536
  37. def OAI.BoltzmannNonuniqueness.JetMainGain.coefficient line 542
  38. theorem OAI.BoltzmannNonuniqueness.JetMainGain.numerator_nonneg line 546
  39. theorem OAI.BoltzmannNonuniqueness.JetMainGain.coefficient_nonneg line 554
  40. theorem OAI.BoltzmannNonuniqueness.JetMainGain.amplitude_nonneg line 557
  41. theorem OAI.BoltzmannNonuniqueness.JetMainGain.nonnegative_gain_bound line 566
  42. theorem OAI.BoltzmannNonuniqueness.JetMainGain.gain_bound line 593
  43. theorem OAI.BoltzmannNonuniqueness.JetMainGain.dominated_gain line 612
  44. def OAI.BoltzmannNonuniqueness.JetGeometry.maskError line 653
  45. theorem OAI.BoltzmannNonuniqueness.JetGeometry.maskError_measurable line 659
  46. theorem OAI.BoltzmannNonuniqueness.JetGeometry.maskError_abs_le line 674
  47. theorem OAI.BoltzmannNonuniqueness.JetGeometry.maskError_integrable line 688
  48. theorem OAI.BoltzmannNonuniqueness.JetGeometry.maskError_average_L1_le line 697
  49. theorem OAI.BoltzmannNonuniqueness.JetGeometry.maskError_average_L1_tendsto line 711
  50. theorem OAI.BoltzmannNonuniqueness.SheetClass.weighted_integrable_of_exponentialMoment line 744
  51. theorem OAI.BoltzmannNonuniqueness.SheetClass.weighted_integral_le line 754
  52. theorem OAI.BoltzmannNonuniqueness.SheetClass.density_integrable_of_exponentialMoment line 764
  53. theorem OAI.BoltzmannNonuniqueness.SheetClass.density_mass_le line 773
  54. theorem OAI.BoltzmannNonuniqueness.SheetClass.density_tail_le line 782
  55. def OAI.BoltzmannNonuniqueness.JetEnvelopeGain.momentConstant line 825
  56. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.momentConstant_nonneg line 829
  57. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.exponential_moment_uniform line 832
  58. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.dominated_exponential_moment line 850
  59. theorem OAI.BoltzmannNonuniqueness.JetEnvelopeGain.dominated_mass_tail line 861