OAI/MathematicalPhysics/Boltzmann/Branching/WeightedHotRegularity.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.finite_sum_coldSource_le line 22
2. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.finite_sum_picard_le line 54
3. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.finite_sum_coldLimit_le line 107
4. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.cold_family_summable line 123
5. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.gain_family_summable line 162
6. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.tsum_coldSource line 176
7. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.hot_source_identity line 189
8. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.hot_source_le_single line 203

   Source documentation

   Dropping the common loss and all but one of the subtracted cold gains.

   theorem hot_source_le_single {β b R : ℝ} (L : ℝ)
       {c : I → X × Velocity → ℝ} {F : X × Velocity → ℝ}
       (hcm : ∀ i, Measurable (c i)) (hFm : Measurable F)
       (hc : ∀ i p, 0 ≤ c i p ∧ c i p ≤ R) (hF : ∀ p, 0 ≤ F p ∧ F p ≤ R)
       (hSum : ∀ s : Finset I, ∀ p, ∑ i ∈ s, c i p ≤ F p)
       (i : I) (p : X × Velocity) :
       source β b L F p - (∑' j, coldSource β b L F (c j) p) -
           L * (F p - ∑' j, c j p) ≤ gain β b F p - gain β b (c i) p := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.HotRepresentative.source, OAI.BoltzmannNonuniqueness.HotRepresentative.coldSource, OAI.BoltzmannNonuniqueness.HotRepresentative.gain

9. lemma OAI.BoltzmannNonuniqueness.Compactness.abs_le_mass_add_variance line 235
10. theorem OAI.BoltzmannNonuniqueness.Compactness.strongL1_of_weighted_variance line 244
11. lemma OAI.BoltzmannNonuniqueness.Compactness.weighted_variance_identity line 295
12. theorem OAI.BoltzmannNonuniqueness.Compactness.weighted_variance_moments line 300
13. def OAI.BoltzmannNonuniqueness.WeightedLocal.hotRemainder line 365
14. def OAI.BoltzmannNonuniqueness.WeightedLocal.hotForcing line 369
15. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.value_sub line 373
16. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.hotRemainder_solution line 394
17. theorem OAI.BoltzmannNonuniqueness.Compactness.weighted_moments_strong line 473
18. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.hot_regularity line 527