OAI/MathematicalPhysics/Boltzmann/Jets/ColdGaussianFamily.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.ColdGronwall.primitive line 23
2. theorem OAI.BoltzmannNonuniqueness.ColdGronwall.eq_zero_of_integral_bound line 26

   Source documentation

   A nonnegative integrable error bounded by a constant times its past integral vanishes.

   theorem eq_zero_of_integral_bound {z : ℝ → ℝ} {C T : ℝ} (hC : 0 ≤ C) (hT : 0 ≤ T)
       (hi : IntervalIntegrable z volume 0 T) (hz : ∀ t ∈ Icc 0 T, 0 ≤ z t)
       (hb : ∀ t ∈ Icc 0 T, z t ≤ C * primitive z t) : ∀ t ∈ Icc 0 T, z t = 0 := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.ColdGronwall.primitive

3. def OAI.BoltzmannNonuniqueness.GaussianLocal.coldForcing line 80
4. def OAI.BoltzmannNonuniqueness.GaussianLocal.coldPicard line 84
5. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.measurable_coldForcing line 90
6. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.coldPicard_properties line 94
7. theorem OAI.BoltzmannNonuniqueness.JetBarrier.off_axis_bound line 147
8. def OAI.BoltzmannNonuniqueness.JetSupersolution.transverseDecayConstant line 182
9. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.transverseDecayConstant_nonneg line 185
10. theorem OAI.BoltzmannNonuniqueness.JetSupersolution.off_axis_small_scale line 191
11. def OAI.BoltzmannNonuniqueness.GaussianLocal.coldLimit line 233
12. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.coldLimit_solution line 237
13. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.finite_sum_picard_le line 322
14. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.finite_sum_coldLimit_le line 373
15. theorem OAI.BoltzmannNonuniqueness.GaussianLocal.cold_family_summable line 389