Prove2Me

Fluids with larger ww disappear faster

Proved
CosmologyEOS.larger_w_dilutes_faster

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

cosmologymathematical-physics

Let w1<w2w_1<w_2. Let aa be the scale factor and let (ε1,p1)(\varepsilon_1,p_1), (ε2,p2)(\varepsilon_2,p_2) be two perfect fluids in the same universe: all functions are differentiable at all times, a>0a>0, ε1>0\varepsilon_1>0, pi=wiεip_i = w_i\varepsilon_i, and each fluid satisfies the fluid equation ε˙i=−3a˙a(εi+pi)\dot\varepsilon_i = -3\frac{\dot a}{a}(\varepsilon_i+p_i). If the universe expands without bound, a(t)→∞a(t)\to\infty as t→∞t\to\infty, then

ε2(t)ε1(t)⟶0(t→∞).\frac{\varepsilon_2(t)}{\varepsilon_1(t)} \longrightarrow 0 \qquad (t\to\infty).

So the fluid with the larger equation of state becomes negligible relative to the other.

Preamble
import Mathlib
import Definitions.Def_CosmologyEOS_Defs

open Real Filter Topology
Formal statement
namespace CosmologyEOS

theorem larger_w_dilutes_faster (w₁ w₂ : ℝ) (hw : w₁ < w₂) (a ε₁ ε₂ p₁ p₂ : ℝ → ℝ)
    (ha_diff : ∀ t, DifferentiableAt ℝ a t)
    (hε₁_diff : ∀ t, DifferentiableAt ℝ ε₁ t)
    (hε₂_diff : ∀ t, DifferentiableAt ℝ ε₂ t)
    (ha_pos : ∀ t, 0 < a t)
    (hε₁_pos : ∀ t, 0 < ε₁ t)
    (heos₁ : ∀ t, p₁ t = w₁ * ε₁ t) (heos₂ : ∀ t, p₂ t = w₂ * ε₂ t)
    (hfluid₁ : ∀ t, FluidEquation a ε₁ p₁ t) (hfluid₂ : ∀ t, FluidEquation a ε₂ p₂ t)
    (hexpand : Tendsto a atTop atTop) :
    Tendsto (fun t => ε₂ t / ε₁ t) atTop (𝓝 0) := by
  sorry

end CosmologyEOS
Source
Wikipedia, "Equation of state (cosmology)", revision 1375011367, https://en.wikipedia.org/w/index.php?title=Equation_of_state_(cosmology)&oldid=1375011367, section 'Fluids'
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statement below, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare the Lean code with the source themselves.

Let w1,w2∈Rw_1,w_2\in\mathbb R with w1<w2w_1<w_2 and let a,ε1,ε2,p1,p2:R→Ra,\varepsilon_1,\varepsilon_2,p_1,p_2:\mathbb R\to\mathbb R. Assume for every t∈Rt\in\mathbb R: aa, ε1\varepsilon_1, ε2\varepsilon_2 are differentiable at tt; a(t)>0a(t)>0; ε1(t)>0\varepsilon_1(t)>0; p1(t)=w1ε1(t)p_1(t) = w_1\varepsilon_1(t) and p2(t)=w2ε2(t)p_2(t) = w_2\varepsilon_2(t); and for i=1,2i=1,2, εi′(t)=−3 a′(t)a(t)(εi(t)+pi(t))\varepsilon_i^{\prime}(t) = -3\,\dfrac{a^{\prime}(t)}{a(t)}(\varepsilon_i(t)+p_i(t)). Assume also a(t)→+∞a(t)\to+\infty as t→+∞t\to+\infty. Then ε2(t)/ε1(t)→0\varepsilon_2(t)/\varepsilon_1(t)\to 0 as t→+∞t\to+\infty. No sign condition is imposed on ε2\varepsilon_2.

Human review

View graph