Extended Young inequality for screening

Positivity of the finite screening coefficient in extended Young.

The exact additive extended Young bound of extended Young.

theorem LiebThirring.Assembly.young_screening_coefficient_pos (κ : ℝ) (hκ : 0 < κ) : 0 < 2 / 5 * (3 / 5) ^ (3 / 2) * κ ^ (-3 / 2)

Positivity of the finite screening coefficient in extended Young.

theorem LiebThirring.Assembly.young_screening (κ : ℝ) (hκ : 0 < κ) (w t : ENNReal) : w * t ≤ ENNReal.ofReal κ * t ^ (5 / 3) + ENNReal.ofReal (2 / 5 * (3 / 5) ^ (3 / 2) * κ ^ (-3 / 2)) * w ^ (5 / 2)

The exact additive extended Young bound of extended Young.