OAI/MathematicalPhysics/Boltzmann/Branching/LargeOutput.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.LargeOutputSlices.one_le_weight line 22
2. theorem OAI.BoltzmannNonuniqueness.LargeOutputSlices.ballChartFiber_threshold line 26
3. def OAI.BoltzmannNonuniqueness.LargeOutputSlices.boundedIncoming line 37
4. def OAI.BoltzmannNonuniqueness.LargeOutputSlices.boundedBall line 39
5. theorem OAI.BoltzmannNonuniqueness.LargeOutputSlices.measurableSet_boundedIncoming line 42
6. theorem OAI.BoltzmannNonuniqueness.LargeOutputSlices.measurableSet_boundedBall line 45
7. theorem OAI.BoltzmannNonuniqueness.LargeOutputSlices.axial_mismatch_lower line 48
8. theorem OAI.BoltzmannNonuniqueness.LargeOutputSlices.weight_boundedBall_bound line 58
9. def OAI.BoltzmannNonuniqueness.LargeOutput.axialConstant line 105
10. theorem OAI.BoltzmannNonuniqueness.LargeOutput.axialConstant_nonneg line 108
11. theorem OAI.BoltzmannNonuniqueness.LargeOutput.normalized_boundedBall_bound line 115
12. def OAI.BoltzmannNonuniqueness.LargeOutput.transverseConstant line 143
13. theorem OAI.BoltzmannNonuniqueness.LargeOutput.transverseConstant_nonneg line 146
14. theorem OAI.BoltzmannNonuniqueness.LargeOutput.normalized_awayBall_bound line 153
15. theorem OAI.BoltzmannNonuniqueness.LargeOutput.transverse_norm_le line 178
16. theorem OAI.BoltzmannNonuniqueness.LargeOutput.ball_subset_away line 182
17. theorem OAI.BoltzmannNonuniqueness.LargeOutput.uniform_large_output line 195

    Source documentation

    Uniform decay of the full kernel as the output velocity goes to infinity.

    theorem uniform_large_output {q L ε : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
        (hε : 0 < ε) :
        ∃ M : ℝ, 0 < M ∧ ∀ (d : ℝ) (ρ : Measure ℝ) (_ : IsProbabilityMeasure ρ)
          (_ : 0 ≤ d) (_ : d ≤ 1 / 8) (_ : AxialMoment ρ L)
          (v : Velocity) (_ : transverse v ≠ 0) (_ : M < ‖v‖),
          normalizedMeasure (sheetLaw d ρ) q v univ ≤ ENNReal.ofReal ε := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity