SubordinateFutureBoxes.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite coordinate boxes containing complete bounded future fibers

The compact closure of the bounded intrinsic future can be transported back to any sampled coordinate. A genuine quotient box can contain this whole compact set, and can itself be cut down to a finite coordinate cube.

theorem OAI.DukePrimeDegree.RootPrefixCoordinates.exists_bounded_box_containing_rebased_cube line 24

theorem OAI.DukePrimeDegree.RootPrefixCoordinates.exists_bounded_box_containing_futureFiber line 50

Source documentation

Apply the compact-box construction to a bounded entire future fiber.

theorem exists_bounded_box_containing_futureFiber
    (C : RootPrefixCoordinates n P V) (c : EliminationChain P D)
    (hP : InitialRootPattern P) (hf : c.finalEntries = allPositiveRoots n)
    (g : G n) (s : UpperRootTransverse n × V) (t : c.Time)
    (hinj : Function.Injective (fun u => C.timeParam c hP hf g (s,u)))
    (T : X n → X n) (Q : X n → ℕ) (m : ℕ) (R : ℝ)
    (hbound : ∀ v : c.Time,
      (∀ k : ℕ, Q (T^[k+m] (rightAction (C.timeParam c hP hf g (s,t)) (c.word v))) =
        Q (T^[k+m] (C.timeParam c hP hf g (s,t)))) → v ∈ c.cube R) :
    ∃ (B : RootPrefixBox C c hP hf g) (S : ℝ), 0 < S ∧
      s ∈ B.transverse ∧ t ∈ B.time ∧ B.time ⊆ c.cube S ∧
      {u | ∀ k : ℕ, Q (T^[k+m] (C.timeParam c hP hf g (s,u))) =
…

Mentions: OAI.DukePrimeDegree.RootPrefixCoordinates, OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.InitialRootPattern, OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.UpperRootTransverse, OAI.DukePrimeDegree.RootPrefixBox