BarrierGeometry.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.BarrierConstruction.AffineBarrierData.box line 17
Source documentation
The physical reciprocal box for a constructed affine barrier.
```
def box (A : AffineBarrierData N κ x₀) : Set (Fin d → ℝ) :=
…
```
Mentions: OAI.Problem326.BarrierConstruction.AffineBarrierData
def OAI.Problem326.BarrierConstruction.AffineBarrierData.plateau line 21
Source documentation
The plateau selected by the constant branch, as finite affine inequalities.
```
def plateau (A : AffineBarrierData N κ x₀) : Set (Fin d → ℝ) :=
…
```
Mentions: OAI.Problem326.BarrierConstruction.AffineBarrierData
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.mem_plateau_iff_active line 24
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.initial_mem_plateau line 29
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.initial_mem_interior_box line 32
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.isCompact_box line 36
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.isClosed_box line 39
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.box_subset_positive line 41
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.inward_on_box line 49
Source documentation
Transfer the inward estimate from exponential coordinates to every physical point of the box. Strict positivity follows from box membership, not from an unproved positivity theorem for trajectories.
```
theorem inward_on_box (A : AffineBarrierData N κ x₀)
    {x : Fin d → ℝ} (hx : x ∈ A.box) {j : Fin A.n}
    (hj : AffineActive A.slope A.offset x j) :
    0 ≤ dot (A.slope j) (massAction N κ x) := by
…
```
Mentions: OAI.Problem326.BarrierConstruction.AffineBarrierData, OAI.Problem326.AffineActive, OAI.Problem326.dot, OAI.Problem326.massAction
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.constant_not_active_on_frontier line 65
Source documentation
A frontier point has an exponent coordinate of absolute value one, where the constant branch cannot be active.
```
theorem constant_not_active_on_frontier (A : AffineBarrierData N κ x₀)
    {x : Fin d → ℝ} (hx : x ∈ frontier A.box) :
    ¬ AffineActive A.slope A.offset x A.constant_branch := by
…
```
Mentions: OAI.Problem326.BarrierConstruction.AffineBarrierData, OAI.Problem326.AffineActive
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.plateau_disjoint_frontier line 79
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.plateau_isFinitePolyhedron line 85
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.plateau_subset_interior_box line 89
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.isCompact_plateau line 94
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.plateau_subset_positive line 98
theorem OAI.Problem326.BarrierConstruction.AffineBarrierData.geometric_properties line 104
Source documentation
The plateau is a compact convex polyhedron containing the initial point and lying strictly in the positive orthant.
```
theorem geometric_properties (A : AffineBarrierData N κ x₀) :
    IsCompact A.plateau ∧ Convex ℝ A.plateau ∧ IsFinitePolyhedron A.plateau ∧
      x₀ ∈ A.plateau ∧ A.plateau ⊆ {x | PositiveState x} :=
…
```
Mentions: OAI.Problem326.BarrierConstruction.AffineBarrierData, OAI.Problem326.IsFinitePolyhedron, OAI.Problem326.PositiveState