OAI/MathematicalPhysics/Boltzmann/Collision/AxialSecondMismatch.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The actual compact thermal parameters preserve axial decay

  1. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.sourceFoot_abs_lower line 21
  2. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.weight_axial_decay line 37
  3. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.gaussian_axial_decay line 69
  4. theorem OAI.BoltzmannNonuniqueness.AxialFlow.profile_dilation line 99
  5. theorem OAI.BoltzmannNonuniqueness.AxialFlow.velocity_dilation line 105
  6. theorem OAI.BoltzmannNonuniqueness.AxialFlow.foot_dilation line 114
  7. theorem OAI.BoltzmannNonuniqueness.AxialFlow.velocity_scale_tendsto line 121
  8. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap_dilation line 152
  9. theorem OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap_error_le line 159
  10. def OAI.BoltzmannNonuniqueness.AxialBackground.weight line 184

    Source documentation

    The stripe fraction is exactly one quarter in the supplied manuscript.

    def weight (K α γ μ t σ z : ℝ) : ℝ :=
…
  11. def OAI.BoltzmannNonuniqueness.AxialBackground.atom line 187
  12. def OAI.BoltzmannNonuniqueness.AxialBackground.cell line 191
  13. theorem OAI.BoltzmannNonuniqueness.AxialBackground.weight_nonneg line 194
  14. theorem OAI.BoltzmannNonuniqueness.AxialBackground.weight_bound line 199
  15. theorem OAI.BoltzmannNonuniqueness.AxialBackground.integrable_atom line 204
  16. theorem OAI.BoltzmannNonuniqueness.AxialBackground.integral_atom line 208
  17. theorem OAI.BoltzmannNonuniqueness.AxialBackground.integral_cell line 215
  18. theorem OAI.BoltzmannNonuniqueness.AxialBackground.atom_gain_bound line 223
  19. theorem OAI.BoltzmannNonuniqueness.AxialBackground.cell_gain_bound line 235
  20. theorem OAI.BoltzmannNonuniqueness.AxialFlow.velocity_collapsed_uniform line 260
  21. theorem OAI.BoltzmannNonuniqueness.AxialFlow.thermal_velocity_collapsed_uniform line 287
  22. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.axial_measure_domination line 327
  23. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.normalized_core_axial_decay line 359
  24. theorem OAI.BoltzmannNonuniqueness.AxialFlow.ballistic_axial_gap_identity line 396
  25. theorem OAI.BoltzmannNonuniqueness.AxialFlow.ballistic_axial_gap line 402
  26. theorem OAI.BoltzmannNonuniqueness.AxialFlow.thermal_second_gap line 412

    Source documentation

    A gap at the first collision persists at the next collision up to the thermal error.

    theorem thermal_second_gap {σ α γ s t₁ t₂ z w d ω b : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht₂ : 0 ≤ t₂) (htt : t₂ ≤ t₁)
    (hgap : b ≤ |w-velocity σ α γ s t₁ z|) (herr : |d*ω| ≤ b/2) :
    b/2 ≤ |w-JetCoreMap.axialMap σ α γ s d t₂ (z-(t₁-t₂)*w) ω| := by
…

    Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.velocity, OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap

  27. theorem OAI.BoltzmannNonuniqueness.AxialFlow.small_scale_second_gap line 426

    Source documentation

    Small scales need only exclude the two endpoint speeds and the ballistic speed at the first collision. The scale threshold is independent of both collision positions.

    theorem small_scale_second_gap {α γ a δ : ℝ}
    (hα : 0 < α) (hγ : 0 < γ) (ha : 0 < a) (hδ : 0 < δ) :
    ∃ μ₀ : ℝ, 0 < μ₀ ∧ ∀ (σ s d t₁ t₂ z w ω : ℝ),
      0 < s → s < μ₀ → a ≤ t₂ → t₂ ≤ t₁ → |d*ω| < δ/4 →
      δ ≤ |w-(σ-α)| → δ ≤ |w-(σ+α)| → δ ≤ |w-z/t₁| →
      δ/2 ≤ |w-JetCoreMap.axialMap σ α γ s d t₂ (z-(t₁-t₂)*w) ω| := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetCoreMap.axialMap