OAI/Analysis/MassAction/PolyhedronGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem326.continuous_dot line 12
2. lemma OAI.Problem326.dot_add_right line 16
3. lemma OAI.Problem326.dot_smul_right line 19
4. lemma OAI.Problem326.dot_isLinearMap line 22
5. lemma OAI.Problem326.IsFinitePolyhedron.isClosed line 28
6. lemma OAI.Problem326.IsFinitePolyhedron.convex line 36
7. lemma OAI.Problem326.finiteAffine_superlevel_isFinitePolyhedron line 44
8. lemma OAI.Problem326.finiteAffine_superlevel_isClosed line 61
9. lemma OAI.Problem326.finiteAffine_superlevel_convex line 66
10. lemma OAI.Problem326.finiteAffine_plateau_eq line 73

    Source documentation

    A capped finite lower envelope has a polyhedral maximum set. This interface is independent of the choice of finite-minimum notation.

    lemma finiteAffine_plateau_eq {ι : Type uIota}
        (a : ι → (Fin d → ℝ)) (c : ι → ℝ) (F : (Fin d → ℝ) → ℝ) (M : ℝ)
        (hlower : ∀ x j, F x ≤ dot (a j) x + c j)
        (hattained : ∀ x, ∃ j, F x = dot (a j) x + c j)
        (hceiling : ∀ x, F x ≤ M) :
        {x | F x = M} = {x | ∀ j, M ≤ dot (a j) x + c j} := by
    …

    Mentions: OAI.Problem326.dot

11. lemma OAI.Problem326.finiteAffine_plateau_isFinitePolyhedron line 88
12. lemma OAI.Problem326.compact_polyhedron_of_affine_barriers line 99

    Source documentation

    Finite affine barriers which exclude the boundary of a compact set produce a compact convex polyhedron in its interior.

    lemma compact_polyhedron_of_affine_barriers {ι : Type uIota} [Fintype ι]
        (a : ι → (Fin d → ℝ)) (c : ι → ℝ) (M : ℝ)
        (B : Set (Fin d → ℝ)) (x0 : Fin d → ℝ)
        (hB : IsCompact B) (hx0B : x0 ∈ interior B)
        (hx0 : ∀ j, M ≤ dot (a j) x0 + c j)
        (hboundary : ∀ x ∈ frontier B, ∃ j, dot (a j) x + c j < M) :
        ∃ K : Set (Fin d → ℝ), IsCompact K ∧ Convex ℝ K ∧
          IsFinitePolyhedron K ∧ x0 ∈ K ∧ K ⊆ interior B ∧
          ∀ x, x ∈ K ↔ ∀ j, M ≤ dot (a j) x + c j := by
    …

    Mentions: OAI.Problem326.dot, OAI.Problem326.IsFinitePolyhedron

13. lemma OAI.Problem326.compact_polyhedron_of_zero_active_slope line 125

    Source documentation

    A zero slope active at the initial point supplies the ceiling level. Excluding zero active slopes on the boundary gives all geometric conclusions.

    lemma compact_polyhedron_of_zero_active_slope {ι : Type uIota} [Fintype ι]
        (a : ι → (Fin d → ℝ)) (c : ι → ℝ) (j0 : ι)
        (B : Set (Fin d → ℝ)) (x0 : Fin d → ℝ)
        (hB : IsCompact B) (hx0B : x0 ∈ interior B)
        (hzero : a j0 = 0)
        (hactive0 : ∀ j, dot (a j0) x0 + c j0 ≤ dot (a j) x0 + c j)
        (hboundary : ∀ x ∈ frontier B, ∀ j,
          (∀ k, dot (a j) x + c j ≤ dot (a k) x + c k) → a j ≠ 0) :
        ∃ K : Set (Fin d → ℝ), IsCompact K ∧ Convex ℝ K ∧
          IsFinitePolyhedron K ∧ x0 ∈ K ∧ K ⊆ interior B ∧
          ∀ x, x ∈ K ↔ ∀ j, c j0 ≤ dot (a j) x + c j := by
    …

    Mentions: OAI.Problem326.dot, OAI.Problem326.IsFinitePolyhedron