theorem G67SumCoordinate.integral_fiber_density {L U s : ℝ} (hL : 0 < L) (hLU : L ≤ U) (hU : U < s) : ∫ (u : ℝ) in L..U, 1 / (u * (s - u)) = Real.log (U * (s - L) / (L * (s - U))) / s

Exact integration of the reciprocal density along a positive sum fiber.

noncomputable def G67SumCoordinate.weight (a b c d s : ℝ) : ℝ

The closed-form fiber weight, including its zero endpoint values.

Equations

• G67SumCoordinate.weight a b c d s = Real.log (G67SumCoordinate.upper b c s * (s - G67SumCoordinate.lower a d s) / (G67SumCoordinate.lower a d s * (s - G67SumCoordinate.upper b c s))) / s

theorem G67SumCoordinate.fiber_integral {a b c d s : ℝ} (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (hs : s ∈ Set.Icc (a + c) (b + d)) : ∫ (u : ℝ) in lower a d s..upper b c s, 1 / (u * (s - u)) = weight a b c d s

No antiderivative or fiber integral is carried as a premise.