PositiveVariationEquality.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Equality in the positive-variation bound

Attaining the total positive variation at an intermediate time forces the derivative to have the two ordered signs on either side of that time.

theorem OAI.PolycyclicRecognition.positive_variation_equality_signs line 21

Source documentation

The equality case used at a maximizing time of each scalar weight of a profile. The positive and negative variations are derived from the integrable derivative; their vanishing is a conclusion.

theorem positive_variation_equality_signs
    (q : ℝ → ℝ) {a t b : ℝ} (hat : a ≤ t) (htb : t ≤ b)
    (hq : IntervalIntegrable q volume a b)
    (heq : (∫ s in a..t, q s) = ∫ s in a..b, max (q s) 0) :
    (∀ᵐ s ∂volume.restrict (Ioc a t), 0 ≤ q s) ∧
      (∀ᵐ s ∂volume.restrict (Ioc t b), q s ≤ 0) := by
…