OAI/GroupTheory/PolycyclicRecognition/Geometry/AffineProfileBoundary.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.affine_profile_on_closed_cell line 21

   Source documentation

   Affineness over the interior already determines the profile over the closed convex cell, including the contact facet. Surjectivity of height is retained, so closure commutes with its inverse image.

   theorem affine_profile_on_closed_cell
       (q : V →ₗ[ℝ] W) (hq : Continuous q) (hqsurj : Function.Surjective q)
       (C : Set W) (hC : Convex ℝ C) (hclosed : IsClosed C)
       (hint : (interior C).Nonempty)
       (f : V → Y) (hf : Continuous f) (A : W →L[ℝ] Y) (b : Y)
       (haffine : ∀ z, q z ∈ interior C → f z = A (q z) + b) :
       ∀ z, q z ∈ C → f z = A (q z) + b := by
   …

2. theorem OAI.PolycyclicRecognition.affine_offset_tendsto line 42

   Source documentation

   Once the linear label is fixed, evaluating at one eventually affine point determines the limiting offset; no separate boundedness assumption on the offsets is needed.

   theorem affine_offset_tendsto
       (f : ℕ → C(V, Y)) (g : C(V, Y)) (hf : Filter.Tendsto f Filter.atTop (nhds g))
       (z : V) (a : Y) (b : ℕ → Y)
       (h : ∀ᶠ n in Filter.atTop, f n z = a + b n) :
       Filter.Tendsto b Filter.atTop (nhds (g z - a)) := by
   …

3. theorem OAI.PolycyclicRecognition.affine_profile_limit_on_closed_cell line 55

   Source documentation

   A limiting label on expanding interior domains extends to the closed cell. Only pointwise eventual membership is needed for the exhaustion.

   theorem affine_profile_limit_on_closed_cell
       (q : V →ₗ[ℝ] W) (hq : Continuous q) (hqsurj : Function.Surjective q)
       (C : Set W) (hC : Convex ℝ C) (hclosed : IsClosed C)
       (hint : (interior C).Nonempty)
       (f : ℕ → C(V, Y)) (g : C(V, Y)) (hf : Filter.Tendsto f Filter.atTop (nhds g))
       (A : W →L[ℝ] Y) (b : ℕ → Y) (c : Y)
       (hb : Filter.Tendsto b Filter.atTop (nhds c))
       (haffine : ∀ z, q z ∈ interior C → ∀ᶠ n in Filter.atTop, f n z = A (q z) + b n) :
       ∀ z, q z ∈ C → g z = A (q z) + c := by
   …