RegularBoundaryAtlas.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.MahlerStokes.RegularBoundaryPatch line 12
Source documentation
A bounded open portion of a genuine regular-level chart, inside U.
```
structure RegularBoundaryPatch (d : ℕ) (U : Set (Fin d → ℝ))
    (g : (Fin d → ℝ) → ℝ) where
…
```
theorem OAI.MahlerStokes.exists_regularBoundaryPatch line 25

structure OAI.MahlerStokes.RegularBoundaryAtlas line 37

Source documentation

A finite cover extracted from actual derivative-based charts.

structure RegularBoundaryAtlas (d : ℕ) (U : Set (Fin d → ℝ))
    (g : (Fin d → ℝ) → ℝ) (K : Set (Fin d → ℝ)) where
…

theorem OAI.MahlerStokes.exists_regularBoundaryAtlas line 46

theorem OAI.MahlerStokes.RegularBoundaryPatch.sublevel_iff line 66

Source documentation

The chart identifies the actual sublevel with the lower coordinate half-space.

theorem RegularBoundaryPatch.sublevel_iff {d : ℕ} {U : Set (Fin d → ℝ)}
    {g : (Fin d → ℝ) → ℝ} (p : RegularBoundaryPatch d U g) {R : ℝ}
    {x : Fin d → ℝ} (hx : x ∈ p.domain) :
    x ∈ regularSublevel U g R ↔ p.chart x p.coordinate < R := by
…

Mentions: OAI.MahlerStokes.RegularBoundaryPatch, OAI.MahlerStokes.regularSublevel

theorem OAI.MahlerStokes.exists_sublevelBoundaryAtlas line 73