Prove2Me

Wall amplitude and corrected divergence

Definition
BianchiIX_Algebra_Flux

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

bianchi-ix-era-statisticsdynamical-systems

For real variables p,s,a,b,cp,s,a,b,c, set

K=a2+b2+c2−2(ab+bc+ca),S=p2+s2,C=S+K.K=a^2+b^2+c^2-2(ab+bc+ca),\qquad S=p^2+s^2,\qquad C=S+K.

The shear components and wall rates are

P=Kp−2a2+b2+c2+ab−2bc+ac,P=Kp-2a^2+b^2+c^2+ab-2bc+ac, Q=Ks+3(−b2+c2+ab−ac),Q=Ks+\sqrt{3}(-b^2+c^2+ab-ac), r1=−S+2p,r2=−S−p+3s,r3=−S−p−3s.r_1=-S+2p,\qquad r_2=-S-p+\sqrt{3}s,\qquad r_3=-S-p-\sqrt{3}s.

These functions define the normalized vacuum Bianchi IX vector field (P,Q,r1a,r2b,r3c)(P,Q,r_1a,r_2b,r_3c).

Define H(a,b,c)=(abc)2/3H(a,b,c)=(abc)^{2/3} and

Δ(q,h)=2(q+4h)1+4h.\Delta(q,h)=\frac{2(q+4h)}{1+4h}.

Real powers and division have their total Lean meanings.

Definition code
import Mathlib.Analysis.Calculus.Deriv.Pow
import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Analysis.Calculus.Deriv.Add
import Mathlib.Analysis.Real.Sqrt
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
import Mathlib.Tactic.FieldSimp

/-! The sharp curvature bound and the positive corrected divergence, Section 5.2. -/

namespace BianchiIX

noncomputable section









def correctedDivergence (q h : ℝ) : ℝ := 2 * (q + 4 * h) / (1 + 4 * h)







def wallAmplitude (a b c : ℝ) : ℝ := (a * b * c) ^ (2 / 3 : ℝ)









end

end BianchiIX
Source
https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Algebra/Flux.lean

View graph