OAI/MathematicalPhysics/Boltzmann/Collision/AxialAtomicSheet.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Uniform axial nonconcentration

The small-interval estimate and the vanishing velocity tails give one modulus for every elementary sheet and every outgoing velocity off the axis.

  1. def OAI.BoltzmannNonuniqueness.AxialModulus.axialRegion line 28
  2. def OAI.BoltzmannNonuniqueness.AxialModulus.intervalMajorant line 31
  3. theorem OAI.BoltzmannNonuniqueness.AxialModulus.tendsto_intervalMajorant line 34
  4. theorem OAI.BoltzmannNonuniqueness.AxialModulus.axialRegion_subset line 44
  5. theorem OAI.BoltzmannNonuniqueness.AxialModulus.axialRegion_bound line 55
  6. theorem OAI.BoltzmannNonuniqueness.AxialModulus.uniform_axial_modulus line 67

    Source documentation

    Uniform non-atomicity of the incoming axial marginal, with the full weight.

    theorem uniform_axial_modulus {q L ε : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (a b : ℝ), 0 < b - a → b - a ≤ δ →
      ∀ (d : ℝ) (ρ : Measure ℝ) (_ : IsProbabilityMeasure ρ)
        (_ : 0 ≤ d) (_ : d ≤ 1 / 8) (_ : AxialMoment ρ L)
        (v : Velocity) (_ : transverse v ≠ 0),
        normalizedMeasure (sheetLaw d ρ) q v (axialRegion v a b) ≤ ENNReal.ofReal ε := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.AxialModulus.axialRegion

  7. theorem OAI.BoltzmannNonuniqueness.AxialAtomicSheet.sheetLaw_zero_dirac line 113
  8. theorem OAI.BoltzmannNonuniqueness.AxialAtomicSheet.dirac_elementary line 120
  9. theorem OAI.BoltzmannNonuniqueness.AxialAtomicSheet.velocity_abs_le line 134
  10. theorem OAI.BoltzmannNonuniqueness.AxialAtomicSheet.velocity_elementary line 142
  11. theorem OAI.BoltzmannNonuniqueness.AxialAtomicSheet.normalized_gain_bound line 148