OAI/MathematicalPhysics/Boltzmann/Collision/SheetIntervals.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.SheetTotal.shellTerm line 27
2. theorem OAI.BoltzmannNonuniqueness.SheetTotal.shellTerm_nonneg line 30
3. theorem OAI.BoltzmannNonuniqueness.SheetTotal.summable_shellTerm line 34
4. def OAI.BoltzmannNonuniqueness.SheetTotal.bound line 51
5. theorem OAI.BoltzmannNonuniqueness.SheetTotal.bound_lt_top line 55
6. theorem OAI.BoltzmannNonuniqueness.SheetTotal.cover_by_shells line 63
7. theorem OAI.BoltzmannNonuniqueness.SheetTotal.normalized_total_bound line 79

   Source documentation

   Uniform finiteness and the complete gain bound for an elementary sheet.

   theorem normalized_total_bound {q d L : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
       (hd : 0 ≤ d) (hdmax : d ≤ 1 / 8) {v : Velocity} (hv : transverse v ≠ 0)
       {ρ : Measure ℝ} [IsProbabilityMeasure ρ] (hρ : AxialMoment ρ L) :
       normalizedChartGain (sheetLaw d ρ) q v ≤ bound q L := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.normalizedChartGain, OAI.BoltzmannNonuniqueness.SheetTotal.bound

8. theorem OAI.BoltzmannNonuniqueness.SheetTotal.normalized_total_lt_top line 99
9. def OAI.BoltzmannNonuniqueness.SheetClass.fiber line 131
10. theorem OAI.BoltzmannNonuniqueness.SheetClass.measurable_fiber line 134
11. theorem OAI.BoltzmannNonuniqueness.SheetClass.gain_eq_lintegral_fiber line 137
12. theorem OAI.BoltzmannNonuniqueness.SheetClass.gain_bind line 144
13. def OAI.BoltzmannNonuniqueness.SheetClass.IsElementary line 153

    Source documentation

    The elementary class allows both zero transverse width and arbitrary axial atoms.

    def IsElementary (L : ℝ) (c : Measure Velocity) : Prop :=
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity

14. theorem OAI.BoltzmannNonuniqueness.SheetClass.elementary_bound line 157
15. theorem OAI.BoltzmannNonuniqueness.SheetClass.mixture_bound line 164
16. theorem OAI.BoltzmannNonuniqueness.SheetClass.domination_bound line 178
17. theorem OAI.BoltzmannNonuniqueness.SheetApplication.gain_const_mul_right line 214
18. theorem OAI.BoltzmannNonuniqueness.SheetApplication.gain_H_eq line 230
19. theorem OAI.BoltzmannNonuniqueness.SheetApplication.ae_transverse_ne_zero line 242
20. theorem OAI.BoltzmannNonuniqueness.SheetApplication.nonnegativeGain_sheet_bound line 257

    Source documentation

    The original nonnegative hard-sphere gain obeys the sheet domination bound, conditionally only on the published Carleman identity.

    theorem nonnegativeGain_sheet_bound
        (hcarleman : Published.GPV2009CarlemanInput)
        {ι : Type*} [MeasurableSpace ι] {ν : Measure ι} [IsProbabilityMeasure ν]
        {M : ι → Measure Velocity} (hM : Measurable M)
        {q L : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
        (hc : ∀ᵐ i ∂ν, IsElementary L (M i))
        {f : Velocity → ℝ≥0∞} (hf : Measurable f) {A : ℝ≥0∞}
        (hdom : volume.withDensity f ≤ A • ν.bind M) :
        ∀ᵐ v : Velocity ∂volume,
          nonnegativeGain f (fun ξ => ENNReal.ofReal (H q ξ)) v ≤
            ENNReal.ofReal (H q v) * (A * SheetTotal.bound q L) := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.nonnegativeGain, OAI.BoltzmannNonuniqueness.SheetTotal.bound

21. def OAI.BoltzmannNonuniqueness.SheetTightness.tailRegion line 300
22. def OAI.BoltzmannNonuniqueness.SheetTightness.tailBound line 303
23. theorem OAI.BoltzmannNonuniqueness.SheetTightness.tendsto_tailBound line 306
24. theorem OAI.BoltzmannNonuniqueness.SheetTightness.measurableSet_tailRegion line 310
25. theorem OAI.BoltzmannNonuniqueness.SheetTightness.cover_tail line 314
26. theorem OAI.BoltzmannNonuniqueness.SheetTightness.normalized_tail_bound line 332
27. theorem OAI.BoltzmannNonuniqueness.SheetTightness.uniform_tail line 345

    Source documentation

    A single truncation works for every width, axial law and off-axis output.

    theorem uniform_tail {q L : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
        {ε : ℝ≥0∞} (hε : 0 < ε) :
        ∃ N : ℕ, ∀ n ≥ N, ∀ (d : ℝ) (ρ : Measure ℝ) (_ : IsProbabilityMeasure ρ)
          (_ : 0 ≤ d) (_ : d ≤ 1 / 8) (_ : AxialMoment ρ L)
          (v : Velocity) (_ : transverse v ≠ 0),
          normalizedMeasure (sheetLaw d ρ) q v (tailRegion v n) ≤ ε := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.SheetTightness.tailRegion

28. def OAI.BoltzmannNonuniqueness.SheetIntervals.intervalRegion line 387
29. theorem OAI.BoltzmannNonuniqueness.SheetIntervals.mem_intervalRegion line 390
30. theorem OAI.BoltzmannNonuniqueness.SheetIntervals.measurableSet_intervalRegion line 398
31. def OAI.BoltzmannNonuniqueness.SheetIntervals.intervalFiber line 403
32. theorem OAI.BoltzmannNonuniqueness.SheetIntervals.intervalFiber_le_slice line 409
33. theorem OAI.BoltzmannNonuniqueness.SheetIntervals.interval_gain_eq line 456
34. def OAI.BoltzmannNonuniqueness.SheetIntervals.intervalBound line 480
35. theorem OAI.BoltzmannNonuniqueness.SheetIntervals.weight_interval_bound line 483
36. theorem OAI.BoltzmannNonuniqueness.SheetIntervals.weight_interval_measure_bound line 505
37. theorem OAI.BoltzmannNonuniqueness.SheetIntervals.normalized_interval_bound line 514

    Source documentation

    The axial interval bound includes the complete ratio H(ξ)/H(v).

    theorem normalized_interval_bound {q d R L a b : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
        (hd : 0 ≤ d) (hdmax : d ≤ 1 / 8) (hR : 0 < R) (hab : a < b)
        {v : Velocity} (hv : transverse v ≠ 0) {ρ : Measure ℝ} [IsProbabilityMeasure ρ]
        (hρ : AxialMoment ρ L) :
        normalizedMeasure (sheetLaw d ρ) q v (intervalRegion v R a b) ≤
          ENNReal.ofReal tiltConstant * ENNReal.ofReal (4 * L) * intervalBound q R (b - a) := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.SheetIntervals.intervalRegion, OAI.BoltzmannNonuniqueness.SheetIntervals.intervalBound

38. theorem OAI.BoltzmannNonuniqueness.SheetIntervals.intervalBound_mono line 532
39. theorem OAI.BoltzmannNonuniqueness.SheetIntervals.intervalBound_tendsto_zero line 543