OAI/Analysis/ForestSpace/Exhaustions.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ForestSpace.ancestral_exhaustion_tendsto line 18

   Source documentation

   Every increasing ancestral exhaustion converges by coordinate density and tail contractivity, without reflexivity.

   theorem ancestral_exhaustion_tendsto (H : ℕ → Finset V)
       (hH : ∀ n, IsLowerSet (H n : Set V)) (hmono : Monotone H)
       (hcover : ∀ v : V, ∃ n, v ∈ H n) (x : X V) :
       Filter.Tendsto (fun n => PX (H n) (hH n) x) Filter.atTop (nhds x) := by
   …

   Mentions: OAI.ForestSpace.X, OAI.ForestSpace.PX

2. theorem OAI.ForestSpace.approximate_tail_outside line 48

   Source documentation

   Completed tails are approximated by finite coordinate combinations outside the ancestral head.

   theorem approximate_tail_outside (H : Finset V) (hH : IsLowerSet (H : Set V))
       (y : X V) (hy : y = QX H hH y) (ε : ℝ) (hε : 0 < ε) :
       ∃ z : FullDual V, z ∈ Submodule.span ℝ (eStar '' (H : Set V)ᶜ) ∧
         ‖(y : FullDual V)-z‖ < ε := by
   …

   Mentions: OAI.ForestSpace.X, OAI.ForestSpace.QX, OAI.ForestSpace.FullDual, OAI.ForestSpace.eStar