OAI/Analysis/AffineBernstein/OrthantGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.continuous_ambientCoordinate line 22
2. def OAI.AffineBernstein.ambientOrthant line 29
3. lemma OAI.AffineBernstein.isClosed_ambientOrthant line 32
4. lemma OAI.AffineBernstein.pos_mem_interior_ambientOrthant line 37
5. lemma OAI.AffineBernstein.graph_not_mem_interior_epigraph line 44
6. lemma OAI.AffineBernstein.affineGraph_not_mem_interior_epigraph line 60
7. theorem OAI.AffineBernstein.orthant_limit_boundary_strips line 71

   Source comment

   Under local-set convergence to the orthant, every bounded boundary point eventually lies in a thin coordinate strip.

   theorem orthant_limit_boundary_strips {n : ℕ} {Cj : ℕ → Set (Space n × ℝ)}
       (h : LocalDistanceConverges Cj (ambientOrthant n))
       (hclj : ∀ j, IsClosed (Cj j)) (hcvj : ∀ j, Convex ℝ (Cj j))
       (hnej : ∀ j, (Cj j).Nonempty) {R ε : ℝ} (hε : 0 < ε) :
       ∀ᶠ j in atTop, ∀ z ∈ Cj j, z ∉ interior (Cj j) → ‖z‖ ≤ R →
         ∃ i, |ambientCoordinates n z i| ≤ ε := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.ambientOrthant, OAI.AffineBernstein.ambientCoordinates