OAI/MathematicalPhysics/Boltzmann/Branching/SmallFirstGain.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.SmallInputGeometry.fiber line 24
2. theorem OAI.BoltzmannNonuniqueness.SmallInputGeometry.abs_axial_le_norm line 29
3. theorem OAI.BoltzmannNonuniqueness.SmallInputGeometry.fiber_le_smallFiber line 33
4. def OAI.BoltzmannNonuniqueness.SmallInputGeometry.threshold line 47
5. theorem OAI.BoltzmannNonuniqueness.SmallInputGeometry.threshold_pos line 49
6. theorem OAI.BoltzmannNonuniqueness.SmallInputGeometry.fiber_eq_zero_of_small_mismatch line 53
7. theorem OAI.BoltzmannNonuniqueness.SmallInputGeometry.fiber_uniform_bound line 67
8. def OAI.BoltzmannNonuniqueness.SmallInput.region line 116
9. def OAI.BoltzmannNonuniqueness.SmallInput.lowIncoming line 119
10. def OAI.BoltzmannNonuniqueness.SmallInput.lowRegion line 121
11. theorem OAI.BoltzmannNonuniqueness.SmallInput.measurableSet_region line 124
12. theorem OAI.BoltzmannNonuniqueness.SmallInput.measurableSet_lowIncoming line 128
13. theorem OAI.BoltzmannNonuniqueness.SmallInput.measurableSet_lowRegion line 131
14. theorem OAI.BoltzmannNonuniqueness.SmallInput.weight_lowRegion_bound line 134
15. theorem OAI.BoltzmannNonuniqueness.SmallInput.normalized_lowRegion_bound line 159
16. def OAI.BoltzmannNonuniqueness.SmallInput.highRegion line 181
17. theorem OAI.BoltzmannNonuniqueness.SmallInput.measurableSet_highRegion line 184
18. theorem OAI.BoltzmannNonuniqueness.SmallInput.normalized_highRegion_bound line 187
19. def OAI.BoltzmannNonuniqueness.SmallInputLimit.lowBound line 244
20. def OAI.BoltzmannNonuniqueness.SmallInputLimit.highBound line 249
21. theorem OAI.BoltzmannNonuniqueness.SmallInputLimit.lowBound_tendsto line 252
22. theorem OAI.BoltzmannNonuniqueness.SmallInputLimit.highBound_tendsto line 271
23. def OAI.BoltzmannNonuniqueness.SmallInputLimit.smallRegion line 284
24. theorem OAI.BoltzmannNonuniqueness.SmallInputLimit.uniform_small_input line 289

    Source documentation

    The thin-sheet small-input limit, uniformly in every output velocity whose transverse component is at least r.

    theorem uniform_small_input {q L r ε : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
        (hr : 0 < r) (hε : 0 < ε) :
        ∃ δ η : ℝ, 0 < δ ∧ 0 < η ∧ ∀ (d : ℝ) (ρ : Measure ℝ) (_ : IsProbabilityMeasure ρ)
          (_ : 0 ≤ d) (_ : d ≤ min η (1 / 8)) (_ : AxialMoment ρ L)
          (v : Velocity) (_ : r ≤ ‖transverse v‖),
          normalizedMeasure (sheetLaw d ρ) q v (smallRegion v δ) ≤ ENNReal.ofReal ε := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.SmallInputLimit.smallRegion

25. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.five_tendsto_of_small_first_mass line 363