PositiveSequenceMinimum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Endpoint minimum for a positive finite log-concave sequence

This is the finite inequality needed by the conditional-variance paths. After one strict decrease, the local product inequality forces every subsequent step to decrease, so there can be no valley between endpoints.

lemma OAI.ContingencyTables.positive_sequence_drop line 16

theorem OAI.ContingencyTables.positive_sequence_minimum line 31

Source documentation

Only positivity and the local three-term product inequality are needed, on the finite interval actually used by the application.

theorem positive_sequence_minimum (a : ℕ → ℝ) (N i j k : ℕ)
    (hpos : ∀ n, n ≤ N → 0 < a n)
    (hlog : ∀ n, n+2 ≤ N → a n*a (n+2) ≤ (a (n+1))^2)
    (hij : i ≤ j) (hjk : j ≤ k) (hkN : k ≤ N) : min (a i) (a k) ≤ a j := by
…