Initial wall mixing is controlled by two weighted amplitude columns

Proved

BianchiIX.entrance_initial_wall_mixing

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

Let $k\geq1$ , $\theta,u,v,w\in[0,1]$ , and $X,Y\in\mathbb R$ . Then

(u|X|+w|Y|)\left(uv+\frac{uvw+\theta(vw)^2}{k^2}\right) \leq3\bigl(uv|X|+(uvw+\theta(vw)^2)|Y|\bigr).

Preamble

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX

Formal statement

theorem BianchiIX.entrance_initial_wall_mixing {k θ u v w X Y : ℝ}
    (hk : 1 ≤ k) (hθ : 0 ≤ θ ∧ θ ≤ 1)
    (hu : 0 ≤ u ∧ u ≤ 1) (hv : 0 ≤ v ∧ v ≤ 1) (hw : 0 ≤ w ∧ w ≤ 1) :
    (u * |X| + w * |Y|) * (u * v + (u * v * w + θ * (v * w) ^ 2) / k ^ 2) ≤
      3 * (u * v * |X| + (u * v * w + θ * (v * w) ^ 2) * |Y|) := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Algebra/EntranceVariationMixing.lean#L9-L47

View graph