LabelTrajectory.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.Affine.active_iff_value_eq_inf line 14
Source documentation
The comparison-based activity convention agrees with attaining the finite minimum, including every tied branch.
```
theorem active_iff_value_eq_inf {d : ℕ} {Λ : Finset (Label d)}
    (hne : Λ.Nonempty) {L : Label d} {h : ℝ} {z : Fin d → ℝ} :
    Active Λ L h z ↔
      L ∈ Λ ∧ L.value h z = Λ.inf' hne (fun J => J.value h z) := by
…
```
Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Active

theorem OAI.Problem326.Affine.trapped_of_active_inward line 29

Source documentation

Canonical affine labels directly supply the finite-interval trapping principle. Only active slopes inside the closed region need point inward.

theorem trapped_of_active_inward
    {d : ℕ} (Λ : Finset (Label d)) (hne : Λ.Nonempty) (h : ℝ)
    (f : (Fin d → ℝ) → (Fin d → ℝ)) (B : Set (Fin d → ℝ))
    {x : ℝ → (Fin d → ℝ)} {T M : ℝ}
    (hT : 0 ≤ T) (hclosed : IsClosed B)
    (hx : ContinuousOn x (Icc 0 T))
    (hxd : ∀ t ∈ Ioo 0 T, HasDerivAt x (f (x t)) t)
    (hx0 : x 0 ∈ interior B)
    (hinward : ∀ z ∈ B, ∀ L, Active Λ L h z →
      0 ≤ dot L.slope (f z))
    (hceiling : ∀ z ∈ B, Λ.inf' hne (fun L => L.value h z) ≤ M)
    (hstart : Λ.inf' hne (fun L => L.value h (x 0)) = M)
…

Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Active, OAI.Problem326.dot