OAI/Analysis/SphereIsometry/InvariantConvexSet.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

A closed invariant convex set from proved finite-prefix growth. The input growth theorem is instantiated by the geometric common-support argument; the recursion, positive scheduling, density and invariance are proved here.

  1. def OAI.Tingley.recursivePrefix line 22

    Source documentation

    Ordinary finite-prefix recursion; no admissibility proof enters the data.

    def recursivePrefix (G : X → X) (v₀ : X) : (n : ℕ) → (Fin (n+1) → X)
  | 0 => fun _ => v₀
  | n+1 => Fin.snoc (α := fun _ : Fin (n+2) => X) (recursivePrefix G v₀ n)
…
  2. def OAI.Tingley.recursiveVector line 27
  3. theorem OAI.Tingley.recursiveVector_zero line 30
  4. theorem OAI.Tingley.recursivePrefix_eq_vector line 33
  5. theorem OAI.Tingley.recursiveVector_succ line 45
  6. def OAI.Tingley.PositivePrefixGrowth line 56

    Source documentation

    The geometric one-step conclusion for the invariant convex set.

    def PositivePrefixGrowth (G : X → X) (E : Set X) : Prop :=
…
  7. theorem OAI.Tingley.recursivePrefix_hull_subset line 63
  8. theorem OAI.Tingley.recursiveVector_prefix_hull_subset line 80
  9. theorem OAI.Tingley.recursiveVector_mem line 90
  10. theorem OAI.Tingley.recursiveStageMean_mem line 96
  11. def OAI.Tingley.recursiveConvexSet line 106

    Source documentation

    The closed convex hull of the one actual recursively constructed sequence.

    def recursiveConvexSet (G : X → X) (v₀ : X) : Set X :=
…
  12. theorem OAI.Tingley.recursiveConvexSet_subset line 109
  13. theorem OAI.Tingley.recursiveConvexSet_nonempty line 116
  14. theorem OAI.Tingley.isClosed_recursiveConvexSet line 121
  15. theorem OAI.Tingley.convex_recursiveConvexSet line 124
  16. theorem OAI.Tingley.recursiveConvexSet_invariant line 127
  17. theorem OAI.Tingley.exists_invariant_closed_convex line 148

    Source documentation

    No density or invariant-set premise: both are obtained from the positive recursion.

    theorem exists_invariant_closed_convex (G : X → X) (E : Set X) (v₀ : X)
    (hv₀ : v₀ ∈ E) (hE : IsClosed E) (hunit : ∀ x ∈ E, ‖x‖ = 1)
    (hG : ContinuousOn G E) (hstep : PositivePrefixGrowth G E) :
    ∃ C : Set X, C.Nonempty ∧ IsClosed C ∧ Bornology.IsBounded C ∧
      Convex ℝ C ∧ C ⊆ E ∧ Set.MapsTo G C C := by
…

    Mentions: OAI.Tingley.PositivePrefixGrowth