OAI/MathematicalPhysics/Boltzmann/Collision/SheetMixtures.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Tightness and axial nonconcentration for sheet mixtures

The full kernel depends linearly on its incoming measure. Consequently the same tail bound and axial modulus hold for the probability mixtures allowed by the manuscript's sheet class.

  1. def OAI.BoltzmannNonuniqueness.SheetMixtures.regionFiber line 26
  2. theorem OAI.BoltzmannNonuniqueness.SheetMixtures.measurable_regionFiber line 30
  3. theorem OAI.BoltzmannNonuniqueness.SheetMixtures.measure_eq_regionFiber line 35
  4. theorem OAI.BoltzmannNonuniqueness.SheetMixtures.measure_bind_apply line 42
  5. theorem OAI.BoltzmannNonuniqueness.SheetMixtures.normalized_bind_apply line 51
  6. theorem OAI.BoltzmannNonuniqueness.SheetMixtures.mixture_tail_bound line 57
  7. theorem OAI.BoltzmannNonuniqueness.SheetMixtures.dominated_tail_bound line 72
  8. theorem OAI.BoltzmannNonuniqueness.SheetMixtures.measurableSet_axialRegion line 83
  9. theorem OAI.BoltzmannNonuniqueness.SheetMixtures.mixture_axial_modulus line 88

    Source documentation

    The elementary modulus works without change for every probability mixture.

    theorem mixture_axial_modulus {q L ε : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (a b : ℝ), 0 < b - a → b - a ≤ δ →
      ∀ {ι : Type*} [MeasurableSpace ι] (ν : Measure ι) [IsProbabilityMeasure ν]
        (M : ι → Measure Velocity), Measurable M → (∀ᵐ i ∂ν, IsElementary L (M i)) →
        ∀ (v : Velocity), transverse v ≠ 0 →
          normalizedMeasure (ν.bind M) q v (axialRegion v a b) ≤ ENNReal.ofReal ε := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity