OAI/MathematicalPhysics/Boltzmann/Branching/DampedLateBoxPhysicalBlock.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.DampedGainHistory.step line 22
2. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.step_slab_mono line 28
3. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.step_measurable line 39
4. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.step_add line 64
5. def OAI.BoltzmannNonuniqueness.DampedGainHistory.iterate line 78
6. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.iterate_measurable line 83
7. def OAI.BoltzmannNonuniqueness.DampedGainHistory.partialSum line 91
8. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.partialSum_le line 97

   Source documentation

   Positive remainders imply domination of every finite collection of collision depths.

   theorem partialSum_le {a T : ℝ} (K : Kernel KineticPhase Velocity)
       (W : KineticPhase × ℝ → ℝ≥0∞) {f d : KineticPhase → ℝ≥0∞}
       (h : ∀ z, z.1.1 ∈ Icc a T → d z+step a K W f z ≤ f z) (n : ℕ) :
       ∀ z, z.1.1 ∈ Icc a T → partialSum a K W d n z ≤ f z := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.DampedGainHistory.step, OAI.BoltzmannNonuniqueness.DampedGainHistory.partialSum

9. def OAI.BoltzmannNonuniqueness.WeakTime.dampedTimeWeight line 124
10. theorem OAI.BoltzmannNonuniqueness.WeakTime.dampedTimeWeight_measurable line 127
11. theorem OAI.BoltzmannNonuniqueness.WeakTime.dampedTimeWeight_bounds line 130
12. theorem OAI.BoltzmannNonuniqueness.WeakTime.dampedSourceIncrement_integral line 137
13. theorem OAI.BoltzmannNonuniqueness.WeakTime.dampedSourceIncrement_weighted_integral line 162
14. def OAI.BoltzmannNonuniqueness.WeakTime.dampedPhaseTest line 172
15. theorem OAI.BoltzmannNonuniqueness.WeakTime.dampedPhaseTest_measurable line 175
16. theorem OAI.BoltzmannNonuniqueness.WeakTime.dampedPhaseTest_bound line 180
17. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.partialSum_measurable line 210
18. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.partialSum_succ line 218
19. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.partialSum_eq line 232
20. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.finite_histories_le line 240
21. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.all_histories_le line 249
22. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.iterate_factorial_bound line 275
23. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.iterate_slab_mono line 346
24. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.iterate_add line 354
25. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.iterate_step line 364
26. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.residual_expansion line 371
27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaled_bounded_history_map line 408
28. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaled_endpoint_integral line 418
29. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledBlockMass line 464
30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedDensityScaledBlockMass_eq line 471
31. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.sum_iterate_le_exp line 512
32. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.all_histories_le_exp line 536
33. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.remainder_tendsto_zero line 545
34. theorem OAI.BoltzmannNonuniqueness.DampedGainHistory.eq_history_sum line 565

    Source documentation

    The bounded solution is exhausted by its finite positive collision histories.

    theorem eq_history_sum {a T C B : ℝ} (hC : 0 ≤ C) (hB : 0 ≤ B)
        (K : Kernel KineticPhase Velocity) [IsSFiniteKernel K]
        {W : KineticPhase × ℝ → ℝ≥0∞} (hWm : Measurable W)
        (hW : ∀ z, z.1.1 ∈ Icc a T → ∀ s ∈ Ioc a z.1.1, W (z,s) ≤ 1)
        (hK : ∀ z, z.1.1 ∈ Icc a T → K z univ ≤ ENNReal.ofReal C)
        {f d : KineticPhase → ℝ≥0∞} (hd : Measurable d)
        (hf : ∀ z, z.1.1 ∈ Icc a T → f z ≤ ENNReal.ofReal B)
        (heq : ∀ z, z.1.1 ∈ Icc a T → f z = d z+step a K W f z)
        (z : KineticPhase) (hz : z.1.1 ∈ Icc a T) :
        f z = ∑' j, iterate a K W d j z := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.DampedGainHistory.step, OAI.BoltzmannNonuniqueness.DampedGainHistory.iterate

35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBox_damped_physical_block_growth line 603