OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveIntegralFixedPoint.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoltzmannNonuniqueness.PositiveIntegral.Domain line 24
2. def OAI.BoltzmannNonuniqueness.PositiveIntegral.time line 26
3. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.time_bounds line 28
4. def OAI.BoltzmannNonuniqueness.PositiveIntegral.value line 32
5. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.measurable_value line 38
6. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_bounds line 74
7. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.damped_integrable line 103
8. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_difference line 120
9. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.exists_fixed_point line 144

   Source documentation

   Positive Picard iteration converges in the complete sup-norm space.

   theorem exists_fixed_point {T L A R S K : ℝ} (hT : 0 ≤ T) (hL : 0 ≤ L)
       (hA : 0 ≤ A) (hR : 0 ≤ R) (hS : 0 ≤ S) (hK : 0 ≤ K)
       (hball : A + T * S ≤ R) (hsmall : T * K < 1)
       {flow : ℝ → P → P} (hflow : Measurable (fun z : ℝ × P => flow z.1 z.2))
       {f₀ : P → ℝ} (hf₀m : Measurable f₀) (hf₀ : ∀ p, 0 ≤ f₀ p ∧ f₀ p ≤ A)
       (source : BoundedMeasurable.PositiveBall (Domain P) R → Domain P → ℝ)
       (hsm : ∀ f, Measurable (source f))
       (hsb : ∀ f z, 0 ≤ source f z ∧ source f z ≤ S)
       (hsl : ∀ f g z, |source f z - source g z| ≤ K * dist f g) :
       ∃ f : BoundedMeasurable.PositiveBall (Domain P) R,
         ∀ z, f.val z = value T L flow f₀ (source f) z := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.BoundedMeasurable.PositiveBall, OAI.BoltzmannNonuniqueness.PositiveIntegral.Domain, OAI.BoltzmannNonuniqueness.PositiveIntegral.value

10. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_mono line 207
11. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_tendsto line 220
12. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_rescale line 255
13. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.fixed_point_unique line 305
14. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_difference_initial line 345
15. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_finsetSum line 383
16. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.hasSum_value line 418
17. theorem OAI.BoltzmannNonuniqueness.positive_marginal_bound line 462