Exact scalar Rumin integration

Rescaling the finite cutoff interval to [0,1] evaluates the squared positive part with coefficient 9/35. Integrability is established before conversion to the extended integral. See Frank, Hundertmark, Jex and Nam (2018), equation (8).

theorem LiebThirring.Assembly.rumin_integrableOn (t d : ℝ) (ht : 0 ≤ t) (hd : 0 < d) : MeasureTheory.IntegrableOn (fun (E : ℝ) => max (√t - √d * E ^ (3 / 4)) 0 ^ 2) (Set.Ioi 0) MeasureTheory.volume

The scalar Rumin positive part is integrable on the positive half-line (scalar Rumin integration).

theorem LiebThirring.Assembly.integral_rumin (t d : ℝ) (ht : 0 ≤ t) (hd : 0 < d) : ∫ (E : ℝ) in Set.Ioi 0, max (√t - √d * E ^ (3 / 4)) 0 ^ 2 = 9 / 35 * d ^ (-2 / 3) * t ^ (5 / 3)

Exact scalar Rumin integral, with coefficient 9/35 (scalar Rumin integration).

theorem LiebThirring.Assembly.lintegral_rumin (t d : ℝ) (ht : 0 ≤ t) (hd : 0 < d) : ∫⁻ (E : ℝ) in Set.Ioi 0, ENNReal.ofReal (max (√t - √d * E ^ (3 / 4)) 0 ^ 2) = ENNReal.ofReal (9 / 35 * d ^ (-2 / 3) * t ^ (5 / 3))

The nonnegative extended integral equals the same finite scalar value (scalar Rumin integration).

theorem LiebThirring.Assembly.ruminConstant_pos : 0 < ruminConstant

The exact Rumin coefficient is strictly positive (the Rumin bound).