Positivity and ordering consequences
ProvedWeightedRootIntegralIdentity.missionDataConsequencesbranch-cutcomplex-analysisordered-reals
For positive ordered branch points, every open integration interval lies in the positive half-line, has nonnegative orientation, and avoids the pole at zero.
Formal statement
import Mathlib
open scoped Interval
theorem WeightedRootIntegralIdentity.missionDataConsequences
(n : ℕ) (hn : 2 ≤ n) (a : ℕ → ℝ)
(hpos : ∀ i < n, 0 < a i)
(hmono : ∀ i < n - 1, a i ≤ a (i + 1)) :
(∀ k < n - 1, a k ≤ a (k + 1)) ∧
(∀ k < n - 1, ∀ x ∈ Set.Ioo (a k) (a (k + 1)), 0 < x ∧ x ≠ 0) := by sorry