OAI/NumberTheory/DukePrimeDegree/Entropy/RootPrefixAmbientFuture.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DukePrimeDegree.normalized_restriction_map_equiv line 13
2. lemma OAI.DukePrimeDegree.RootPrefixBox.map_uncentered_future_eq_ambient line 32

   Source documentation

   The box expression, once unrestricted, is exactly the intrinsic whole-future measure pushed along the actual root orbit through its sample.

   lemma map_uncentered_future_eq_ambient
       (B : RootPrefixBox C c hP₀ hf g)
       (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
       (ell : Fin (d+1) → ℝ) (hell : ∑ k, ell k=0) (Q : X (d+1) → ℕ)
       (m : ℕ) (z : (UpperRootTransverse (d+1) × V) × c.Time) :
       let T := fun x => rightAction x (diagonalOneParameter ell hell (-1))
   …

   Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.UpperRootTransverse